English
If f : E → R has a differentiable derivative within a neighborhood and p is a real exponent, then x ↦ f(x)^p is differentiable with derivative (p f(x)^{p-1}) f'(x) whenever f(x) ≠ 0 or p satisfies the appropriate condition.
Русский
Если функция f : E → R имеет производную внутри области и показатель p — действительное число, то x ↦ f(x)^p дифференцируема, а её производная равна (p f(x)^{p-1}) f'(x) при условии f(x) ≠ 0 или при выполнении соответствующего условия на p.
LaTeX
$$$ \forall f:\,E\to\mathbb{R}, f', x, s, p:\, \text{HasFDerivWithinAt } f f' s x \Rightarrow (f(x) \neq 0 \lor 1 \le p) \Rightarrow \text{HasFDerivWithinAt} \left( x \mapsto f(x)^p \right) \left( (p f(x)^{p-1}) \cdot f' \right) s x $$$
Lean4
@[fun_prop]
theorem rpow_const (hf : HasFDerivAt f f' x) (h : f x ≠ 0 ∨ 1 ≤ p) :
HasFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x :=
(hasDerivAt_rpow_const h).comp_hasFDerivAt x hf
