English
Under appropriate hypotheses, one has HasFDerivWithinAt for translated arguments and adjusted derivative form.
Русский
При надлежащих условиях существует производная внутри для перенесённых аргументов с корректной формой производной.
LaTeX
$$$\\text{HasFPowerSeriesWithinOnBall } f p s x r \\Rightarrow \\text{HasFDerivWithinAt } f (\\text{adjusted}) (insert x s) (x+y)$$$
Lean4
/-- If a function has a power series on a ball, then so does its derivative. -/
protected theorem fderiv [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) :
HasFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries 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_hasFPowerSeriesOnBall
?_
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.fderiv_eq, add_sub_cancel]
simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz
