English
If f has a finite power series on a ball, then so does its derivative; the changeOrigin map preserves finiteness and maps to the derivative series.
Русский
Если у функции есть конечное разложение в ряд ФПС на шаре, то и для ее производной верно аналогичное разложение; операция смены источника сохраняет конечность и приводит к производной серии.
LaTeX
$$$HasFiniteFPowerSeriesOnBall f p x (n+1) r \Rightarrow HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n r$$$
Lean4
/-- If a function has a finite power series on a ball, then so does its derivative. -/
protected theorem fderiv (h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r) :
HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x n 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_hasFiniteFPowerSeriesOnBall
?_
simpa using ((p.hasFiniteFPowerSeriesOnBall_changeOrigin 1 h.finite).mono h.r_pos le_top).comp_sub x
dsimp only
rw [← h.fderiv_eq, add_sub_cancel]
simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz
