hasFTaylorSeriesUpToOn — Mathlib

English

There exists a HasFTaylorSeriesUpToOn structure on a neighborhood for an analytic function, with coefficients analytic on that neighborhood.

Русский

Существуют коэффициенты Тейлора на окрестности для аналитической функции, аналитичность которых сохраняется на этой окрестности.

LaTeX

$$$\\text{AnalyticOn.hasFTaylorSeriesUpToOn}$$$

Lean4

protected theorem hasFTaylorSeriesUpToOn {n : WithTop ℕ∞} (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s :=
  by
  refine ⟨fun x _hx ↦ rfl, fun m _hm x hx ↦ ?_, fun m _hm x hx ↦ ?_⟩
  · have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt
    rwa [insert_eq_of_mem hx] at this
  · exact (h.iteratedFDerivWithin hu m x hx).continuousWithinAt

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