hasFDerivWithinAt_pow' — Mathlib

English

Within an algebraic context, HasFDerivWithinAt for the map x ↦ x^n is given by the same sum expression with the respective scalar actions on left and right.

Русский

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

LaTeX

$$$\\text{HasFDerivWithinAt}\\ f f' s x \\Rightarrow \\text{HasFDerivWithinAt}\\ (\\text{pow } f n)\\ (\\text{sum over } i)\\ s x$$$

Lean4

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

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