English
If f and g are differentiable at a point x and f(x) ∈ slitPlane, then the derivative of x ↦ f(x)^{g(x)} is g(x) f(x)^{g(x)-1} f'(x) + f(x)^{g(x)} log f(x) g'(x).
Русский
Если 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:\\mathbb{C}\\to\\mathbb{C}\\text{ with }f(x)\\in\\mathrm{slitPlane},\\ HasDerivAt f f' x\\HasDerivAt g g' x\\,\\Rightarrow\\ \\\\ HasDerivAt\\left(x\\mapsto f(x)^{g(x)}\\right)\\left(g(x) f(x)^{g(x)-1} f' + f(x)^{g(x)} \\log(f(x)) g'\\right).$$$
Lean4
theorem cpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h0 : f x ∈ slitPlane) :
HasDerivAt (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 only [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt
