fun_pow' — Mathlib

English

If f is differentiable at x with derivative f', then for any n, HasDerivAt of f^n at x has derivative ∑_{i=0}^{n-1} f(x)^{n-1-i} f' f(x)^i.

Русский

Если f дифференцируема в точке x с производной f', то для любого n производная f(x)^n в точке x равна сумме ∑_{i=0}^{n-1} f(x)^{n-1-i} f' f(x)^i.

LaTeX

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

Lean4

theorem fun_pow' (h : HasDerivAt f f' x) (n : ℕ) :
    HasDerivAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x := by
  simpa using h.hasFDerivAt.pow' n |>.hasDerivAt

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