fderivWithin_pow' — Mathlib

English

If f is differentiable, then the derivative of f^n is the same Leibniz-type sum as above.

Русский

Если f дифференцируема, то производная f^n имеет ту же сумму Лейбница.

LaTeX

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

Lean4

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

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