ftaylorSeries — Mathlib

English

For any ENat n, ContDiff 𝕜 n f is equivalent to HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f).

Русский

Для любого ENat n ContDiff 𝕜 n f эквивалентно HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f).

LaTeX

$$$\operatorname{ContDiff}_{\mathbb{K}}\ n\ f \iff \operatorname{HasFTaylorSeriesUpTo}\ n\ f\ (ftaylorSeries\ 𝕜\ f)$$$

Lean4

/-- When a function is `C^n`, it admits `ftaylorSeries 𝕜 f` as a Taylor series up
to order `n` in `s`. -/
theorem ftaylorSeries (hf : ContDiff 𝕜 n f) : HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f) :=
  by
  simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ] at hf ⊢
  exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

Похожие утверждения