fderivWithin_fun_pow — Mathlib

English

Within a set, the derivative of the power map on a ring follows the same Leibniz-type sum with within-derivatives.

Русский

Во множестве производная степенной карты на кольце следует той же сумме Лейбница для внутри-производной.

LaTeX

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

Lean4

theorem fderivWithin_fun_pow (hxs : UniqueDiffWithinAt 𝕜 s x) (n : ℕ) (hf : DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 (fun x ↦ f x ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x :=
  hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs

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