English
If the k-th term of a formal multilinear series is zero, then the k-th iterated derivative series is identically zero.
Русский
Если k-й член ряда формальных многообразий равен нулю, то k-я итеративная производная ряда равна нулю на всём.
LaTeX
$$$$p(n)=0 \\Rightarrow iteratedFDerivWithin 𝕜 n f s x = 0.$$$$
Lean4
/-- Formal multilinear series associated to the iterated derivative, defined by iterating
`p ↦ p.derivSeries` and currying suitably. It is defined so that, if a function has `p` as a power
series, then its iterated derivative of order `k` has `p.iteratedFDerivSeries k` as a power
series. -/
noncomputable def iteratedFDerivSeries (p : FormalMultilinearSeries 𝕜 E F) (k : ℕ) :
FormalMultilinearSeries 𝕜 E (E [×k]→L[𝕜] F) :=
match k with
| 0 =>
(continuousMultilinearCurryFin0 𝕜 E
F).symm |>.toContinuousLinearEquiv.toContinuousLinearMap.compFormalMultilinearSeries
p
| (k + 1) =>
(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E)
F).symm |>.toContinuousLinearEquiv.toContinuousLinearMap.compFormalMultilinearSeries
(p.iteratedFDerivSeries k).derivSeries
