hasFDerivAt_exp — Mathlib

English

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

Русский

Для банаховых алгебр с CharZero экспонента имеет производную Фреше exp(x) • 1 в любой x.

LaTeX

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

Lean4

/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has
Fréchet derivative `NormedSpace.exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
theorem hasFDerivAt_exp {x : 𝔸} : HasFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x :=
  hasStrictFDerivAt_exp.hasFDerivAt

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