English
If f,g: domain → ℂ are differentiable at 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:\\text{domain}\\to\\mathbb{C}\\text{ with }f(x)\\in\\mathrm{slitPlane},\\ HasDerivAt\\bigl(x\\mapsto f(x)^{g(x)}\\bigr)= g(x) f(x)^{g(x)-1} f'(x) + f(x)^{g(x)} \\log(f(x)) g'(x).$$$
Lean4
theorem cpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) (h0 : f x ∈ slitPlane) :
HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x := by
simpa only [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt
