Carathéodory's theorem for both complementary domains of a Jordan curve

A Jordan curve C ⊆ ℂ has exactly two complementary components: its inside filledHull C \ C and its outside (filledHull C)ᶜ. This file shows that the inside is a conformal image of the open unit disc and the outside a conformal image of the exterior (closedBall 0 1)ᶜ of the closed unit disc, and that these maps extend to homeomorphisms of the closed disc onto filledHull C, the closure of the inside, and of the closed exterior (ball 0 1)ᶜ onto (filledHull C \ C)ᶜ, the closure of the outside, the unit circle going onto C in both cases.

• For the inside, the closed unit disc is homeomorphic to filledHull C, the closure of the inside, by a map that is holomorphic on the open disc and sends its centre to any prescribed point of the inside. This is Carathéodory's theorem for the Jordan domain filledHull C \ C, and in particular the closed-disc form of the Schoenflies theorem.
• For the outside, the closed exterior (ball 0 1)ᶜ of the unit disc is homeomorphic to (filledHull C \ C)ᶜ, the closure of the outside, by a map that is holomorphic off the closed disc and tends to infinity at infinity. Inverting the outside about a point p of the inside, z ↦ (z - p)⁻¹, and adding 0, the image of infinity, gives a bounded Jordan domain bounded by the inverted curve (TauCeti.IsJordanCurve.isJordanDomain_insert_zero_image_inv_sub_compl_filledHull); the exterior map is read back from its Riemann map normalized at 0.

Main results

• TauCeti.IsJordanCurve.exists_homeomorph_closedBall_filledHull — the inside of a Jordan curve is the image of the disc under a holomorphic bijection that extends to a homeomorphism of the closed disc onto filledHull C, carrying the circle onto C.
• TauCeti.IsJordanCurve.exists_homeomorph_compl_ball_compl_filledHull_sdiff — the outside of a Jordan curve is the image of the exterior of the disc under a holomorphic bijection that tends to infinity at infinity and extends to a homeomorphism of the closed exterior onto the complement of the inside, carrying the circle onto C.

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, Theorem 2.6.

The inside

theorem TauCeti.IsJordanCurve.exists_homeomorph_closedBall_filledHull {C : Set ℂ} {p : ℂ} (hC : IsJordanCurve C) (hp : p ∈ filledHull C \ C) : ∃ (g : ℂ → ℂ), ContinuousOn g (Metric.closedBall 0 1) ∧ DifferentiableOn ℂ g (Metric.ball 0 1) ∧ Set.BijOn g (Metric.ball 0 1) (filledHull C \ C) ∧ Set.BijOn g (Metric.sphere 0 1) C ∧ g 0 = p ∧ ∃ (e : ↑(Metric.closedBall 0 1) ≃ₜ ↑(filledHull C)), ∀ (z : ↑(Metric.closedBall 0 1)), ↑(e z) = g ↑z

Carathéodory's theorem for the inside of a Jordan curve. For a Jordan curve C ⊆ ℂ and a point p of its inside filledHull C \ C, there is a map g, holomorphic on the open unit disc with g 0 = p, carrying the disc bijectively onto the inside and the unit circle bijectively onto C, which restricts to a homeomorphism of the closed disc onto filledHull C.

The outside

theorem TauCeti.IsJordanCurve.exists_homeomorph_compl_ball_compl_filledHull_sdiff {C : Set ℂ} (hC : IsJordanCurve C) : ∃ (h : ℂ → ℂ), ContinuousOn h (Metric.ball 0 1)ᶜ ∧ DifferentiableOn ℂ h (Metric.closedBall 0 1)ᶜ ∧ Set.BijOn h (Metric.closedBall 0 1)ᶜ (filledHull C)ᶜ ∧ Set.BijOn h (Metric.sphere 0 1) C ∧ Filter.Tendsto h (Bornology.cobounded ℂ) (Bornology.cobounded ℂ) ∧ ∃ (e : ↑(Metric.ball 0 1)ᶜ ≃ₜ ↑(filledHull C \ C)ᶜ), ∀ (z : ↑(Metric.ball 0 1)ᶜ), ↑(e z) = h ↑z

Carathéodory's theorem for the outside of a Jordan curve. For a Jordan curve C ⊆ ℂ there is a map h, holomorphic off the closed unit disc and tending to infinity at infinity, carrying the exterior of the closed disc bijectively onto the outside (filledHull C)ᶜ and the unit circle bijectively onto C, which restricts to a homeomorphism of the closed exterior (ball 0 1)ᶜ onto the complement of the inside, the closure of the outside (TauCeti.IsJordanCurve.closure_compl_filledHull).