English
For differentiable f,g: ℝ→ℝ and h>0, the derivative of x ↦ f(x)^g(x) is f'(x) g(x) f(x)^{g(x)-1} + g'(x) f(x)^{g(x)} log f(x).
Русский
Пусть f,g: ℝ→ℝ и h>0, то производная функции x ↦ f(x)^{g(x)} равна f'(x) g(x) f(x)^{g(x)-1} + g'(x) f(x)^{g(x)} log f(x).
LaTeX
$$$\\text{If } f,g:\\mathbb{R}\\to\\mathbb{R}\\text{ are differentiable and } f(x)>0,\\\\ \\frac{d}{dx} f(x)^{g(x)}= f'(x)\\, g(x)\\, f(x)^{g(x)-1} + g'(x)\\, f(x)^{g(x)} \\log f(x).$$$
Lean4
theorem _root_.HasStrictDerivAt.rpow {f g : ℝ → ℝ} {f' g' : ℝ} (hf : HasStrictDerivAt f f' x)
(hg : HasStrictDerivAt g g' x) (h : 0 < f x) :
HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x :=
by
convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x (hf.prodMk hg) using 1
simp [mul_assoc, mul_comm]
