English
If a function is polynomial on a set, then so are its successive Fréchet derivatives.
Русский
Если функция полиномальна на множестве, то ее последовательные производные Фреше также полиномальны.
LaTeX
$$$\text{CPolynomialOn } 𝕜 f s \Rightarrow \forall n, \text{CPolynomialOn } 𝕜 (\text{iteratedFDeriv } 𝕜 n f) s$$$
Lean4
/-- If a function is polynomial on a set `s`, so are its successive Fréchet derivative. -/
theorem iteratedFDeriv (h : CPolynomialOn 𝕜 f s) (n : ℕ) : CPolynomialOn 𝕜 (iteratedFDeriv 𝕜 n f) s := by
induction n with
| zero =>
rw [iteratedFDeriv_zero_eq_comp]
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F).comp_cpolynomialOn h
| succ n IH =>
rw [iteratedFDeriv_succ_eq_comp_left]
convert ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
simp
