iteratedDeriv_comp_const_smul — Mathlib

English

Within s, the nth derivative of the negated function equals the negation of the nth derivative of the function.

Русский

Внутри s n-я повторная производная от отрицательной функции равна отрицанию n-й повторной производной исходной функции.

LaTeX

$$$\\operatorname{iteratedDerivWithin}_n (\\Pi.neg f) s x = -\\operatorname{iteratedDerivWithin}_n f s x$$$

Lean4

theorem iteratedDeriv_comp_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiff 𝕜 n f) (c : 𝕜) :
    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x) :=
  by
  funext x
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_comp_const_smul (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr h) c
      (Set.mapsTo_univ _ _)

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