fderiv_pow' — Mathlib

English

For every n, the derivative of the map f^n is the same Leibniz-type sum as above.

Русский

Для каждого n производная отображения f^n совпадает с тем же суммарным выражением.

LaTeX

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

Lean4

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

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