English
Equality between fderivWithin and the shifted first coefficient holds under unique differentiability assumptions.
Русский
Справедливость равенства fderivWithin и сдвинутого первого коэффициента при уникальности дифференцирования.
LaTeX
$$$fderivWithin 𝕜 f (insert x s) (x+y) = \\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p.changeOrigin y 1)$$$
Lean4
/-- If a function has a power series within a set on a ball, then so does its derivative. -/
protected theorem fderivWithin [CompleteSpace F] (h : HasFPowerSeriesWithinOnBall f p s x r)
(hu : UniqueDiffOn 𝕜 (insert x s)) :
HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r :=
by
refine .congr' (f := fun z ↦ continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin (z - x) 1)) ?_ (fun z hz ↦ ?_)
· refine
continuousMultilinearCurryFin1 𝕜 E
F |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
?_
apply HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall
simpa using ((p.hasFPowerSeriesOnBall_changeOrigin 1 (h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x
· dsimp only
rw [← h.fderivWithin_eq _ _ hu, add_sub_cancel]
· simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz.2
· simpa using hz.1
