Hurwitz's theorem

Hurwitz's theorem describes how the zeros of a locally uniform limit of holomorphic functions relate to the zeros of the approximants, and it does so in both directions. The limit acquires no new zeros — a limit of nowhere-vanishing functions is nowhere vanishing or identically zero — and it loses none either: every zero of the limit is approached by zeros of the approximants. This is the second target of layer L0 (the local-mapping engine) of the conformal-mapping roadmap, and the perturbation backbone for the injectivity step of the Riemann mapping theorem.

Both directions come from one Rouché estimate, isolated here as TauCeti.eventually_finsum_analyticOrderNatAt_ball_eq. Fix a disc whose closure lies in Ω and on whose bounding circle the limit g does not vanish. Then ‖g‖ has a positive minimum δ on that circle by compactness, and locally uniform convergence eventually forces ‖g - F i‖ < δ ≤ ‖g‖ there — exactly Rouché's hypothesis. So eventually the zero counts of F i and of g inside the disc agree, an equality of natural numbers from which both halves of Hurwitz's theorem are read off by looking at one side or the other:

• the count of g is 0 whenever the F i are zero-free, and a function whose count vanishes on every such disc has no zeros at all;
• the count of g is positive at an isolated zero of g, so the count of F i is too, and F i has a zero in a disc that can be taken as small as one likes.

The second reading needs the zero of g to be isolated, which is why the identically zero alternative is unavoidable and why Ω is assumed connected: it is the identity theorem that turns "g is not constantly v" into "g ≠ v on a punctured neighbourhood of each point".

Everything is stated for an arbitrary value v, not only for v = 0: applying the above to g - v costs nothing and gives the statement actually used downstream — a value omitted by the F i is omitted by the limit unless the limit is constantly that value. Specialising to v = 0 recovers the classical phrasing TauCeti.hurwitz.

Throughout, every hypothesis on the family — holomorphy, omitting a value, injectivity — is assumed only eventually along l: it holds on some index set belonging to l, not on every index. Along a sequence that reads "for all sufficiently large i", the phrasing the docstrings below use; for a general filter it says only that the indices where the hypothesis fails are excluded by a member of l, whose complement need not be finite. That is the form limit arguments produce and consume, and it costs nothing: the conclusions are eventual along l as well, so indices outside a set of l never enter.

The corollary usually quoted alongside is the injectivity form: a locally uniform limit of injective holomorphic functions is injective or constant. That is the version the Riemann mapping theorem consumes. It is proved from the value form rather than by applying TauCeti.hurwitz to the differences F i - F i b on the punctured domain Ω \ {b}, since that route needs the punctured set to be connected — a fact Mathlib does not currently supply for an open connected subset of ℂ.

Main results

• TauCeti.eventually_finsum_analyticOrderNatAt_ball_eq — Hurwitz's theorem, counting form: on a disc whose bounding circle avoids the zeros of the limit, the approximants eventually have the same number of zeros as the limit, counted with multiplicity.
• TauCeti.hurwitz_eventually_exists_eq — zeros of the limit are limits of zeros: if g is not constantly v and g z₀ = v, then every neighbourhood of z₀ eventually contains a point where F i takes the value v.
• TauCeti.hurwitz_eventually_exists_eq_zero — the same for v = 0.
• TauCeti.hurwitz_forall_ne — a value omitted by the F i is omitted by a limit that is not constantly that value.
• TauCeti.hurwitz_forall_ne_or_forall_eq — the dichotomy form of the previous statement.
• TauCeti.hurwitz — a locally uniform limit of nowhere-vanishing holomorphic functions on a connected open set is nowhere vanishing or identically zero.
• TauCeti.hurwitz_injOn — a locally uniform limit of injective holomorphic functions is injective or constant.

Coordination with upstream Mathlib

Mathlib has no Hurwitz theorem. However, per the Coordination with upstream Mathlib section of ConformalMapping/README.md, this layer overlaps mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which proves this material internally as the private lemmas eqOn_zero_or_forall_ne_zero_of_tendstoLocallyUniformlyOn and eqOn_const_or_injOn_of_tendstoLocallyUniformlyOn. This file is therefore a temporary shim: once the corresponding Mathlib lemmas land, these statements should be backed by them — or deleted and their consumers refactored — rather than maintained as independent re-proofs. What Tau Ceti adds at L0 is named, discoverable API, not first proof.

References

• L. Ahlfors, Complex Analysis, Ch. 5.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII.

theorem TauCeti.eventually_finsum_analyticOrderNatAt_ball_eq {ι : Type u_1} {l : Filter ι} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} {c : ℂ} {r : ℝ} (hr : 0 < r) (hg : AnalyticOnNhd ℂ g (Metric.closedBall c r)) (hF : ∀ᶠ (i : ι) in l, AnalyticOnNhd ℂ (F i) (Metric.closedBall c r)) (hconv : TendstoUniformlyOn F g l (Metric.sphere c r)) (hne : ∀ z ∈ Metric.sphere c r, g z ≠ 0) : ∀ᶠ (i : ι) in l, ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c r), analyticOrderNatAt (F i) z = ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball c r), analyticOrderNatAt g z

Hurwitz's theorem, counting form. Let g and — for all sufficiently large i — the F i be analytic on a closed disc closedBall c r of positive radius, let F i → g uniformly on the bounding circle sphere c r, and let g not vanish on that circle. Then for all sufficiently large i, F i has exactly as many zeros in ball c r as g does, counted with multiplicity.

This is Rouché's theorem TauCeti.rouche applied along the filter: the bound δ ≤ ‖g‖ on the compact circle, from TauCeti.exists_pos_le_norm_of_mem_sphere, is eventually beaten by the uniform error ‖g - F i‖ there. Nothing about an ambient domain enters, so a locally uniform limit on an open Ω feeds this lemma through tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact on any disc with closedBall c r ⊆ Ω, which is how both halves of Hurwitz's theorem below use it.

