Theorem: Complex.hasTemperateGrowth_exp_real_smul_I (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Tactic:
refine ⟨contDiff_exp_real_smul_I, ?_⟩
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨n, 1, ?_⟩
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
intro x
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedDeriv n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedDeriv n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
rw [iteratedDeriv_exp_real_smul_I]
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖I ^ n * cexp (x • I)‖ ≤ 1 * (1 + ‖x‖) ^ n

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖I ^ n * cexp (x • I)‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
simp
State after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ (1 + |x|) ^ n

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ (1 + |x|) ^ n
Tactic:
exact one_le_pow_of_one_le (by simp) n
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ 1 + |x|
Tactic:
simp
State after:
no goals