iteratedDeriv_comp_const_mul — Mathlib

English

For f, the nth derivative of f(c x) within s equals c^n times the nth derivative of f at c x.

Русский

Для f n-я повторная производная от f(c x) внутри s равна c^n умножить на n-ю повторную производную f в c x.

LaTeX

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

Lean4

theorem iteratedDeriv_comp_const_mul {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiff 𝕜 n f) (c : 𝕜) :
    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x) := by
  simpa only [smul_eq_mul] using iteratedDeriv_comp_const_smul h c

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