Those two halves are readings of this one equality, so the hypothesis on the circle is the only genuine constraint: some circle must separate the zero being tracked from the rest of the zero set, and that is exactly what the identity theorem provides when g is not locally constant.

theorem TauCeti.hurwitz_eventually_exists_eq_zero {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hgz₀ : g z₀ = 0) (hnc : ¬∀ z ∈ Ω, g z = 0) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∃ z ∈ Ω ∩ Metric.ball z₀ ε, F i z = 0

Hurwitz's theorem: zeros of the limit are limits of zeros. If g is the locally uniform limit on a connected open Ω of functions F i that are holomorphic for all sufficiently large i, is not identically zero, and vanishes at z₀ ∈ Ω, then every ball about z₀ contains a zero of F i for all sufficiently large i.

The hypothesis that g is not identically zero cannot be dropped: for ι = ℕ and l = atTop, the constant functions F n z = 1 / (n + 1 : ℂ) are holomorphic and nowhere zero and converge locally uniformly to g = 0, which vanishes at every z₀, yet no F n has a zero anywhere.

Note that the ball is not assumed to lie in Ω; the zero produced is located in Ω ∩ ball z₀ ε, which the proof reaches by shrinking ε first.

theorem TauCeti.hurwitz_eventually_exists_eq {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) {v z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hgz₀ : g z₀ = v) (hnc : ¬∀ z ∈ Ω, g z = v) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∃ z ∈ Ω ∩ Metric.ball z₀ ε, F i z = v

Hurwitz's theorem: values of the limit are limits of values. If g is the locally uniform limit on a connected open Ω of functions F i that are holomorphic for all sufficiently large i, is not constantly v, and takes the value v at z₀ ∈ Ω, then every ball about z₀ contains a point where F i takes the value v, again for all sufficiently large i.

This is TauCeti.hurwitz_eventually_exists_eq_zero applied to the translated family F i - v, which converges locally uniformly to g - v. It is the form the injectivity corollary consumes: two disjoint balls about two points where g takes the same value eventually both contain points where F i takes that value, contradicting injectivity of F i.

theorem TauCeti.hurwitz_forall_ne {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) {v : ℂ} (hne : ∀ᶠ (i : ι) in l, ∀ z ∈ Ω, F i z ≠ v) (hnc : ¬∀ z ∈ Ω, g z = v) (z : ℂ) : z ∈ Ω → g z ≠ v

Hurwitz's theorem for an omitted value. If F i is holomorphic on Ω and avoids the value v there for all sufficiently large i, and the locally uniform limit g is not constantly v, then g avoids v as well.

Contrapositive of TauCeti.hurwitz_eventually_exists_eq: a point where g took the value v would force F i to take it too.

theorem TauCeti.hurwitz_forall_ne_or_forall_eq {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) {v : ℂ} (hne : ∀ᶠ (i : ι) in l, ∀ z ∈ Ω, F i z ≠ v) : (∀ z ∈ Ω, g z ≠ v) ∨ ∀ z ∈ Ω, g z = v

Hurwitz's theorem for an omitted value, dichotomy form. On a connected open set, a locally uniform limit of functions that are holomorphic and avoid the value v for all sufficiently large i either avoids v everywhere or is constantly v.

The dichotomy is genuine: for ι = ℕ and l = atTop, the functions F n z = v + 1 / (n + 1 : ℂ) avoid v on any Ω and converge locally uniformly to the constant v.

theorem TauCeti.hurwitz {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) (hne : ∀ᶠ (i : ι) in l, ∀ z ∈ Ω, F i z ≠ 0) : (∀ z ∈ Ω, g z ≠ 0) ∨ ∀ z ∈ Ω, g z = 0

Hurwitz's theorem. On a connected open set, a locally uniform limit of functions that are holomorphic and nowhere zero for all sufficiently large i is itself either nowhere zero or identically zero.

This is the value v = 0 of TauCeti.hurwitz_forall_ne_or_forall_eq. The dichotomy is genuine: for ι = ℕ and l = atTop, the constant functions F n z = 1 / (n + 1 : ℂ) on any Ω converge locally uniformly to 0, so the second alternative cannot be dropped.

theorem TauCeti.hurwitz_injOn {ι : Type u_1} {l : Filter ι} {Ω : Set ℂ} {F : ι → ℂ → ℂ} {g : ℂ → ℂ} [l.NeBot] (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ᶠ (i : ι) in l, DifferentiableOn ℂ (F i) Ω) (hconv : TendstoLocallyUniformlyOn F g l Ω) (hinj : ∀ᶠ (i : ι) in l, Set.InjOn (F i) Ω) : Set.InjOn g Ω ∨ ∃ (v : ℂ), ∀ z ∈ Ω, g z = v

Hurwitz's theorem for injectivity. On a connected open set, a locally uniform limit of functions that are holomorphic and injective for all sufficiently large i is either injective or constant.

This is the form the Riemann mapping theorem consumes: it is what keeps the extremal map injective in the limit. Both alternatives genuinely occur — for ι = ℕ and l = atTop, the injective maps F n z = z / (n + 1 : ℂ) converge locally uniformly to the constant 0.

The proof does not route through TauCeti.hurwitz on the punctured domain Ω \ {b}, which would need that set to be connected — a fact Mathlib does not currently provide for an open connected subset of ℂ. Instead, if g were non-constant with g a = g b for a ≠ b, then TauCeti.hurwitz_eventually_exists_eq places a point where F i takes the single value g a within dist a b / 3 of each of a and b; the triangle inequality separates those two points, contradicting injectivity of F i.