English
If p(n+k) = 0 for all n, then iteratedFDerivSeries k n = 0 for all n.
Русский
Если p(n+k)=0 для всех n, то iteratedFDerivSeries k n = 0 для всех n.
LaTeX
$$$$\\forall n, p(n+k)=0 \\Rightarrow iteratedFDerivSeries k n = 0.$$$$
Lean4
/-- If a function has a power series on a ball, then so do its iterated derivatives. -/
protected theorem iteratedFDerivWithin (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s) (k : ℕ)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r := by
induction k with
| zero =>
exact
(continuousMultilinearCurryFin0 𝕜 E
F).symm |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
h
| succ k ih =>
rw [iteratedFDerivWithin_succ_eq_comp_left]
apply
(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E)
F).symm |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
(ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)
