fderiv — Mathlib

English

Iterating the Fréchet derivative is analytic on a neighborhood and preserves differentiability structure.

Русский

Повторение Фреше-производной сохраняет аналитичность на окрестности и структуру дифференцируемости.

LaTeX

$$$\\text{AnalyticOnNhd } f s \\Rightarrow \\text{AnalyticOnNhd } (\\text{iteratedFDeriv } 𝕜 n f) s$$$

Lean4

/-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/
@[fun_prop]
protected theorem fderiv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (fderiv 𝕜 f) x :=
  by
  rcases h with ⟨p, r, hp⟩
  exact hp.fderiv.analyticAt

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