Theorem: Function.HasTemperateGrowth.bound_forall_range (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine _root_.bound_forall_range n ?_
State after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
⊢ ∀ i < n, ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k

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

State before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : E → F
hf : HasTemperateGrowth f
i : ℕ
a✝ : i < n
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
exact hf.2 i
State after:
no goals