English
The derivative of the hpowed function f^n is the sum ∑_{i=0}^{n-1} (f x)^{n−1−i} •> f' <• (f x)^i, expressed in the same operator-sum form as in the standard chain/product rule.
Русский
Производная функции f^n задаётся суммой по i: f(x)^{n−1−i} f'(x) f(x)^i.
LaTeX
$$$\\mathrm{D}\\bigl(f^n\\bigr)(x) = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\; f'(x) \\; f(x)^i$$$
Lean4
theorem fun_pow' (h : HasFDerivAt f f' x) (n : ℕ) :
HasFDerivAt (fun x ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> f' <• f x ^ i) x :=
match n with
| 0 => by simpa using hasFDerivAt_const 1 x
| 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 _ _ _ _
