English
If f and g are analytic within a set and f avoids nonpositive reals on that set, then z ↦ f(z)^{g(z)} is analytic within the set.
Русский
Если f и g аналитичны внутри множества и f(z) избегает неотрицательных вещественных значений на этом множестве, то z↦f(z)^{g(z)} аналитична внутри множества.
LaTeX
$$$\\text{AnalyticWithinAt}(\\lambda z: f(z)^{g(z)}, s, x)$ under $f$ analytic and $g$ analytic and $f(x)\\in slitPlane$$$
Lean4
/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/
theorem cpow (fa : AnalyticWithinAt ℂ f s x) (ga : AnalyticWithinAt ℂ g s x) (m : f x ∈ slitPlane) :
AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x :=
by
have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) :=
by
filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
intro z fz
simp only [fz, cpow_def, if_false]
apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e
exact ((fa.clog m).mul ga).cexp
