hasStrictFDerivAt_exp_of_mem_ball

English

In the mem of ball for exp series radius, exp has strict Frechet derivative exp(x) • 1 at x.

Русский

При попадании в шар радиуса ряда экспоненты, экспонента имеет строгую производную экспоненты exp(x) • 1 в x.

LaTeX

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

Lean4

/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of
characteristic zero has strict Fréchet derivative `NormedSpace.exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸`
at any point `x` in the disk of convergence. -/
theorem hasStrictFDerivAt_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasStrictFDerivAt (exp 𝕂) (exp 𝕂 x • (1 : 𝔸 →L[𝕂] 𝔸)) x :=
  let ⟨_, hp⟩ := analyticAt_exp_of_mem_ball x hx
  hp.hasFDerivAt.unique (hasFDerivAt_exp_of_mem_ball hx) ▸ hp.hasStrictFDerivAt

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