contDiff_iff_ftaylorSeries — Mathlib

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⟩

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