Small Jordan curves through image crosscuts

Let f be a conformal map of a disc onto a bounded domain whose frontier is a Jordan curve. The length--area method supplies, at every point ζ of the source circle, arbitrarily small circular crosscuts with short images. This file closes such an image crosscut along the frontier of the image domain and proves that the resulting Jordan curve is arbitrarily small.

There are two cases. If the two boundary ends of the closed image crosscut coincide, the crosscut itself is a Jordan curve by TauCeti.isJordanCurve_closure_image_ball_inter_sphere_of_subsingleton. Otherwise the crosscut is an arc between two nearby points of the image frontier. The quantitative Jordan-curve theorem TauCeti.IsJordanCurve.exists_pos_forall_exists_path_injective_diam_le joins those points by a small injective path along the frontier, and the distinct-end closing theorem from Conformal/Crosscut/Arc.lean closes the two arcs into a Jordan curve. In both cases the curve lies in the closure of the image domain and contains the closed image crosscut.

Main result

• TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le -- below every prescribed radius, a short image crosscut lies on an arbitrarily small Jordan curve contained in the closure of the image domain.
• TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded -- the bounded-image form used for a Riemann map.

Roadmap role

This is the last construction before the planar-separation step in layer L5 of the ConformalMapping roadmap, the Jordan-domain case of the Caratheodory boundary correspondence. The remaining step is to show that the boundary piece of the crosscut neighbourhood lies on the small Jordan curve chosen here. The existing crosscut criterion then bounds the cut-off image piece and gives the continuous extension of the conformal map.

Layer L5 is absent from Mathlib's in-progress Riemann-mapping development, and the pinned Mathlib has no Jordan-curve vocabulary. The proof follows the crosscut argument in Caratheodory's 1913 paper and the presentations in Pommerenke, Section 2.2--2.3, and Duren, Chapter 3.

References

• C. Caratheodory, Ueber die gegenseitige Beziehung der Raender bei der konformen Abbildung, Math. Ann. 73 (1913).
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Sections 2.2--2.3.
• P. L. Duren, Univalent Functions, Chapter 3.

theorem TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le {f : ℂ → ℂ} {c ζ : ℂ} {r : ℝ} (hζ : dist ζ c = r) (hr : 0 < r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hinj : Set.InjOn f (Metric.ball c r)) (hdir : ∫⁻ (z : ℂ) in Metric.ball c r, ‖deriv f z‖ₑ ^ 2 ≠ ⊤) (hfrontier : IsJordanCurve (frontier (f '' Metric.ball c r))) {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) : ∃ ρ ∈ Set.Ioo 0 R, ρ < 2 * r ∧ ∃ (J : Set ℂ), IsJordanCurve J ∧ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ⊆ J ∧ J ⊆ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ∪ frontier (f '' Metric.ball c r) ∧ J ⊆ closure (f '' Metric.ball c r) ∧ Metric.diam J ≤ ε

A short image crosscut lies on a small Jordan curve. Let f be holomorphic and injective on ball c r, with finite Dirichlet integral and Jordan-curve frontier. For every ε > 0, every boundary point ζ of the disc, and every radius bound R > 0, there is a genuine circular crosscut of radius ρ < R whose closed image is contained in a Jordan curve J satisfying

• J ⊆ closure (f '' ball c r), and
• Metric.diam J ≤ ε.

The closed image crosscut may itself be the Jordan curve: this is the case in which its two ends on frontier (f '' ball c r) coincide. When the ends are distinct, J is the union of the closed image crosscut and a small injective path along that frontier.

No assertion is made about which component of the complement of J contains the crosscut neighbourhood. Identifying that component is the planar-separation input still needed by the Caratheodory boundary correspondence.

theorem TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded {f : ℂ → ℂ} {c ζ : ℂ} {r : ℝ} (hζ : dist ζ c = r) (hr : 0 < r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hinj : Set.InjOn f (Metric.ball c r)) (hb : Bornology.IsBounded (f '' Metric.ball c r)) (hfrontier : IsJordanCurve (frontier (f '' Metric.ball c r))) {ε R : ℝ} (hε : 0 < ε) (hR : 0 < R) : ∃ ρ ∈ Set.Ioo 0 R, ρ < 2 * r ∧ ∃ (J : Set ℂ), IsJordanCurve J ∧ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ⊆ J ∧ J ⊆ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ∪ frontier (f '' Metric.ball c r) ∧ J ⊆ closure (f '' Metric.ball c r) ∧ Metric.diam J ≤ ε

The bounded-image form of the small-Jordan-curve theorem. A holomorphic injection of a disc onto a bounded domain has finite Dirichlet integral by the conformal area formula, so for every positive tolerance and radius bound, some closed image crosscut can be chosen on a Jordan curve in the closure of the image domain whose diameter is at most the tolerance.

This is the form used for the Riemann map of a bounded Jordan domain.