hasFDerivAt_pow — Mathlib

English

If f is differentiable with derivative f', then f^n is differentiable with derivative given by the Leibniz sum.

Русский

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

LaTeX

$$$\\text{HasFDerivAt}_{\\mathbb{K}}(f^n)\\big(x\\big) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; f'(x) \\; f(x)^i.$$$

Lean4

theorem hasFDerivAt_pow (n : ℕ) {x : 𝔸} :
    HasFDerivAt (𝕜 := 𝕜) (fun x : 𝔸 ↦ x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x :=
  hasFDerivAt_id _ |>.pow n

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