English
The complex exponential is differentiable everywhere with derivative exp x at a point x.
Русский
Комплексная экспонента дифференцируема повсюду, производная в точке x равна exp(x).
LaTeX
$$$ \\text{HasDerivAt}_{\\mathbb{C}}(\\exp, \\exp(x), x) \\quad \\text{for all } x \\in \\mathbb{C}$$$
Lean4
/-- The complex exponential is everywhere differentiable, with the derivative `exp x`. -/
theorem hasDerivAt_exp (x : ℂ) : HasDerivAt exp (exp x) x :=
by
rw [hasDerivAt_iff_isLittleO_nhds_zero]
have : (1 : ℕ) < 2 := by simp
refine (IsBigO.of_bound ‖exp x‖ ?_).trans_isLittleO (isLittleO_pow_id this)
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]
simp only [Metric.mem_ball, dist_zero_right, norm_pow]
exact fun z hz => exp_bound_sq x z hz.le
