iteratedFDeriv_comp_add_left' — 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 {m} (hmn : m ≤ n) (x : E),\ p x m = iteratedFDeriv 𝕜 m f x$$$

Lean4

/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
theorem iteratedFDeriv_comp_add_left' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) = fun x ↦ iteratedFDeriv 𝕜 n f (a + x) := by
  simpa [← iteratedFDerivWithin_univ] using iteratedFDerivWithin_comp_add_left' n a (s := univ)

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