English
Let f be differentiable with derivative f'. Then the derivative of the map x ↦ f(x)^n is the sum over i = 0,...,n−1 of f(x)^{n−1−i} f' f(x)^i, expressed in the appropriate linear-map form. Equivalently, d(f^n) = ∑_{i=0}^{n-1} f^{n-1-i} (df) f^{i}.
Русский
Пусть f дифференцируема, производная f'; тогда производная функции x ↦ f(x)^n равна сумма по i от 0 до n−1: f(x)^{n−1−i} f'(x) f(x)^i.
LaTeX
$$$\\frac{d}{dx} (f(x))^n = \\sum_{i=0}^{n-1} f(x)^{n-1-i} \\cdot f'(x) \\cdot f(x)^i$$$
Lean4
theorem fun_pow' (h : HasStrictFDerivAt f f' x) (n : ℕ) :
HasStrictFDerivAt (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 hasStrictFDerivAt_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)]
refine this.congr_fderiv <| aux _ _ _ _
