English
Within a set s, the derivative of the map x ↦ f(x)^n at x is the same polynomial-form sum with f'(x) replaced by the restricted derivative in the ambient space, i.e., HasFDerivWithinAt f f' s x implies HasFDerivWithinAt (f^n) with the same sum structure.
Русский
Внутри множества s производная x ↦ f(x)^n имеет ту же структуру суммы, когда граница производной ограничена множеством s.
LaTeX
$$$\\text{HasFDerivWithinAt}\\ f\\ f'\\ s\\ x \\Rightarrow \\text{HasFDerivWithinAt}\\ (f^n)\\ f'\\ s\\ x$ with the same summation structure as in the global case.$$
Lean4
theorem fun_pow' (h : HasFDerivWithinAt f f' s x) (n : ℕ) :
HasFDerivWithinAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) s x :=
match n with
| 0 => by simpa using hasFDerivWithinAt_const 1 x s
| 1 => by simpa using h
| n + 1 + 1 => by
have := h.mul' (h.fun_pow' (n + 1))
simp_rw [pow_succ' _ (n + 1)]
exact this.congr_fderiv <| aux _ _ _ _
