Branches of logarithm and nth root on simply connected domains

In this file we prove that for a function g : X → ℂ defined on a locally path connected space that is continuous on an open simply connected set U and 0 ∉ g '' U, there exist continuous branches of log (g z) and ⁿ√(g z) on U.

theorem Complex.exists_continuousOn_eqOn_exp_comp {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (hUc : IsSimplyConnected U) (hUo : IsOpen U) {g : X → ℂ} (hgc : ContinuousOn g U) (hU₀ : 0 ∉ g '' U) : ∃ (f : X → ℂ), ContinuousOn f U ∧ Set.EqOn (exp ∘ f) g U

If g : X → ℂ defined on a locally path connected space is continuous on an open simply connected set U and 0 ∉ g '' U, then there exists a continuous branch of log ∘ g on U. More precisely, there exists a function f : X → ℂ continuous on U such that exp (f x) = g x for all x ∈ U.

theorem Complex.exists_continuousOn_pow_eq {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (hUc : IsSimplyConnected U) (hUo : IsOpen U) {g : X → ℂ} (hgc : ContinuousOn g U) (hU₀ : 0 ∉ g '' U) {n : ℕ} (hn : n ≠ 0) : ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

If g : X → ℂ defined on a locally path connected space is continuous on an open simply connected set U and 0 ∉ g '' U, then for any n ≠ 0, there exists a continuous branch of ⁿ√g on U. More precisely, there exists a function f : X → ℂ continuous on U such that (f x) ^ n = g x for all x.

theorem Complex.UnitDisc.exists_continuousOn_pow_eq {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (hUc : IsSimplyConnected U) (hUo : IsOpen U) {g : X → UnitDisc} (hgc : ContinuousOn g U) (hU₀ : 0 ∉ g '' U) (n : ℕ+) : ∃ (f : X → UnitDisc), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

If g : X → 𝔻 defined on a locally path connected space is continuous on an open simply connected set U and 0 ∉ g '' U, then for any n ≠ 0, there exists a continuous branch of ⁿ√g on U. More precisely, there exists a function f : X → 𝔻 continuous on U such that (f x) ^ n = g x for all x.