Theorem: SchwartzMap.hasTemperateGrowth (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ Function.HasTemperateGrowth ⇑f
Tactic:
refine ⟨f.smooth', ?_⟩
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k

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

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hf_decay := f.decay' 0 n
State after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
hf_decay : ∃ C, ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
hf_decay : ∃ C, ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf_decay with ⟨C, hC⟩
State after:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k

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

State before:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨0, C, ?_⟩
State after:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0

State before:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0
Tactic:
simpa
State after:
no goals