English
The derivative of an analytic function is analytic on the same neighborhood.
Русский
Производная аналитичной функции аналитична на той же окрестности.
LaTeX
$$$\\text{AnalyticOnNhd } f s \\Rightarrow \\text{AnalyticOnNhd } (fderiv 𝕜 f) s$$$
Lean4
/-- If a function is analytic on a neighborhood of a set `s`, then it has a Taylor series given
by the sequence of its derivatives. Note that, if the function were just analytic on `s`, then
one would have to use instead the sequence of derivatives inside the set, as in
`AnalyticOn.hasFTaylorSeriesUpToOn`. -/
theorem hasFTaylorSeriesUpToOn [CompleteSpace F] (n : WithTop ℕ∞) (h : AnalyticOnNhd 𝕜 f s) :
HasFTaylorSeriesUpToOn n f (ftaylorSeries 𝕜 f) s :=
by
refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
· apply HasFDerivAt.hasFDerivWithinAt
exact ((h.iteratedFDeriv m x hx).differentiableAt).hasFDerivAt
· apply (DifferentiableAt.continuousAt (𝕜 := 𝕜) ?_).continuousWithinAt
exact (h.iteratedFDeriv m x hx).differentiableAt
