Unbounded Jordan domains

An unbounded open set U ⊆ ℂ is a Jordan domain of the Riemann sphere when its frontier, together with the point at infinity, is a Jordan curve in OnePoint ℂ: for instance the upper half-plane, a sector, or an unbounded polygonal domain. Inverting such a domain about a point q outside its closure, z ↦ (z - q)⁻¹, gives a bounded domain whose frontier is the inverted frontier of U together with 0, the image of infinity; so it is a bounded Jordan domain of the plane. Carathéodory's theorem for that bounded domain, read back through the inversion, gives the Riemann map of U on the closed upper half-plane: a homeomorphism onto the closure of U which sends the real line onto the frontier and tends to infinity at infinity.

Main statements

• TauCeti.frontier_image_inv_sub: inverting an open unbounded set about a point outside its closure adds 0 to the inverted frontier.
• TauCeti.isJordanCurve_frontier_image_inv_sub: the inversion of an unbounded Jordan domain about an exterior point is a bounded Jordan domain.
• TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_insert_infty: Carathéodory's theorem on the closed upper half-plane for an unbounded Jordan domain, with infinity sent to infinity.
• TauCeti.exists_prevertices_of_isJordanCurve_insert_infty: such a map with real prevertices of 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.isOpen_image_inv_sub {U : Set ℂ} {q : ℂ} (hUo : IsOpen U) (hqU : q ∉ U) : IsOpen ((fun (z : ℂ) => (z - q)⁻¹) '' U)

The inversion z ↦ (z - q)⁻¹ maps an open set not containing q to an open set.

theorem TauCeti.isBounded_image_inv_sub {U : Set ℂ} {q : ℂ} (hq : q ∉ closure U) : Bornology.IsBounded ((fun (z : ℂ) => (z - q)⁻¹) '' U)

Inverting a set U about a point q outside its closure gives a bounded set.

theorem TauCeti.not_isBounded_of_isJordanCurve_insert_infty {S : Set ℂ} (hS : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' S))) : ¬Bornology.IsBounded S

A Jordan curve of the Riemann sphere through the point at infinity is unbounded in the plane: were its finite part S bounded, infinity would be an isolated point of the curve.

theorem TauCeti.not_isBounded_of_isJordanCurve_frontier {U : Set ℂ} (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) : ¬Bornology.IsBounded U

An open set whose frontier is, with the point at infinity, a Jordan curve of the Riemann sphere is unbounded.

theorem TauCeti.closure_image_inv_sub {U : Set ℂ} {q : ℂ} (hq : q ∉ closure U) (hUb : ¬Bornology.IsBounded U) : closure ((fun (z : ℂ) => (z - q)⁻¹) '' U) = insert 0 ((fun (z : ℂ) => (z - q)⁻¹) '' closure U)

Inverting an unbounded set U about a point q outside its closure, the closure of the image is the image of the closure together with 0, the image of infinity.

theorem TauCeti.frontier_image_inv_sub {U : Set ℂ} {q : ℂ} (hUo : IsOpen U) (hq : q ∉ closure U) (hUb : ¬Bornology.IsBounded U) : frontier ((fun (z : ℂ) => (z - q)⁻¹) '' U) = insert 0 ((fun (z : ℂ) => (z - q)⁻¹) '' frontier U)

Inverting an open unbounded set U about a point q outside its closure, the frontier of the image is the image of the frontier together with 0, the image of infinity.

theorem TauCeti.isJordanCurve_insert_zero_image_inv_sub {q : ℂ} {S : Set ℂ} (hq : q ∉ S) (hS : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' S))) : IsJordanCurve (insert 0 ((fun (z : ℂ) => (z - q)⁻¹) '' S))

Inverting the finite part of a spherical Jordan curve through infinity about a point off that curve gives a planar Jordan curve through 0. No domain or frontier identification is needed.

theorem TauCeti.isJordanCurve_frontier_image_inv_sub {U : Set ℂ} {q : ℂ} (hUo : IsOpen U) (hq : q ∉ closure U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) : IsJordanCurve (frontier ((fun (z : ℂ) => (z - q)⁻¹) '' U))

Inverting an unbounded Jordan domain gives a bounded Jordan domain. If the frontier of an open set U, together with infinity, is a spherical Jordan curve, inversion about a point outside its closure gives a planar Jordan frontier through 0.

theorem TauCeti.exists_continuousOn_bijOn_upperHalfPlaneSet_of_isJordanCurve_insert_infty {U : Set ℂ} {q : ℂ} (hUo : IsOpen U) (hUc : IsConnected U) (hq : q ∉ closure U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) : ∃ (f : ℂ → ℂ), ContinuousOn f {z : ℂ | 0 ≤ z.im} ∧ DifferentiableOn ℂ f UpperHalfPlane.upperHalfPlaneSet ∧ Set.BijOn f UpperHalfPlane.upperHalfPlaneSet U ∧ Set.BijOn f {z : ℂ | 0 ≤ z.im} (closure U) ∧ Set.BijOn f {z : ℂ | z.im = 0} (frontier U) ∧ Filter.Tendsto f (Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 ≤ z.im}) (Bornology.cobounded ℂ)

Carathéodory's theorem on the closed upper half-plane for an unbounded Jordan domain. Let U be a connected open subset of ℂ with a point q outside its closure, and suppose that the frontier of U together with the point at infinity is a Jordan curve of the Riemann sphere, so that U is unbounded. 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 U, from the closed upper half-plane onto closure U and from the real line onto frontier U, and which tends to infinity at infinity within the closed half-plane.

The Jordan curve theorem on the sphere would supply the exterior point q from the other hypotheses; here it is assumed.

theorem TauCeti.exists_prevertices_of_isJordanCurve_insert_infty {U : Set ℂ} {q : ℂ} {ι : Type u_1} (hUo : IsOpen U) (hUc : IsConnected U) (hq : q ∉ closure U) (hUJ : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' frontier U))) {v : ι → ℂ} (hv : Function.Injective v) (hvU : ∀ (i : ι), v i ∈ frontier U) : ∃ (f : ℂ → ℂ) (a : ι → ℝ), 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}) (Bornology.cobounded ℂ)

A Carathéodory map of the upper half-plane onto an unbounded Jordan domain U, sending infinity to infinity, together with real prevertices a i mapping to prescribed distinct points v i of the frontier of U.