Theorem: Function.hasTemperateGrowth_const (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
c : F
⊢ HasTemperateGrowth fun x => c
Tactic:
refine ⟨contDiff_const, ?_⟩
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
c : F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) 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
c : F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) 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
c : F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) 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
c : F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨0, ‖c‖, ?_⟩
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
c : F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ ‖c‖ * (1 + ‖x‖) ^ 0

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
c : F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ ‖c‖ * (1 + ‖x‖) ^ 0
Tactic:
cases n <;> simp [iteratedFDeriv_const_of_ne]
State after:
no goals