fderiv_fun_pow — Mathlib

English

Let f be differentiable at x with derivative f'(x); then the derivative of the map x ↦ f(x)^n is the Leibniz sum: D (f^n)(x) = ∑ f(x)^{n-1-i} f'(x) f(x)^i.

Русский

Пусть f дифференцируема в точке x с производной f'(x); тогда производная x ↦ f(x)^n равна сумме Лейбница.

LaTeX

$$$\\mathrm{d}(f^n)(x) = \\sum_{i=0}^{n-1} f(x)^{\,n-1-i} \\; f'(x) \\; f(x)^i.$$$

Lean4

theorem fderiv_fun_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x :=
  hf.hasFDerivAt.pow n |>.fderiv

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