English
If f,g are differentiable within a set s, and f(x) lies in slitPlane, then f(x)^g(x) is differentiable within s with the cpow derivative.
Русский
Если f,g дифференцируемы внутри s и f(x) лежит в slitPlane, то f(x)^g(x) дифференцируемо внутри s с производной cpow.
LaTeX
$$$\\\\forall f,g, DifferentiableWithinAt Complex f s x, DifferentiableWithinAt Complex g s x, f x \\in slitPlane \\\\Rightarrow DifferentiableWithinAt Complex (\\\\lambda x, f(x)^{g(x)}) s x$$$
Lean4
theorem cpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) (h0 : f x ∈ slitPlane) :
HasFDerivWithinAt (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 convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prodMk hg)
