pow — Mathlib

English

Within a set s, the derivative of f^n is the same Leibniz-type sum with inner derivatives: f(x)^i times f'(x) times f(x)^{n-1-i}.

Русский

Внутри множества f^n имеет ту же сумму Лейбница с внутренними производными.

LaTeX

$$$fderivWithin_{\\mathbb{K}}(f^n)(s,x) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; fderivWithin_{\\mathbb{K}}f(s,x) \\; f(x)^i.$$$

Lean4

theorem pow (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
    HasFDerivWithinAt (fun x ↦ f x ^ n) ((n • f x ^ (n - 1)) • f') s x :=
  h.pow' n |>.congr_fderiv <| aux_sum_eq_pow _

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