Theorem: SchwartzMap.decay₁ (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
intro k n
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
have := @one_add_le_sup_seminorm_apply ℝ E F _ _ _ _ _ _ _ ⟨k, n⟩ k n (by simp) (by simp) f
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ (k, n).1 * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ (k, n).1 * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
simp at this
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ k * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
this :
  ∀ (x : E),
    (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
      2 ^ k * (Finset.sup (Finset.Iic (k, n)) fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
⊢ ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
use ((2 : ℝ) ^ k) * Finset.sup (Finset.Iic (k, n)) (fun m => SchwartzMap.seminorm ℝ m.1 m.2) f
State after:
no goals

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ k ≤ (k, n).1
Tactic:
simp
State after:
no goals

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
k n : ℕ
⊢ n ≤ (k, n).2
Tactic:
simp
State after:
no goals