An image crosscut of finite length ends in two points

Conformal/Crosscut/Image.lean identifies the boundary piece a circular crosscut clings to as the union of the cluster sets of the map at the crosscut's two endpoints, and shows each of them to be a continuum. Nothing there says those continua are single points; in its own words, the identification is "with a union of cluster sets, not with a connected subset of ∂Ω running between them". This file supplies the missing degeneration, from the one hypothesis that the length–area method already produces: an image crosscut of finite length has an honest limit at each of its two ends, so its closure is the crosscut together with two points.

That this can be had at all, and without circularity, is the point. The end of an image crosscut is a boundary cluster set, and the boundary cluster sets of the map on the disc degenerating to points is exactly the layer-L5 milestone of TauCetiRoadmap/ConformalMapping/README.md still open. The ends here degenerate for a different and much cheaper reason: the arc ball c r ∩ sphere ζ ρ is one-dimensional, and the length of its image is a finite number, so the images of its angles satisfy a Cauchy criterion as the angle runs to an end of the arc. No boundary behaviour of the map on the disc is used, and none is proved.

The estimate

The engine is the chord bound of Conformal/LengthArea.lean in its primitive, set-free form TauCeti.ofReal_dist_le_mul_lintegral_Ioc: the images of the endpoints of an arc of angles are at distance at most |ρ| times the angular integral of ‖deriv f‖ over that arc. Applied to a sub-arc, it says that the oscillation of f along a piece of the circle is controlled by the length carried by that piece alone — in the vocabulary of TauCeti/MeasureTheory/Integral/DominatedIncrement.lean, that the increments of f ∘ circleMap ζ ρ are dominated by the angular length density θ ↦ |ρ| * ‖deriv f (circleMap ζ ρ θ)‖ₑ. Neither of the two conclusions drawn from that domination sees the circle: a map on an order-connected subset of ℝ whose increments are dominated by a density of finite total integral has bounded image and is uniformly continuous, the latter by absolute continuity of the integral. Both are proved there, at that generality, and the two statements below are their instances at the arc — TauCeti.exists_pos_forall_dist_le_of_lintegral_ne_top, a modulus of continuity for f along the arc in the angular parameter, and TauCeti.isBounded_image_circleMap_image_Ioo_of_lintegral_ne_top.

