The extremal problem of the Riemann mapping theorem

The Riemann mapping theorem is proved by solving an extremal problem: among all holomorphic injections of a domain Ω into the unit disc that send a chosen base point z₀ to the origin, maximize ‖deriv · z₀‖. This file introduces that competing family and shows the maximum is attained.

The sibling file DiscInjection.lean supplies the family's nonemptiness; this file supplies compactness. Together they set up the Koebe square-root argument, which shows that a maximizer cannot omit a value — that step is not in this file.

The argument

Cauchy's estimate on a closed ball inside Ω bounds ‖deriv f z₀‖ by 1 / r uniformly over the family, so the supremum M is finite; it is positive because the family is nonempty and an injective holomorphic map has nonvanishing derivative. Along a maximizing sequence, Montel's selection theorem extracts a locally uniformly convergent subsequence. Its limit g inherits every defining property:

• holomorphy, from Montel;
• g z₀ = 0 and ‖deriv g z₀‖ = M, by passing to the limit pointwise — the derivatives converge locally uniformly too, by the Weierstrass convergence theorem;
• injectivity, from Hurwitz's theorem for injectivity (TauCeti.hurwitz_injOn); the competing alternative, that g is constant, is excluded because ‖deriv g z₀‖ = M > 0;
• mapping into the open disc. This is the one property that does not pass to the limit for free: a locally uniform limit of maps into ball 0 1 a priori only lands in closedBall 0 1. A boundary value would make ‖g‖ attain an interior maximum, so the maximum modulus principle would force ‖g‖ ≡ 1 on Ω, contradicting g z₀ = 0.

Attribution and upstream coordination

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.

Main statements

• TauCeti.IsPointedDiscInjectionOn — membership in the competing family.
• TauCeti.exists_isPointedDiscInjectionOn — the family is nonempty.
• TauCeti.exists_isMaxOn_norm_deriv — the extremal problem has a solution, given one competitor.
• TauCeti.exists_isMaxOn_norm_deriv_of_isSimplyConnected — the form used by the Riemann mapping theorem, where simple connectivity supplies that competitor.

References

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

structure TauCeti.IsPointedDiscInjectionOn (f : ℂ → ℂ) (Ω : Set ℂ) (z₀ : ℂ) : Prop

A pointed disc injection on Ω at the base point z₀: a holomorphic injection of Ω into the open unit disc sending z₀ to the origin. It is the pointed form of the maps produced by TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall in DiscInjection.lean.

Such maps are classically called schlicht, the traditional name for an injective holomorphic map; the name here deliberately avoids normalized, which conventionally demands the further normalization deriv f z₀ = 1 that this predicate does not impose.

This is the competing family of the Riemann mapping theorem's extremal problem: the theorem is proved by maximizing ‖deriv f z₀‖ over all such f.

• differentiableOn : DifferentiableOn ℂ f Ω

  A pointed disc injection is holomorphic on Ω.

• mapsTo : Set.MapsTo f Ω (Metric.ball 0 1)

  A pointed disc injection takes Ω into the open unit disc.

• injOn : Set.InjOn f Ω

  A pointed disc injection is injective on Ω.

• map_base : f z₀ = 0

  A pointed disc injection sends the base point to the origin.

theorem TauCeti.IsPointedDiscInjectionOn.norm_le_one {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsPointedDiscInjectionOn f Ω z₀) {z : ℂ} (hz : z ∈ Ω) : ‖f z‖ ≤ 1

A pointed disc injection is bounded by 1, since it lands in the unit disc.

theorem TauCeti.IsPointedDiscInjectionOn.deriv_ne_zero {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsPointedDiscInjectionOn f Ω z₀) (hΩo : IsOpen Ω) {z : ℂ} (hz : z ∈ Ω) : deriv f z ≠ 0

A pointed disc injection has nonvanishing derivative throughout Ω: it is injective on a neighbourhood of each point, which by the local injectivity criterion forces deriv f z ≠ 0.

theorem TauCeti.exists_isPointedDiscInjectionOn {Ω : Set ℂ} {z₀ : ℂ} (hΩc : IsSimplyConnected Ω) (hΩo : IsOpen Ω) (hΩne : Ω ≠ Set.univ) (hz₀ : z₀ ∈ Ω) : ∃ (f : ℂ → ℂ), IsPointedDiscInjectionOn f Ω z₀

The competing family is nonempty. Every base point of a nonempty, simply connected, open, proper subset of ℂ admits a pointed disc injection.

This repackages TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall_apply_eq_zero.

theorem TauCeti.exists_isMaxOn_norm_deriv {Ω : Set ℂ} {z₀ : ℂ} (hΩo : IsOpen Ω) (hconn : IsPreconnected Ω) (hz₀ : z₀ ∈ Ω) (hne : ∃ (f : ℂ → ℂ), IsPointedDiscInjectionOn f Ω z₀) : ∃ (g : ℂ → ℂ), IsPointedDiscInjectionOn g Ω z₀ ∧ ∀ (f : ℂ → ℂ), IsPointedDiscInjectionOn f Ω z₀ → ‖deriv f z₀‖ ≤ ‖deriv g z₀‖

The extremal problem has a solution. If the competing family at a base point z₀ of an open preconnected set Ω is nonempty, then some member maximizes ‖deriv · z₀‖ over the whole family.

The compactness argument needs nothing beyond these hypotheses: preconnectedness for the maximum modulus principle and for Hurwitz's theorem, and one competitor to make the supremum positive. Simple connectivity enters only through TauCeti.exists_isPointedDiscInjectionOn, which supplies that competitor; see the corollary TauCeti.exists_isMaxOn_norm_deriv_of_isSimplyConnected.

This is the compactness half of the Riemann mapping theorem. It does not assert that the maximizer is surjective; that is the Koebe square-root argument, proved elsewhere.

theorem TauCeti.exists_isMaxOn_norm_deriv_of_isSimplyConnected {Ω : Set ℂ} {z₀ : ℂ} (hΩc : IsSimplyConnected Ω) (hΩo : IsOpen Ω) (hΩne : Ω ≠ Set.univ) (hz₀ : z₀ ∈ Ω) : ∃ (g : ℂ → ℂ), IsPointedDiscInjectionOn g Ω z₀ ∧ ∀ (f : ℂ → ℂ), IsPointedDiscInjectionOn f Ω z₀ → ‖deriv f z₀‖ ≤ ‖deriv g z₀‖

The extremal problem has a solution on a simply connected proper subdomain. This is the form the Riemann mapping theorem uses: on a nonempty, simply connected, open, proper subset Ω of ℂ with base point z₀, some pointed disc injection maximizes ‖deriv · z₀‖.

Simple connectivity and properness serve only to produce one competitor; the compactness argument itself is TauCeti.exists_isMaxOn_norm_deriv.