𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ HasDerivAt exp (exp x) x
rw [hasDerivAt_iff_isLittleO_nhds_zero]
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
have : (1 : ℕ) < 2 := by norm_num
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖exp (x + x_1) - exp x - x_1 • exp x‖ ≤ ‖exp x‖ * ‖x_1 ^ 2‖
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ (fun h => exp (x + h) - exp x - h • exp x) =o[𝓝 0] fun h => h
refine' (IsBigO.of_bound ‖exp x‖ _).trans_isLittleO (isLittleO_pow_id this)
case h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), a ∈ Metric.ball 0 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a ^ 2‖
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖exp (x + x_1) - exp x - x_1 • exp x‖ ≤ ‖exp x‖ * ‖x_1 ^ 2‖
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]
case h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a‖ ^ 2
case h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), a ∈ Metric.ball 0 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a ^ 2‖
simp only [Metric.mem_ball, dist_zero_right, norm_pow]
no goals
case h
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖exp (x + a) - exp x - a • exp x‖ ≤ ‖exp x‖ * ‖a‖ ^ 2
exact fun z hz => exp_bound_sq x z hz.le
no goals
𝕜 : Type ?u.55
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedAlgebra 𝕜 ℂ
x : ℂ
⊢ 1 < 2
norm_num