English
If f differentiable within s at x, then the derivative of x ↦ f(x)^n within s at x equals ∑_{i=0}^{n-1} f(x)^{n-1-i} (derivWithin f s x) f(x)^i.
Русский
Если f дифференцируема внутри s в точке x, то производная x ↦ f(x)^n внутри s в x равна ∑_{i=0}^{n-1} f(x)^{n-1-i} (derivWithin f s x) f(x)^i.
LaTeX
$$$$\\frac{d}{dx}\\bigl(f(x)^n\\bigr)\\Big|_{x}\\;\\text{within } s = \\sum_{i=0}^{n-1} f(x)^{\,n-1-i}\\, (\\operatorname{derivWithin} f\\, s\\ x)\\, f(x)^{\,i}. $$$$
Lean4
@[simp low]
theorem derivWithin_fun_pow' (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
derivWithin (fun x => f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (h.hasDerivWithinAt.pow' n).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
