English
If hf : ContDiff 𝕜 n f, then HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f).
Русский
Пусть f — функция, C^n, тогда ftaylorSeries 𝕜 f является тейлоровой сериейupTo до порядка n.
LaTeX
$$$\operatorname{ContDiff}_{\mathbb{K}}\ n\ f \Rightarrow \operatorname{HasFTaylorSeriesUpTo}\ n\ f\ (ftaylorSeries\ 𝕜\ f)$$$
Lean4
/-- For `n : ℕ∞`, a function is `C^n` iff it admits `ftaylorSeries 𝕜 f`
as a Taylor series up to order `n`. -/
theorem contDiff_iff_ftaylorSeries {n : ℕ∞} : ContDiff 𝕜 n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f) :=
by
constructor
· rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ
· exact fun h ↦ ⟨ftaylorSeries 𝕜 f, h⟩