English
If f,g: domain → ℂ have strict derivatives f' and g' at x and f(x) lies in the slit plane, then the derivative of x ↦ f(x)^{g(x)} is given by the usual product-and-log rule: g(x) f(x)^{g(x)-1} f'(x) + f(x)^{g(x)} log(f(x)) g'(x).
Русский
Пусть f,g: область → ℂ имеют строгие производные f' и g' в точке x и f(x) лежит в slitPlane. Тогда производная функции x ↦ f(x)^{g(x)} равна g(x) f(x)^{g(x)-1} f'(x) + f(x)^{g(x)} log(f(x)) g'(x).
LaTeX
$$$\\text{If }f,g:\\text{dom}\\to\\mathbb{C}\\text{ with strict derivatives }f',g'\\text{ at }x\\text{ and }f(x)\\in\\mathrm{slitPlane},\\\\ (f,g\\mapsto f^{g})' (x)= g(x) f(x)^{g(x)-1} f'(x) + f(x)^{g(x)} \\log(f(x)) g'(x).$$$
Lean4
nonrec theorem cpow (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) (h0 : f x ∈ slitPlane) :
HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x := by
simpa using (hf.cpow hg h0).hasStrictDerivAt
