hasStrictDerivAt_exp — Mathlib

English

Let 𝕂 be either the real or complex numbers and x ∈ 𝕂. Then the exponential map exp: 𝕂 → 𝕂 is differentiable at every point, and its strict derivative at x is exp(x).

Русский

Пусть 𝕂 = ℝ или ℂ и x ∈ 𝕂. Тогда экспонента exp: 𝕂 → 𝕂 дифференцируема в каждой точке, и её строгая производная в точке x равна exp(x).

LaTeX

$$$$ \forall x \in \mathbb{K}, \; \dfrac{d}{dz} e^{z} \Big|_{z=x} = e^{x} \qquad (\mathbb{K} = \mathbb{R} \text{ or } \mathbb{C}). $$$$

Lean4

/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `NormedSpace.exp 𝕂 x`
at any point `x`. -/
theorem hasStrictDerivAt_exp {x : 𝕂} : HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x :=
  hasStrictDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)

Похожие утверждения