fderiv_pow — Mathlib

English

For any differentiable f, the derivative of f^n is the Leibniz sum above.

Русский

Для любой дифференцируемой f производная f^n — та самая сумма Лейбница.

LaTeX

$$$\\forall f,\\ (\\text{Differentiable}_{\\mathbb{K}} f)\\Rightarrow \\forall n\\in\\mathbb{N},\\ \\mathrm{fderiv}(f^n)(x) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; f'(x) \\; f(x)^i.$$$

Lean4

theorem fderiv_pow (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (fun x ↦ f x ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x :=
  fderiv_fun_pow n hf

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