pow' — Mathlib

English

In a normed algebra, for any differentiable f, the derivative of f^n at x is the sum over i = 0,...,n−1 of (f(x))^{n−1−i} (f'(x)) (f(x))^{i}, represented as a derivative of the hPow map.

Русский

В нормированной алгебре производная f^n в точке x равна сумме по i от 0 до n−1: 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 : HasStrictFDerivAt f f' x) (n : ℕ) :
    HasStrictFDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
  h.fun_pow' n

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