English
If a function f has a power series within a ball around a point, then it is differentiable on the intersection of the ball with the domain.
Русский
Если вокруг точки имеется степенная серия внутри области мячика, то функция дифференцируема на пересечении шара и области определения.
LaTeX
$$$\\text{HasFPowerSeriesWithinOnBall } f p s x r \\Rightarrow \\text{DifferentiableOn } f (\\mathrm{EMetric}\\ hyphen) $$
Lean4
theorem differentiableOn [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r) :
DifferentiableOn 𝕜 f (insert x s ∩ EMetric.ball x r) :=
by
intro y hy
have Z := (h.analyticWithinAt_of_mem hy).differentiableWithinAt
rcases eq_or_ne y x with rfl | hy
· exact Z.mono inter_subset_left
· apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
rw [nhdsWithin_insert_of_ne hy]
exact self_mem_nhdsWithin
