The normalized Riemann map

The Riemann mapping theorem of RiemannMapping/Existence.lean produces some biholomorphism of a simply connected proper domain onto the unit disc, and RiemannMapping/Uniqueness.lean shows any two such maps differ by a disc automorphism. Neither statement singles out a map. This file adds the classical normalization that does: fixing a base point z₀ ∈ Ω, there is exactly one biholomorphism Ω → 𝔻 with

f z₀ = 0 and deriv f z₀ > 0,

the second condition being an inequality in the scoped order ComplexOrder on ℂ, so that it says precisely that deriv f z₀ is a positive real number. With Ω and z₀ fixed, this pins the Riemann map down on Ω: the maps here are total functions ℂ → ℂ, whose values off Ω no condition constrains, and what is proved is that any two normalized maps agree on Ω — that is, that the biholomorphism Ω → 𝔻 they restrict to is unique.

The argument

Both halves reduce to the existing ones by a rotation.

• Existence. The extremal map of ExtremalFamily.lean is already a bijection onto the disc sending z₀ to 0 (Koebe.lean supplies the surjectivity), and its derivative c at z₀ is nonzero. Multiplying it by the unimodular constant ‖c‖ / c leaves both of those properties intact — rotations preserve the disc — and turns the derivative at z₀ into ‖c‖ > 0.
• Uniqueness. Two normalized maps differ by a rotation u of the disc by TauCeti.exists_eqOn_const_mul_of_image_eq_ball_of_apply_eq_zero. Differentiating at z₀ gives deriv g z₀ = u * deriv f z₀ with both derivatives positive reals of the same modulus, so u = 1 and the two maps agree on Ω.

A note on "normalized"

TauCeti.IsPointedDiscInjectionOn in ExtremalFamily.lean deliberately avoids the word normalized, reserving it for the schlicht-function normalization deriv f z₀ = 1. The normalization used here is the other classical one, the Riemann-map normalization f z₀ = 0, deriv f z₀ > 0 of Ahlfors, Ch. 6 §1: it is the one that is achievable for every domain, since the size of deriv f z₀ is not free once the image is required to be the unit disc.

Main statements

• TauCeti.IsNormalizedRiemannMapOn — the normalization, as a predicate.
• TauCeti.exists_isNormalizedRiemannMapOn — existence of the normalized Riemann map.
• TauCeti.IsNormalizedRiemannMapOn.eqOn — uniqueness: two normalized maps agree on the domain.
• TauCeti.riemannMapping_normalized — the two combined.
• TauCeti.eqOn_id_of_isNormalizedRiemannMapOn_ball — the normalized Riemann map of the disc at the origin is the identity.

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. As with the rest of this development's L0–L3 material, 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.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII §4.

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

A normalized Riemann map of a domain Ω at a base point z₀ ∈ Ω: a holomorphic bijection of Ω onto the open unit disc that sends z₀ to the origin and has a positive real derivative there.

The order on deriv f z₀ is the scoped ComplexOrder one, so 0 < deriv f z₀ unfolds to 0 < (deriv f z₀).re ∧ 0 = (deriv f z₀).im.

This normalization is what makes the Riemann map unique: TauCeti.riemannMapping produces a map only up to a disc automorphism, whereas by TauCeti.riemannMapping_normalized any two functions satisfying the predicate below agree on Ω. Uniqueness can only be uniqueness on Ω, since the predicate says nothing about the values of f outside Ω.

• base_mem : z₀ ∈ Ω

  The base point of a normalized Riemann map lies in its domain, so that the conditions at the base point really do constrain the map on Ω.

• differentiableOn : DifferentiableOn ℂ f Ω

  A normalized Riemann map is holomorphic on its domain.

• bijOn : Set.BijOn f Ω (Metric.ball 0 1)

  A normalized Riemann map is a bijection of its domain onto the open unit disc.

• map_base : f z₀ = 0

  A normalized Riemann map sends the base point to the origin.

• deriv_pos : 0 < deriv f z₀

  A normalized Riemann map has positive real derivative at the base point.

