Carathéodory's continuity theorem

A conformal map of a disc onto a bounded region whose boundary is a Jordan curve extends continuously to the closed disc.

The argument

Fix a point ζ of the bounding circle and a tolerance ε. The crosscut neighbourhoods ball c r ∩ ball ζ ρ shrink to ζ, so by the Cauchy criterion TauCeti.subsingleton_clusterSetOn_of_forall_exists it is enough to make the image of one of them have diameter at most ε. Four inputs combine to do that, at a radius ρ chosen by the length–area method:

• a small curve along the crosscut. TauCeti.exists_isJordanCurve_superset_closure_image_ball_inter_sphere_diam_le_of_isBounded produces, at some radius ρ below any prescribed bound, a Jordan curve J of diameter at most ε containing the closed image crosscut and running back along the image boundary;
• the far side stays wide. TauCeti.exists_pos_forall_le_diam_image_sdiff_closedBall, applied at the point ζ off the disc, gives a d > 0 below which the image of the far side ball c r \ closedBall ζ ρ never shrinks, for every small ρ; taking J narrower than d makes it narrower than the far side;
• both sides of the cut are connected. The near side ball c r ∩ ball ζ ρ is an intersection of two discs, hence convex (TauCeti.isConnected_ball_inter_ball); the far side ball c r \ closedBall ζ ρ is connected by the Möbius reduction TauCeti.isConnected_ball_diff_closedBall;
• a Jordan curve minus a point is preconnected. At a point of the circular crosscut, the curve J minus that point is path-connected by TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton, so the winding-number two-sidedness theorem applies directly. No plane-separation hypothesis is needed.

TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton then puts the near side inside filledHull J — the far side cannot be the enclosed one, being wider than J — and TauCeti.diam_le_diam_of_subset_filledHull reads that enclosure as the width bound diam (f '' (ball c r ∩ ball ζ ρ)) ≤ diam J ≤ ε. Since this holds at every boundary point, the extension theorem TauCeti.exists_continuousOn_closure_eqOn_of_isBounded assembles the continuous extension on closedBall c r.

What is not claimed

Injectivity of the extension is not established, and no statement below asserts it: the L5 milestone asks for a homeomorphism of the closures, and this file supplies only the continuous extension. Given injectivity on the bounding circle, TauCeti.closureHomeomorph of Conformal/BoundaryCorrespondence.lean upgrades the extension to that homeomorphism, and TauCeti.injOn_closure_of_injOn_frontier of Conformal/ClusterSet.lean reduces injectivity on the closed disc to injectivity on the circle; producing the latter is a separate Jordan-curve argument whose analytic half is TauCeti.not_eqOn_const_inter_sphere_of_injOn of Conformal/ArcConstancy.lean.

Nor is the converse route through Conformal/Crosscut/BoundarySplit.lean taken: the enclosure route used here asks only that the near side fall inside a small curve, whereas that route asks which arc of the image boundary the near side clings to.

Roadmap role

This is layer L5 of TauCetiRoadmap/ConformalMapping/README.md, the Jordan-domain case of the Carathéodory boundary correspondence.

Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, and Mathlib has no boundary correspondence for conformal maps and no Jordan curve theorem, so this is new Lean formalization rather than a temporary shim.

Main results

• TauCeti.exists_diam_image_ball_inter_ball_le_of_isJordanCurve_frontier — the crosscut neighbourhoods at a boundary point have images of arbitrarily small diameter.
• TauCeti.subsingleton_clusterSetOn_of_isJordanCurve_frontier and TauCeti.exists_tendsto_nhdsWithin_of_isJordanCurve_frontier — such a map has at most one boundary cluster value at each point of the bounding circle, hence a boundary limit there.
• TauCeti.exists_continuousOn_closedBall_eqOn_of_isJordanCurve_frontier — Carathéodory's continuity theorem: it extends continuously to the closed disc.
• TauCeti.exists_continuousOn_closedBall_bijOn_ball_of_isJordanCurve_frontier — the form the milestone is stated in: a bounded domain with Jordan-curve boundary is the image of the disc under a holomorphic bijection continuous up to the closed disc.

References

• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913), 305–320.
• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Theorem 2.1 and §2.2–2.3.
• P. L. Duren, Univalent Functions, Theorem 3.1.

The crosscut neighbourhoods have small images

theorem TauCeti.exists_diam_image_ball_inter_ball_le_of_isJordanCurve_frontier {f : ℂ → ℂ} {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)) (hJf : IsJordanCurve (frontier (f '' Metric.ball c r))) (hζ : dist ζ c = r) {ε : ℝ} (hε : 0 < ε) : ∃ ρ > 0, Metric.diam (f '' (Metric.ball c r ∩ Metric.ball ζ ρ)) ≤ ε

