iteratedFDeriv_comp_sub' — Mathlib

English

The n-th iterated derivative with a right-shift by a constant equals the derivative with the shifted argument.

Русский

Итеративная производная n-го порядка при правом сдвиге на константу равна производной с аргументом, сдвинутым вправо.

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{k}}(n)\ (f\circ (\cdot + a)) = \operatorname{iteratedFDeriv}_{\mathbb{k}}(n)\ f \circ (\cdot + a)$$$

Lean4

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

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