pow' — Mathlib

English

For a differentiable f, the derivative of the map x ↦ f(x)^n is the sum ∑_{i=0}^{n-1} (f x)^{n−1−i} •> f' <• (f x)^i, where f' is the derivative of f at x.

Русский

Для дифференцируемой f производная x ↦ f(x)^n равна сумма по i: f(x)^{n−1−i} f'(x) f(x)^i.

LaTeX

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

Lean4

theorem pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
    HasFDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x :=
  h.fun_pow' n

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