Turning the angular modulus into a statement about the plane needs the chord formula TauCeti.dist_circleMap_eq_two_mul_sin_abs: on an arc of angular width below a full turn the chord 2 * |ρ| * sin (|θ - θ'| / 2) stays away from zero as long as the angular gap does, so points of the arc close in the plane are close in angle — this and nothing more is what the arc not wrapping around the circle buys. With that, TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo reads the modulus as the Cauchy criterion TauCeti.subsingleton_clusterSetOn_of_forall_exists of Topology/ClusterSet.lean and concludes at every point of the closed arc, its two endpoints included.

The same chord bound, applied with the whole arc rather than a sub-arc, bounds the image (TauCeti.isBounded_image_circleMap_image_Ioo_of_lintegral_ne_top), which is what turns that subsingleton cluster set into an honest limit: TauCeti.exists_tendsto_nhdsWithin_circleMap_image_Ioo, with cluster-set form TauCeti.exists_clusterSetOn_circleMap_image_Ioo_eq_singleton. All of this is about an arc of angles and asks nothing of a crosscut.

The crosscut

The crosscut statements are those arc statements at the arc description of Conformal/Crosscut/Endpoints.lean: ball c r ∩ sphere ζ ρ is the open arc of angles within arccos (ρ / (2 * r)) of arg (c - ζ), and closedBall c r ∩ sphere ζ ρ is the closed one, of angular width 2 * arccos (ρ / (2 * r)), which is below π — and so, with room to spare, below the full turn the arc statements ask for — exactly because ρ is positive. Finiteness of the angular integral over the arc is finiteness of TauCeti.circleImageLength f (ball c r) ζ ρ, the quantity Wolff's lemma makes small: a crosscut short enough for the length–area estimates is in particular of finite length, so the hypothesis costs a consumer nothing it has not already paid for.

The conclusion, TauCeti.exists_closure_image_ball_inter_sphere_eq_insert, is that the closure of the image crosscut is the image crosscut together with two points. Which two points, and whether they are distinct, is not addressed: an image crosscut may well close up. What the L5 argument needs is only that the two ends are points on ∂Ω, so that the small arc of a locally connected ∂Ω joining them can be named.

Main results

• TauCeti.exists_pos_forall_dist_le_of_lintegral_ne_top — a modulus of continuity along an arc of finite image length, in the angular parameter.
• TauCeti.isBounded_image_circleMap_image_Ioo_of_lintegral_ne_top — an arc of finite image length has bounded image.
• TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo — at every point of an arc of angular width below a full turn and of finite image length, the cluster set of the map along the arc has at most one element.
• TauCeti.exists_tendsto_nhdsWithin_circleMap_image_Ioo and TauCeti.exists_clusterSetOn_circleMap_image_Ioo_eq_singleton — hence such an arc carries a limit at each point of its closure, its two endpoints included, and its cluster set there is a single point.
• TauCeti.subsingleton_clusterSetOn_ball_inter_sphere, TauCeti.exists_tendsto_nhdsWithin_ball_inter_sphere and TauCeti.exists_clusterSetOn_ball_inter_sphere_eq_singleton — the three arc statements at the arc of a circular crosscut, the last of them the form Conformal/Crosscut/Image.lean indexes over.
• TauCeti.exists_biUnion_clusterSetOn_ball_inter_sphere_eq_pair — hence the union of the cluster sets at the two endpoints, the term Conformal/Crosscut/Image.lean adjoins to the image crosscut to close it, is a pair of points. (That file also identifies the union with the boundary piece the image crosscut clings to, but only for injective f.)
• TauCeti.exists_closure_image_ball_inter_sphere_eq_insert — hence the closure of an image crosscut of finite length is the image crosscut together with two points.

Generality

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0–L6, everything below is stated for maps of ℂ. The arc statements ask nothing of the ambient disc — only that f be holomorphic on an open set containing the arc — so they apply to any circle in any domain, the crosscut being one instance; neither injectivity of f nor any hypothesis on its image is used anywhere in the file. They ask nothing of the sign of the radius either, a negative ρ tracing the same circle in the other sense and ρ = 0 collapsing the arc to the point ζ, where the estimates are trivial. The crosscut statements do ask 0 < ρ < 2 * r, which is what makes ball c r ∩ sphere ζ ρ a genuine crosscut.

Coordination with upstream Mathlib

Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which stops at the mapping theorem itself, and the pinned Mathlib has no boundary correspondence for conformal maps. So this file is new Lean formalization rather than a temporary shim, and it consumes no L0–L3 shim: its analytic input is the chord bound of Conformal/LengthArea.lean, which rests on the fundamental theorem of calculus along an arc.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, §2.2 (crosscuts and the length–area method).
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX.

A modulus of continuity along an arc of finite image length

theorem TauCeti.exists_pos_forall_dist_le_of_lintegral_ne_top {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (ζ : ℂ) {ρ a b : ℝ} (hmemU : ∀ θ ∈ Set.Ioo a b, circleMap ζ ρ θ ∈ U) (hfin : ∫⁻ (θ : ℝ) in Set.Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ ≠ ⊤) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ θ₁ ∈ Set.Ioo a b, ∀ θ₂ ∈ Set.Ioo a b, |θ₁ - θ₂| ≤ η → dist (f (circleMap ζ ρ θ₁)) (f (circleMap ζ ρ θ₂)) ≤ ε

A modulus of continuity along an arc of finite image length. If f is holomorphic on an open set containing the piece of the circle of radius ρ about ζ cut out by the angles Ioo a b, and the angular integral of ‖deriv f‖ over that arc is finite, then for every tolerance ε > 0 there is an angular gap η > 0 within which the images of two angles of the arc stay ε apart.

The gap is uniform over the arc, and in particular does not shrink as an end of the arc is approached: that is the whole content. A short sub-arc carries little length, and by the chord bound TauCeti.ofReal_dist_le_mul_lintegral_Ioc the length a sub-arc carries bounds the distance between the images of its two ends; that is the domination hypothesis of Set.OrdConnected.uniformContinuousOn_of_edist_le_setLIntegral, which draws the modulus from the absolute continuity of the integral and knows nothing of circles.

Uniform continuity in the angle is not uniform continuity of f on the arc as a subset of the plane, but on an arc of angular width below a full turn the two agree, which is what TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo exploits.

Nothing is assumed of the sign of the radius: a negative ρ traces the same circle in the other sense, and at ρ = 0 the circle is the single point ζ, where there is nothing to estimate.

theorem TauCeti.isBounded_image_circleMap_image_Ioo_of_lintegral_ne_top {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (ζ : ℂ) {ρ a b : ℝ} (hmemU : ∀ θ ∈ Set.Ioo a b, circleMap ζ ρ θ ∈ U) (hfin : ∫⁻ (θ : ℝ) in Set.Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ ≠ ⊤) : Bornology.IsBounded (f '' circleMap ζ ρ '' Set.Ioo a b)

An arc of finite image length has bounded image. The chord bound applied to the whole arc rather than to a sub-arc: by Set.OrdConnected.isBounded_image_of_edist_le_setLIntegral any two of its points have images at distance at most |ρ| * ∫⁻ θ in Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ, a finite number.

This is what makes a subsingleton cluster set along the arc an honest limit, the compactness input of TauCeti.exists_tendsto_of_clusterSetOn_subsingleton.

The cluster sets of an arc of finite image length

theorem TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (ζ : ℂ) {ρ a b θ₀ : ℝ} (hab : a < b) (hab2π : b - a < 2 * Real.pi) (hθ₀ : θ₀ ∈ Set.Icc a b) (hmemU : ∀ θ ∈ Set.Ioo a b, circleMap ζ ρ θ ∈ U) (hfin : ∫⁻ (θ : ℝ) in Set.Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ ≠ ⊤) : (clusterSetOn f (circleMap ζ ρ '' Set.Ioo a b) (circleMap ζ ρ θ₀)).Subsingleton

An arc of finite image length has at most one cluster value at each of its points. For f holomorphic on an open set containing the open arc circleMap ζ ρ '' Ioo a b, of angular width below a full turn and of finite image length, and for any angle θ₀ of the closed arc, f has at most one cluster value along the arc at the point circleMap ζ ρ θ₀.

The two endpoints θ₀ = a and θ₀ = b are the case with content; at an interior angle the statement is continuity. The angular width restriction is what makes closeness in the plane the same as closeness in angle, and it is exactly the requirement that the arc not wrap around the circle: by the chord formula TauCeti.dist_circleMap_eq_two_mul_sin_abs the chord is 2 * |ρ| * sin (|θ - θ₀| / 2), which over the angular gaps between m and the width b - a of the arc stays at least its value at one of those two ends, so a point of the arc within 2 * |ρ| * min (sin (m / 2)) (sin ((b - a) / 2)) of circleMap ζ ρ θ₀ is within m of θ₀ in angle. Feeding that to the modulus TauCeti.exists_pos_forall_dist_le_of_lintegral_ne_top gives the Cauchy criterion TauCeti.subsingleton_clusterSetOn_of_forall_exists. A radius of either sign traces the same circle; at ρ = 0 the arc is the single point ζ and the criterion is immediate, no angular control being needed.

theorem TauCeti.exists_tendsto_nhdsWithin_circleMap_image_Ioo {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (ζ : ℂ) {ρ a b θ₀ : ℝ} (hab : a < b) (hab2π : b - a < 2 * Real.pi) (hθ₀ : θ₀ ∈ Set.Icc a b) (hmemU : ∀ θ ∈ Set.Ioo a b, circleMap ζ ρ θ ∈ U) (hfin : ∫⁻ (θ : ℝ) in Set.Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ ≠ ⊤) : ∃ (v : ℂ), Filter.Tendsto f (nhdsWithin (circleMap ζ ρ θ₀) (circleMap ζ ρ '' Set.Ioo a b)) (nhds v)

An arc of finite image length has a limit at each point of its closure. The cluster set along the arc is a subsingleton by TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo, and it is nonempty because the image of the arc is bounded, TauCeti.isBounded_image_circleMap_image_Ioo_of_lintegral_ne_top — so the map is confined along the arc to a compact set, which is the hypothesis of TauCeti.exists_tendsto_of_clusterSetOn_subsingleton.

The two endpoints θ₀ = a and θ₀ = b are the case with content: there the arc is a curve with an honest end.

theorem TauCeti.exists_clusterSetOn_circleMap_image_Ioo_eq_singleton {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (ζ : ℂ) {ρ a b θ₀ : ℝ} (hab : a < b) (hab2π : b - a < 2 * Real.pi) (hθ₀ : θ₀ ∈ Set.Icc a b) (hmemU : ∀ θ ∈ Set.Ioo a b, circleMap ζ ρ θ ∈ U) (hfin : ∫⁻ (θ : ℝ) in Set.Ioo a b, ‖deriv f (circleMap ζ ρ θ)‖ₑ ≠ ⊤) : ∃ (v : ℂ), clusterSetOn f (circleMap ζ ρ '' Set.Ioo a b) (circleMap ζ ρ θ₀) = {v}

The cluster set of an arc of finite image length is a single point. The limit of TauCeti.exists_tendsto_nhdsWithin_circleMap_image_Ioo written as a cluster set, which is the form a boundary piece described as a union of cluster sets is indexed over.

The two ends of a circular crosscut

theorem TauCeti.subsingleton_clusterSetOn_ball_inter_sphere {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) {e : ℂ} (he : e ∈ Metric.closedBall c r ∩ Metric.sphere ζ ρ) : (clusterSetOn f (Metric.ball c r ∩ Metric.sphere ζ ρ) e).Subsingleton

A circular crosscut of finite image length has at most one cluster value at each point of its closure. This is TauCeti.subsingleton_clusterSetOn_circleMap_image_Ioo at the arc description of Conformal/Crosscut/Endpoints.lean: a genuine circular crosscut is the open arc of angles within arccos (ρ / (2 * r)) of arg (c - ζ), of angular width below π, and its closure adds exactly the two angles at the ends.

The two endpoints, where e ∈ sphere c r ∩ sphere ζ ρ, are the case with content. Neither injectivity of f nor any hypothesis on its image is used.

theorem TauCeti.exists_tendsto_nhdsWithin_ball_inter_sphere {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) {e : ℂ} (he : e ∈ Metric.closedBall c r ∩ Metric.sphere ζ ρ) : ∃ (v : ℂ), Filter.Tendsto f (nhdsWithin e (Metric.ball c r ∩ Metric.sphere ζ ρ)) (nhds v)

A circular crosscut of finite image length has a limit at each point of its closure. This is TauCeti.exists_tendsto_nhdsWithin_circleMap_image_Ioo at the arc description of Conformal/Crosscut/Endpoints.lean.

At the two endpoints, where e ∈ sphere c r ∩ sphere ζ ρ, this is the statement that the image crosscut is a curve with two honest ends.

theorem TauCeti.exists_clusterSetOn_ball_inter_sphere_eq_singleton {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) {e : ℂ} (he : e ∈ Metric.closedBall c r ∩ Metric.sphere ζ ρ) : ∃ (v : ℂ), clusterSetOn f (Metric.ball c r ∩ Metric.sphere ζ ρ) e = {v}

The end of a circular crosscut of finite image length is a single point. This is TauCeti.exists_clusterSetOn_circleMap_image_Ioo_eq_singleton at the arc description of Conformal/Crosscut/Endpoints.lean, and it is the form TauCeti.frontier_inter_closure_image_inter_sphere_eq_biUnion_clusterSetOn of Conformal/Crosscut/Image.lean indexes the boundary piece over.

theorem TauCeti.exists_biUnion_clusterSetOn_ball_inter_sphere_eq_pair {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) : ∃ (u : ℂ) (v : ℂ), ⋃ e ∈ Metric.sphere c r ∩ Metric.sphere ζ ρ, clusterSetOn f (Metric.ball c r ∩ Metric.sphere ζ ρ) e = {u, v}

The two ends of a circular crosscut of finite image length are two points. The union of the cluster sets of f at the two endpoints of the crosscut is a pair. That union is the term Conformal/Crosscut/Image.lean adjoins to the image crosscut to write closure (f '' (ball c r ∩ sphere ζ ρ)), under exactly the hypotheses assumed here; that decomposition is a union, not a disjoint one, so nothing here says the pair misses the image crosscut. The other description of the union in that file, as the piece of frontier (f '' ball c r) the image crosscut clings to, is not available here: it asks f to be injective on ball c r, which makes f '' ball c r open and hence disjoint from its own frontier. Adding that hypothesis is TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair of Conformal/Crosscut/BoundaryEnds.lean.

Nothing is claimed about the two points: they may coincide, an image crosscut being free to close up. What a boundary-correspondence argument needs of them is that they are points at all, so that the arc of a locally connected image boundary joining them can be named.

theorem TauCeti.exists_closure_image_ball_inter_sphere_eq_insert {f : ℂ → ℂ} {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) : ∃ (u : ℂ) (v : ℂ), closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) = insert u (insert v (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)))

The closure of an image crosscut of finite length is the image crosscut together with two points. Conformal/Crosscut/Image.lean writes that closure as the image crosscut together with the cluster sets at the two endpoints, and TauCeti.exists_biUnion_clusterSetOn_ball_inter_sphere_eq_pair collapses those to a pair.

Which two points they are is not recorded here; the sharper statement that they are exactly the points where the closed image crosscut meets frontier (f '' ball c r) is TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair in Conformal/Crosscut/BoundaryEnds.lean, which asks injectivity of f in addition.