English
If f has a derivative within s at x and g has a derivative within s at x, and f(x) > 0, then the derivative of f^g is given by a product rule with log f.
Русский
Если f и g имеют производные внутри s в x и f(x) > 0, то производная f(x)^{g(x)} задаётся правилом произведения с log f.
LaTeX
$$HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x$$
Lean4
theorem rpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) (h : 0 < f x) :
HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x :=
by
convert (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1
dsimp; ring
