iteratedFDeriv_comp_sub — Mathlib

English

Equates the value of the Taylor polynomial coefficient with the iterated derivative under the HasFTaylorSeriesUpTo hypothesis.

Русский

Сравнивает значение коэффициента Тейлора и повторную производную при наличии HasFTaylorSeriesUpTo.

LaTeX

$$$\forall h,\ HasFTaylorSeriesUpTo n f p \rightarrow \forall \{m : Nat\}, (m \le n) \Rightarrow p x m = iteratedFDeriv 𝕜 m f x$$$

Lean4

/-- The iterated derivative commutes with subtracting a constant. -/
theorem iteratedFDeriv_comp_sub (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a) := by simp [iteratedFDeriv_comp_sub']

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