English
If a function is analytic in a neighborhood, then its derivative within the neighborhood is analytic there as well.
Русский
Если функция аналитична в окрестности, её внутренняя производная также аналитична на ней.
LaTeX
$$$\\text{AnalyticOnNhd } f s \\Rightarrow \\text{AnalyticOnNhd } (fderivWithin 𝕜 f s) s$$$
Lean4
/-- If a function has a power series within a set on a ball, then so does its derivative. Version
assuming that the function is analytic on `s`. For a version without this assumption but requiring
that `F` is complete, see `HasFPowerSeriesWithinOnBall.fderivWithin_of_mem`. -/
protected theorem fderivWithin_of_mem_of_analyticOn (hr : HasFPowerSeriesWithinOnBall f p s x r) (h : AnalyticOn 𝕜 f s)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r :=
by
refine ⟨hr.r_le.trans p.radius_le_radius_derivSeries, hr.r_pos, fun {y} hy h'y ↦ ?_⟩
apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_zero_eq_enorm] using h'y) hy
· rw [insert_eq_of_mem hx] at hy ⊢
apply DifferentiableWithinAt.hasFDerivWithinAt
exact h.differentiableOn _ hy
· rwa [insert_eq_of_mem hx]
