Holomorphic branches of log and of n-th roots on a simply connected domain

Mathlib's Complex.exists_continuousOn_eqOn_exp_comp produces a continuous branch of log ∘ g on a simply connected open set. The Riemann-mapping argument needs a holomorphic one. This file supplies that upgrade for the logarithm, consuming Mathlib's branch rather than rebuilding it, and then obtains the n-th root from it directly as exp (L / n).

Note that the root branch is not an upgrade of Mathlib's Complex.exists_continuousOn_pow_eq, which this file does not use: once the logarithm branch is holomorphic, exp (L / n) is holomorphic by composition and satisfies (exp (L / n)) ^ n = exp L = g outright, so routing through a separate continuous root branch would add a second continuity-to-holomorphy argument for no gain.

The upgrade is local and purely formal. Near a point z₀, the continuous branch L agrees with logBranch w₀ ∘ g where w₀ = L z₀, the branch of the logarithm based at w₀: that composite is holomorphic (the argument sits near 1, inside the slit plane, where Complex.log is), and it agrees with L because continuity of L confines L z - w₀ to the strip |im| < π on which that branch inverts Complex.exp. So no new analysis is involved — only the observation that a continuous logarithm of a holomorphic nonvanishing function is automatically holomorphic.

Attribution and upstream coordination

The mathematics here is an upgrade of prior Mathlib work, not a first proof. The logarithm and zero-free root branches rest on two efforts of Yury Kudryashov's; the germ statement rests in addition on Mathlib's order-of-vanishing formalization.

The branch itself is Mathlib's: Complex.exists_continuousOn_eqOn_exp_comp in Mathlib.Analysis.Complex.BranchLogRoot (© Yury Kudryashov) supplies the continuous logarithm branch on a simply connected domain, which this file consumes rather than rebuilds. What TauCeti.exists_differentiableOn_eqOn_exp_comp and TauCeti.exists_differentiableOn_pow_eq add to it is the continuity-to-holomorphy upgrade. The n-th root is not obtained from Mathlib's continuous root API (Complex.exists_continuousOn_pow_eq is never used here): it is derived as exp (L / n) from the upgraded holomorphic logarithm branch L.

The order of vanishing is Mathlib's too: Mathlib.Analysis.Analytic.Order (© Vincent Beffara; authors Vincent Beffara and Stefan Kebekus) formalizes analyticOrderAt and the factorization theory around it, on which TauCeti.exists_eventuallyEq_pow_iff_dvd rests throughout. AnalyticAt.analyticOrderAt_eq_natCast supplies the factorization of a germ of finite order, analyticOrderAt_eq_top identifies the germ of order ⊤ as the one vanishing near z₀, and analyticOrderAt_pow gives the converse direction outright. What is added here is only the assembly of those with the root branch above.

The consumer is the Riemann mapping construction in Mathlib.Analysis.Complex.RiemannMapping (© Yury Kudryashov), whose Complex.exists_mapsTo_unitBall_injOn_deriv_ne_zero performs the same square-root step that the sibling file DiscInjection.lean re-derives on top of this API; see its docstring for why that lemma cannot be named by an importer.

The Riemann mapping theorem is being formalized upstream at mathlib4#33505, which proves holomorphic log / n-th-root statements (exists_branch_log, exists_branch_nthRoot) internally, as private lemmas, alongside the argument principle, Hurwitz and Montel. The ConformalMapping roadmap's stated contribution at these layers is therefore named, reusable API rather than first proof. Accordingly the two branch declarations here are a temporary shim: when the human-curated Mathlib versions land, those should be deleted and every downstream consumer refactored onto them. That does not extend to TauCeti.exists_eventuallyEq_pow_iff_dvd: the upstream statements are zero-free, like the ones they replace, so they do not subsume a germ that vanishes.

Roots of a germ that vanishes

The root branch needs g to be zero-free, so on its own it says nothing about a germ that vanishes. Locally that gap closes by factoring the zero out: A z = (z - z₀) ^ m • g z with g z₀ ≠ 0, so an n-th root of the germ exists exactly when n divides its order of vanishing (TauCeti.exists_eventuallyEq_pow_iff_dvd), namely (z - z₀) ^ (m / n) times the branch above applied to g. This weakens the zero-free hypothesis — the case of order 0 — to the divisibility condition, and the converse direction shows the condition is sharp. The germ that vanishes identically near z₀, of order ⊤, is its own n-th root.

Main statements

• TauCeti.exists_differentiableOn_eqOn_exp_comp — a holomorphic branch of log ∘ g.
• TauCeti.exists_differentiableOn_pow_eq — a holomorphic branch of ⁿ√g.
• TauCeti.exists_eventuallyEq_pow_iff_dvd — a holomorphic germ has a holomorphic n-th root iff n divides its order of vanishing.
• TauCeti.deriv_eq_logDeriv_of_eqOn_exp_comp — the derivative of a branch of the logarithm is the logarithmic derivative, and so does not depend on which branch was chosen.

theorem TauCeti.exists_differentiableOn_eqOn_exp_comp {U : Set ℂ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (hU₀ : 0 ∉ g '' U) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.EqOn (Complex.exp ∘ f) g U

A holomorphic branch of log ∘ g on a simply connected domain. If g is holomorphic and nowhere zero on a simply connected open U ⊆ ℂ, there is a holomorphic f on U with exp ∘ f = g. Mathlib's Complex.exists_continuousOn_eqOn_exp_comp supplies the branch; only its holomorphy is added here.

theorem TauCeti.exists_differentiableOn_pow_eq {U : Set ℂ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g U) (hU₀ : 0 ∉ g '' U) {n : ℕ} (hn : n ≠ 0) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.EqOn (fun (z : ℂ) => f z ^ n) g U

A holomorphic n-th root on a simply connected domain. The Koebe square-root step of the Riemann mapping theorem is the case n = 2.

theorem TauCeti.exists_eventuallyEq_pow_iff_dvd {A : ℂ → ℂ} {z₀ : ℂ} {n : ℕ} (hA : AnalyticAt ℂ A z₀) (hn : n ≠ 0) : (∃ (ψ : ℂ → ℂ), AnalyticAt ℂ ψ z₀ ∧ ∀ᶠ (z : ℂ) in nhds z₀, A z = ψ z ^ n) ↔ ↑n ∣ analyticOrderAt A z₀

When a holomorphic germ has a holomorphic n-th root: exactly when n divides its order of vanishing. This weakens the zero-free hypothesis of TauCeti.exists_differentiableOn_pow_eq, which is the case of order 0, to the divisibility condition, and records that the condition is sharp. A germ of order ⊤, one vanishing identically near z₀, is included: n ≠ 0 divides ⊤.

theorem TauCeti.deriv_eq_logDeriv_of_eqOn_exp_comp {U : Set ℂ} (hUo : IsOpen U) {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (h : Set.EqOn (Complex.exp ∘ f) g U) {z : ℂ} (hz : z ∈ U) : deriv f z = logDeriv g z

The derivative of a branch is the logarithmic derivative. Wherever a holomorphic f satisfies exp ∘ f = g on an open set, f' = g' / g there. This is what makes a branch of the logarithm useful even though exp determines it only up to 2πi ℤ: the ambiguity is a locally constant additive one, so it disappears on differentiating.