hasFDerivAt_pow' — Mathlib

English

Within a set s, HasFDerivWithinAt for the map f^n is given by the same polynomial-sum expression with the appropriate left/right actions and domain restriction to s.

Русский

В пределах множества HasFDerivWithinAt для x^n задаётся та же сумма с ограничением по s.

LaTeX

$$$\\text{HasFDerivWithinAt}\\ f'^n\\ s x = \\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) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 _ <• x ^ i)
      x :=
  hasFDerivAt_id _ |>.pow' n

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