hasStrictFDerivAt_exp — Mathlib

English

For any x in a Banach algebra, exp has strict Frechet derivative exp(x) • 1 at x.

Русский

В любой точке x экспонента имеет строгую производную exp(x) • 1.

LaTeX

$$$$ \HasStrictFDerivAt(\exp, \exp(x) \cdot 1, x) $$$$

Lean4

/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict
Fréchet derivative `NormedSpace.exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
theorem hasStrictFDerivAt_exp {x : 𝔸} : HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x :=
  hasStrictFDerivAt_exp_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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