English
If a function has a power series within a ball around x, then it is differentiable on the ball.
Русский
Если функция имеет степенную серию в шаре вокруг точки x, она дифференцируема на шаре.
LaTeX
$$$\\text{HasFPowerSeriesOnBall } f p x r \\Rightarrow \\text{DifferentiableOn } f (EMetric.ball x r)$$$
Lean4
/-- If a function has a power series within a set on a ball, then so does its derivative. For a
version without completeness, but assuming that the function is analytic on the set `s`, see
`HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn`. -/
protected theorem fderivWithin_of_mem [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r)
(hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r :=
by
have : insert x s = s := insert_eq_of_mem hx
rw [← this] at hu
convert h.fderivWithin hu
exact this.symm
