hasFDerivAt_exp_zero_of_radius_pos

English

Same as HasFDerivAt_exp_zero_of_radius_pos: the Frechet derivative of exp at zero is the identity, under convergence radius condition.

Русский

То же, что и HasFDerivAt_exp_zero_of_radius_pos: производная экспоненты в нуле равна тождественному отображению при условии накопления радиуса.

LaTeX

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

Lean4

/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
theorem hasFDerivAt_exp_zero_of_radius_pos (h : 0 < (expSeries 𝕂 𝔸).radius) : HasFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
  (hasStrictFDerivAt_exp_zero_of_radius_pos h).hasFDerivAt

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