hasStrictDerivAt_exp_of_mem_ball — Mathlib

English

If the radius of convergence is positive, exp has strict derivative 1 at zero.

Русский

При положительном радиусе экспонента имеет строгую производную в нуле равную 1.

LaTeX

$$$$ \HasStrictDerivAt(\exp, 1, 0) $$$$

Lean4

/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
`NormedSpace.exp 𝕂 x` at any point `x` in the disk of convergence. -/
theorem hasStrictDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝕂} (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) :
    HasStrictDerivAt (exp 𝕂) (exp 𝕂 x) x := by simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt

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