English
Iterated Fréchet derivatives are analytic on a neighborhood given initial analyticity, by induction.
Русский
Итеративные Фреше-производные аналитичны на окрестности при базовой аналитичности по индукции.
LaTeX
$$$\\text{AnalyticOnNhd } f s \\Rightarrow \\text{AnalyticOnNhd } (\\text{iteratedFDeriv } 𝕜 n f) s$$$
Lean4
/-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. See also
`AnalyticOnNhd.iteratedFDeriv_of_isOpen`, removing the completeness assumption but requiring the set
to be open. -/
protected theorem iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
AnalyticOnNhd 𝕜 (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_analyticOnNhd h
| succ n
IH =>
rw [iteratedFDeriv_succ_eq_comp_left]
-- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined.
convert ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv
case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm
simp
