The Riemann map of a Jordan domain on the closed upper half-plane

Carathéodory's theorem extends the Riemann map of a Jordan domain to a homeomorphism from the closed unit disc onto the closure of the domain. This file applies the generic closed-disc to upper-half-plane transport to that map.

Main statement

• TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_frontier: the Riemann map of a Jordan domain, normalized to send infinity to a prescribed boundary point, as a continuous injection of the closed upper half-plane.
• TauCeti.exists_injective_forall_eq_of_surjOn_im_eq_zero: distinct real prevertices of distinct points of the image of the real line.
• TauCeti.exists_prevertices_of_isJordanCurve_frontier: a Carathéodory map of a bounded Jordan domain with real prevertices mapping to prescribed frontier points.

References

• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Springer, 1992, Ch. 2.

theorem TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_frontier {Ω : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hΩJ : IsJordanCurve (frontier Ω)) {p : ℂ} (hp : p ∈ frontier Ω) : ∃ (f : ℂ → ℂ), ContinuousOn f {z : ℂ | 0 ≤ z.im} ∧ DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet ∧ Set.BijOn f UpperHalfPlane.upperHalfPlaneSet Ω ∧ Set.BijOn f {z : ℂ | 0 ≤ z.im} (closure Ω \ {p}) ∧ Set.BijOn f {z : ℂ | z.im = 0} (frontier Ω \ {p}) ∧ Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (nhds p)

Carathéodory's theorem on the closed upper half-plane. Let Ω be a bounded, connected open subset of ℂ whose frontier is a Jordan curve, and let p be a point of that frontier. Then there is a map which is continuous on the closed upper half-plane, holomorphic on the open upper half-plane, a bijection from the open upper half-plane onto Ω, from the closed upper half-plane onto closure Ω with p removed and from the real line onto frontier Ω with p removed, and which tends to p at infinity within the closed half-plane.

theorem TauCeti.exists_injective_forall_eq_of_surjOn_im_eq_zero {ι : Type u_1} {f : ℂ → ℂ} {T : Set ℂ} (hf : Set.SurjOn f {z : ℂ | z.im = 0} T) {v : ι → ℂ} (hv : Function.Injective v) (hvT : ∀ (i : ι), v i ∈ T) : ∃ (a : ι → ℝ), Function.Injective a ∧ ∀ (i : ι), f ↑(a i) = v i

Real prevertices: if f maps the real line surjectively onto a set T, then distinct points v i of T are the images f (a i) of distinct real numbers a i.

theorem TauCeti.exists_prevertices_of_isJordanCurve_frontier {ι : Type u_1} [Finite ι] {U : Set ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hUb : Bornology.IsBounded U) (hUJ : IsJordanCurve (frontier U)) {v : ι → ℂ} (hv : Function.Injective v) (hvU : ∀ (i : ι), v i ∈ frontier U) : ∃ (f : ℂ → ℂ) (a : ι → ℝ) (p : ℂ), Function.Injective a ∧ DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet ∧ ContinuousOn f {z : ℂ | 0 ≤ z.im} ∧ Set.InjOn f {z : ℂ | 0 ≤ z.im} ∧ Set.BijOn f UpperHalfPlane.upperHalfPlaneSet U ∧ (∀ (i : ι), f ↑(a i) = v i) ∧ Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (nhds p) ∧ p ∉ f '' {z : ℂ | 0 ≤ z.im}

A Carathéodory map of the upper half-plane onto a bounded Jordan domain, sending infinity to a frontier point p distinct from the specified points v i, together with real prevertices a i mapping to those frontier points.