hasStrictFDerivAt_pow' — Mathlib

English

For a differentiable f and natural n, the derivative of instHPow.hPow f n can be written as a sum ∑_{i=0}^{n−1} (f x)^{n−1−i} •> f' <• (f x)^i, expressed in the same product-rule style as above.

Русский

Для дифференцируемой функции f и натурального n производная instHPow.hPow f n равна сумме по i: f(x)^{n−1−i} f'(x) f(x)^i.

LaTeX

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

Lean4

theorem hasStrictFDerivAt_pow' (n : ℕ) {x : 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ x ^ n)
      (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i) x :=
  hasStrictFDerivAt_id _ |>.pow' n

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