fderiv_fun_pow' — Mathlib

English

Let f be differentiable. Then for every n, the derivative of the map x ↦ f(x)^n is given by a Leibniz-type sum: f'(x) is inserted between powers of f(x).

Русский

Пусть f дифференцируема. Тогда для каждого n производная x ↦ f(x)^n задаётся суммой вида: f'(x) вставляется между множителями f(x)^{k}.

LaTeX

$$$f'(x^n) = \\sum_{i=0}^{n-1} f(x)^{\,n-1-i} \\, f'(x) \\, f(x)^i \quad\\text{where } f'(x) \\text{ is the derivative of } f.$$$

Lean4

theorem fderiv_fun_pow' (n : ℕ) (hf : DifferentiableAt 𝕜 f x) :
    fderiv 𝕜 (fun x ↦ f x ^ n) x = (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i) :=
  hf.hasFDerivAt.pow' n |>.fderiv

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