English
For a Banach algebra over a field with char zero, in the ball of convergence, exp has Fréchet derivative equal to exp(x) times 1.
Русский
В шаре радиуса сходящности, экспонента имеет производную Фреше равную exp(x) умноженному на единицу.
LaTeX
$$$$ \HasFDerivAt(\exp, \exp(x) \cdot 1, x) \text{ for } x \text{ in ball of convergence} $$$$
Lean4
/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of
characteristic zero has Fréchet derivative `NormedSpace.exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸`
at any point `x`in the disk of convergence. -/
theorem hasFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
HasFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x :=
by
have hpos : 0 < (expSeries 𝕂 𝔸).radius := (zero_le _).trans_lt hx
rw [hasFDerivAt_iff_isLittleO_nhds_zero]
suffices
(fun h => exp 𝕂 x * (exp 𝕂 (0 + h) - exp 𝕂 0 - ContinuousLinearMap.id 𝕂 𝔸 h)) =ᶠ[𝓝 0] fun h =>
exp 𝕂 (x + h) - exp 𝕂 x - exp 𝕂 x • ContinuousLinearMap.id 𝕂 𝔸 h
by
refine (IsLittleO.const_mul_left ?_ _).congr' this (EventuallyEq.refl _ _)
rw [← hasFDerivAt_iff_isLittleO_nhds_zero]
exact hasFDerivAt_exp_zero_of_radius_pos hpos
have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius := EMetric.ball_mem_nhds _ hpos
filter_upwards [this] with _ hh
rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, ContinuousLinearMap.id_apply, smul_eq_mul]
ring
