The Koebe square-root step #

The Riemann mapping theorem is proved by maximizing ‖deriv f z₀‖ over the holomorphic injections of a domain into the unit disc that fix a base point. Compactness (ExtremalFamily.lean) produces a maximizer; this file supplies the other half: a maximizer cannot omit a value of the disc.

The engine is a statement about the disc alone: a proper open subset of the unit disc containing the origin and having holomorphic square roots admits a holomorphic injection back into the disc that fixes the origin and has derivative of norm exceeding 1 there — no proper subdomain is extremal. Simple connectivity enters this step only through the square roots (IsSimplyConnected.hasHolomorphicSquareRoots), and it enters the Riemann mapping theorem only through them and through connectedness.

The construction #

Let U be such a subdomain and pick a ∈ ball 0 1 \ U; write μ c for the Möbius factor z ↦ (z - c) / (1 - conj c * z) of Conformal/Moebius.lean. Since μ a does not vanish on U, it has a holomorphic square root h there. Put b := h 0, so b ^ 2 = μ a 0 = -a, and set

f := μ b ∘ h, the improved map;
G := μ (-a) ∘ (· ^ 2) ∘ μ (-b), an automorphism followed by squaring followed by an automorphism.

Why the derivative grows #

Not by computing deriv f 0. The four steps are:

G ∘ f is the identity on U, by pure algebra: the Möbius factors cancel in pairs and the square meets h ^ 2 = μ a. This also gives InjOn f U for free, G being a left inverse.
G is not injective on the disc: it squares after an automorphism, so μ b u and μ b (-u) collide for any nonzero u in the disc — the proof uses u = 1/2.
Hence ‖deriv G 0‖ < 1, by the strict Schwarz lemma of Conformal/Schwarz.lean: Schwarz gives ≤ 1, and equality would make G affine, hence injective.
Differentiating G ∘ f = id at 0 gives deriv G 0 * deriv f 0 = 1.

Together ‖deriv G 0‖ * ‖deriv f 0‖ = 1 with ‖deriv G 0‖ < 1 forces 1 < ‖deriv f 0‖. This is the route a lecturer takes, and it is also the cheaper one to formalize: the only chain rule used is the one on an identity, and no field_simp over the Möbius denominators is needed.

Main statements #

TauCeti.exists_isPointedDiscInjectionOn_one_lt_norm_deriv — a proper subdomain of the disc with holomorphic square roots expands.
TauCeti.surjOn_ball_of_isMaxOn — an extremal pointed disc injection is surjective onto the disc.

Coordination with upstream Mathlib #

The Riemann mapping theorem is being formalized upstream at mathlib4#33505, which proves the L0–L3 prerequisites internally as private lemmas. The declarations here are an explicitly temporary shim: delete them and refactor downstream consumers onto the exported Mathlib versions once those land.

References #

L. Ahlfors, Complex Analysis, Ch. 6 §1.2.
J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII §4.

source

theorem TauCeti.exists_isPointedDiscInjectionOn_one_lt_norm_deriv {U : Set ℂ} (hUo : IsOpen U) (hUs : HasHolomorphicSquareRoots U) (hU₀ : 0 ∈ U) (hUd : U ⊆ Metric.ball 0 1) (hUne : U ≠ Metric.ball 0 1) :

∃ (f : ℂ → ℂ), IsPointedDiscInjectionOn f U 0 ∧ 1 < ‖deriv f 0‖

A proper subdomain of the disc with holomorphic square roots expands. If U is an open proper subset of the unit disc with 0 ∈ U on which nowhere-zero holomorphic functions have holomorphic square roots — for instance a simply connected one — then there is a holomorphic injection of U into the disc fixing the origin whose derivative there has norm exceeding 1.

This is the engine of the Riemann mapping theorem: no proper subdomain can be extremal.

source

theorem TauCeti.surjOn_ball_of_isMaxOn {Ω : Set ℂ} (hΩo : IsOpen Ω) (hΩs : HasHolomorphicSquareRoots Ω) {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) {g : ℂ → ℂ} (hg : IsPointedDiscInjectionOn g Ω z₀) (hmax : ∀ (f : ℂ → ℂ), IsPointedDiscInjectionOn f Ω z₀ → ‖deriv f z₀‖ ≤ ‖deriv g z₀‖) :

Set.SurjOn g Ω (Metric.ball 0 1)

An extremal pointed disc injection is surjective onto the disc. If Ω is open with holomorphic square roots — for instance simply connected — and g maximizes ‖deriv · z₀‖ over the holomorphic injections of Ω into the disc fixing z₀, then g omits no value of the disc.

Otherwise U := g '' Ω would be an open proper subdomain of the disc containing 0 and, as an injective holomorphic image of Ω, having holomorphic square roots; composing g with the map that TauCeti.exists_isPointedDiscInjectionOn_one_lt_norm_deriv produces on U would beat g.