iteratedFDeriv — Mathlib

English

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

Русский

Если существует имеет HasFTaylorSeriesUpTo для f в точке x, тогда p x m равно iteratedFDeriv m f x для m ≤ n.

LaTeX

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

Lean4

/-- If two functions agree in a neighborhood, then so do their iterated derivatives. -/
theorem iteratedFDeriv {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[𝓝 x] f₂) (n : ℕ) :
    iteratedFDeriv 𝕜 n f₁ =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f₂ := by
  simp_all [← nhdsWithin_univ, ← iteratedFDerivWithin_univ, Filter.EventuallyEq.iteratedFDerivWithin]

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