The image of a crosscut neighbourhood can be made arbitrarily small. Let f be holomorphic and injective on ball c r, with bounded image whose boundary is a Jordan curve, and let ζ lie on the bounding circle. For every ε > 0 there is a crosscut radius ρ > 0 with

Metric.diam (f '' (ball c r ∩ ball ζ ρ)) ≤ ε.

The preconnectedness hypothesis on the curve J minus a point, needed by the enclosure theorem TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton, is supplied by TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton. Connectedness of both cut sides and a far side wider than J are discharged here.

The boundary limit

theorem TauCeti.subsingleton_clusterSetOn_of_isJordanCurve_frontier {f : ℂ → ℂ} {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)) (hJf : IsJordanCurve (frontier (f '' Metric.ball c r))) (hζ : dist ζ c = r) : (clusterSetOn f (Metric.ball c r) ζ).Subsingleton

Such a map has at most one cluster value at each point of the bounding circle. The Cauchy criterion TauCeti.subsingleton_clusterSetOn_of_forall_exists applied to the width bound of TauCeti.exists_diam_image_ball_inter_ball_le_of_isJordanCurve_frontier: two points of a crosscut neighbourhood have images within its diameter of each other by Metric.dist_le_diam_of_mem.

theorem TauCeti.exists_tendsto_nhdsWithin_of_isJordanCurve_frontier {f : ℂ → ℂ} {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)) (hJf : IsJordanCurve (frontier (f '' Metric.ball c r))) (hζ : dist ζ c = r) : ∃ (v : ℂ), Filter.Tendsto f (nhdsWithin ζ (Metric.ball c r)) (nhds v)

Such a map has a boundary limit at each point of the bounding circle. The values of f converge as the argument approaches ζ from inside the disc.

The cluster set at ζ is a subsingleton by TauCeti.subsingleton_clusterSetOn_of_isJordanCurve_frontier, and it is nonempty because f maps the disc into the compact closure of its bounded image, which is what TauCeti.exists_tendsto_of_clusterSetOn_subsingleton needs; Metric.closure_ball puts ζ in the closure of the disc. This is the pointwise form of TauCeti.exists_continuousOn_closedBall_eqOn_of_isJordanCurve_frontier, and names the limit.

theorem TauCeti.exists_continuousOn_closedBall_eqOn_of_isJordanCurve_frontier {f : ℂ → ℂ} {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)) (hJf : IsJordanCurve (frontier (f '' Metric.ball c r))) : ∃ (F : ℂ → ℂ), ContinuousOn F (Metric.closedBall c r) ∧ Set.EqOn F f (Metric.ball c r)

Carathéodory's continuity theorem. A holomorphic injection of a disc onto a bounded region whose boundary is a Jordan curve extends continuously to the closed disc.

Every boundary cluster set is a subsingleton by TauCeti.subsingleton_clusterSetOn_of_isJordanCurve_frontier, which is exactly what the extension theorem TauCeti.exists_continuousOn_closure_eqOn_of_isBounded asks of a map into a proper space with bounded image; Metric.frontier_ball and Metric.closure_ball turn its frontier and closure into the circle and the closed disc.

No injectivity is claimed for the extension on the circle, and none is needed for continuity.

The Jordan-domain form

theorem TauCeti.exists_continuousOn_closedBall_bijOn_ball_of_isJordanCurve_frontier {Ω : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsConnected Ω) (hΩb : Bornology.IsBounded Ω) (hΩJ : IsJordanCurve (frontier Ω)) : ∃ (g : ℂ → ℂ), ContinuousOn g (Metric.closedBall 0 1) ∧ DifferentiableOn ℂ g (Metric.ball 0 1) ∧ Set.BijOn g (Metric.ball 0 1) Ω

A bounded Jordan domain is the image of the disc under a holomorphic bijection continuous up to the closed disc. This is the form layer L5 of TauCetiRoadmap/ConformalMapping/README.md states its milestone in, minus the injectivity of the boundary values.

The Riemann mapping theorem, in the shape TauCeti.exists_bijOn_ball_differentiableOn_invFunOn, supplies a holomorphic bijection of Ω onto the disc with holomorphic inverse; the inverse is the map extended. That Ω is a proper subset of ℂ needs no separate hypothesis, frontier univ being empty while a Jordan curve is not. Nor does simple connectivity: a Jordan domain is simply connected (TauCeti.IsJordanDomain.isSimplyConnected).

The extension is named as the map itself rather than beside it: replacing the inverse Riemann map by its extension changes neither its holomorphy on the open disc nor its bijectivity onto Ω.