fderivWithin_fun_pow' — Mathlib

English

For a differentiable f, the derivative of f^n at x is the Leibniz-type sum ∑ f(x)^{n-1-i} f'(x) f(x)^i.

Русский

Для дифференцируемой f производная f^n в точке x равна сумме вида ∑ f(x)^{n-1-i} f'(x) f(x)^i.

LaTeX

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

Lean4

theorem fderivWithin_fun_pow' (hxs : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 (fun x ↦ f x ^ n) s x =
      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i) :=
  hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs

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