hasStrictFDerivAt_exp_zero_of_radius_pos

English

If the radius of convergence of the exponential series is positive, then the exponential map has Fréchet derivative equal to the identity at zero.

Русский

При положительном радиусе сходимости ряда экспоненты, экспоненте соответствует производная Фреше в точке 0 равная тождественному отображению.

LaTeX

$$$$ \text{HasFDerivAt}(\exp, 1, 0) \; \text{when radius is positive} $$$$

Lean4

/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has strict Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
theorem hasStrictFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) :
    HasStrictFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
  by
  convert (hasFPowerSeriesAt_exp_zero_of_radius_pos h).hasStrictFDerivAt
  ext x
  change x = expSeries 𝕂 𝔸 1 fun _ => x
  simp [expSeries_apply_eq, Nat.factorial]

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