English
From analytic on nhd, one obtains a Taylor series expansion up to any order on a neighborhood with analytic coefficients.
Русский
Из аналитичности на окрестности следует разложение по Тейлору до любой степени на окрестности с аналитическими коэффициентами.
LaTeX
$$$\\text{AnalyticOn hasFTaylorSeriesUpToOn}$$$
Lean4
/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative within this
set. Note that this theorem does not require completeness of the space. -/
protected theorem iteratedFDerivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) (n : ℕ) :
AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s := by
induction n with
| zero =>
rw [iteratedFDerivWithin_zero_eq_comp]
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F) |>.comp_analyticOn h
| succ n IH =>
rw [iteratedFDerivWithin_succ_eq_comp_left]
apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
apply LinearIsometryEquiv.analyticOnNhd
