eq_iteratedFDeriv — Mathlib

English

If HasFTaylorSeriesUpTo n f p holds, then for any m with m ≤ n, p x m equals iteratedFDeriv m f x.

Русский

Если HasFTaylorSeriesUpTo n f p выполняется, то для любого m ≤ n, p x m равно iteratedFDeriv m f x.

LaTeX

$$$\forall n,\ HasFTaylorSeriesUpTo\ n\ f\ p \Rightarrow \forall x,\forall m\le n,\ p\ x\ m = \operatorname{iteratedFDeriv}_{\mathbb{k}}\; m\ f\ x$$$

Lean4

theorem eq_iteratedFDeriv (h : HasFTaylorSeriesUpTo n f p) {m : ℕ} (hmn : m ≤ n) (x : E) :
    p x m = iteratedFDeriv 𝕜 m f x := by
  rw [← iteratedFDerivWithin_univ]
  rw [← hasFTaylorSeriesUpToOn_univ_iff] at h
  exact h.eq_iteratedFDerivWithin_of_uniqueDiffOn hmn uniqueDiffOn_univ (mem_univ _)

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