iteratedDeriv_const_mul — Mathlib

English

For ContDiffOn, the nth derivative of f composed with negation respects a sign pattern with (−1)^n.

Русский

Для ContDiffOn n-я повторная производная от f(−x) следует знаковому правилу (−1)^n.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\lambda x. f (-x)) x = (-1)^n \\cdot \\operatorname{iteratedDerivWithin}_n f (-x)$$

Lean4

theorem iteratedDeriv_const_mul {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiffAt 𝕜 n f x) (c : 𝕜) :
    iteratedDeriv n (fun z => c * f z) x = c * iteratedDeriv n f x := by
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_const_mul (Set.mem_univ x) uniqueDiffOn_univ c (contDiffWithinAt_univ.mpr h)

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