theorem TauCeti.IsNormalizedRiemannMapOn.mapsTo {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : Set.MapsTo f Ω (Metric.ball 0 1)

theorem TauCeti.IsNormalizedRiemannMapOn.injOn {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : Set.InjOn f Ω

theorem TauCeti.IsNormalizedRiemannMapOn.surjOn {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : Set.SurjOn f Ω (Metric.ball 0 1)

theorem TauCeti.IsNormalizedRiemannMapOn.image_eq {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : f '' Ω = Metric.ball 0 1

theorem TauCeti.IsNormalizedRiemannMapOn.isPointedDiscInjectionOn {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : IsPointedDiscInjectionOn f Ω z₀

A normalized Riemann map competes in the extremal family of ExtremalFamily.lean: it is a holomorphic injection into the disc fixing the base point.

theorem TauCeti.IsNormalizedRiemannMapOn.deriv_ne_zero_base {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : deriv f z₀ ≠ 0

theorem TauCeti.IsNormalizedRiemannMapOn.coe_norm_deriv {Ω : Set ℂ} {f : ℂ → ℂ} {z₀ : ℂ} (hf : IsNormalizedRiemannMapOn f Ω z₀) : ↑‖deriv f z₀‖ = deriv f z₀

The derivative of a normalized Riemann map at the base point is its own modulus.

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

Existence of the normalized Riemann map. Every nonempty, simply connected, open, proper subset Ω of ℂ carries, at each of its points z₀, a holomorphic bijection onto the open unit disc sending z₀ to 0 with positive real derivative there.

The extremal map of TauCeti.exists_isMaxOn_norm_deriv_of_hasHolomorphicSquareRoots already fixes the base point and is onto by TauCeti.surjOn_ball_of_isMaxOn; only a rotation is needed to make its derivative positive.

theorem TauCeti.IsNormalizedRiemannMapOn.eqOn {Ω : Set ℂ} {f g : ℂ → ℂ} {z₀ : ℂ} (hg : IsNormalizedRiemannMapOn g Ω z₀) (hf : IsNormalizedRiemannMapOn f Ω z₀) (hΩo : IsOpen Ω) : Set.EqOn g f Ω

Uniqueness of the normalized Riemann map. Two normalized Riemann maps of the same domain at the same base point agree on that domain.

Together with TauCeti.exists_isNormalizedRiemannMapOn this makes the normalized Riemann map a genuinely well-defined function of (Ω, z₀) on Ω: what is determined is the restriction Ω → 𝔻, not the values of a representative off Ω. Note that neither simple connectivity nor properness of Ω is needed here: uniqueness holds wherever two such maps happen to exist.

theorem TauCeti.riemannMapping_normalized {Ω : Set ℂ} {z₀ : ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) (hz₀ : z₀ ∈ Ω) : ∃ (f : ℂ → ℂ), IsNormalizedRiemannMapOn f Ω z₀ ∧ ∀ (g : ℂ → ℂ), IsNormalizedRiemannMapOn g Ω z₀ → Set.EqOn g f Ω

The Riemann mapping theorem, normalized. A nonempty, simply connected, open, proper subset Ω of ℂ with a base point z₀ carries a holomorphic bijection onto the open unit disc that sends z₀ to 0 with positive real derivative there, and that map is unique: any other one agrees with it on Ω.

This is the pinned-down form of TauCeti.riemannMapping, which asserts existence only.

theorem TauCeti.isNormalizedRiemannMapOn_id_ball : IsNormalizedRiemannMapOn id (Metric.ball 0 1) 0

The identity is the normalized Riemann map of the unit disc at the origin.

theorem TauCeti.eqOn_id_of_isNormalizedRiemannMapOn_ball {f : ℂ → ℂ} (hf : IsNormalizedRiemannMapOn f (Metric.ball 0 1) 0) : Set.EqOn f id (Metric.ball 0 1)

Rigidity of the disc. A holomorphic bijection of the open unit disc onto itself that fixes the origin and has positive real derivative there is the identity.

This strengthens TauCeti.eqOn_id_of_leftInvOn_ball_of_map_zero_of_deriv_zero_eq_one, which assumes the derivative at the origin is exactly 1: here it is only assumed to be a positive real, and uniqueness of the normalized Riemann map supplies the rest.