Documentation

TauCeti.Analysis.Complex.Conformal.Crosscut.BoundaryEnds

The ends of an image crosscut are two boundary points #

A circular crosscut ball c r ∩ sphere ζ ρ at a boundary point ζ of a disc is carried by a conformal map f to a curve inside the image domain f '' ball c r, and that curve reaches the boundary of the image domain only in the limit. Two files describe what it reaches:

Putting the two together is what this file does: for an injective holomorphic f, the closed image crosscut meets the boundary of the image domain in a pair of points,

frontier (f '' ball c r) ∩ closure (f '' (ball c r ∩ sphere ζ ρ)) = {u, v},

and those two points are no further apart than the image crosscut is wide. Feeding that width bound the length–area estimate of Conformal/ShortCrosscut.lean then gives the statement layer L5 of TauCetiRoadmap/ConformalMapping/README.md — Carathéodory's boundary correspondence — consumes: at every boundary point of the disc, and below every prescribed radius, there is a crosscut whose image is narrow and whose two ends are two points of the image boundary within ε of each other.

That is precisely the hypothesis TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le of TauCeti/Topology/JordanCurve/SmallArc.lean runs on: two nearby points of a Jordan curve cut a small closed arc off it. Until now nothing connected the analytic side of L5 — the length–area method, which produces short image crosscuts — to the topological side, which turns two nearby boundary points into a small boundary arc; the pair {u, v} produced here is the connection.

What is not claimed #

The two ends may coincide: an image crosscut is free to close up, and no hypothesis available here excludes it. So {u, v} is a pair only in the sense of Set.instInsert, possibly a singleton, and the small-arc theorem — which asks p ≠ q — still has to rule that out from properties of the image domain. Nor is the piece of the boundary cut off between the two ends identified: bounding frontier (f '' ball c r) ∩ frontier (f '' (ball c r ∩ ball ζ ρ)), the second geometric input of TauCeti.exists_continuousOn_closure_eqOn_of_forall_exists_diam_union_le, is a matter of the image domain rather than of the crosscut, and is untouched here.

Main results #

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 disc is a general ball c r rather than the unit disc, the boundary point entering only through dist ζ c = r.

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. Through Conformal/Crosscut/Image.lean it consumes the L0–L3 shim TauCeti.isOpen_image_of_differentiableOn_of_injOn, to be refactored onto Mathlib's open mapping API once the upstream work lands.

References #

The boundary piece of an image crosscut is a pair #

source
theorem TauCeti.exists_frontier_inter_closure_image_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)) (hinj : Set.InjOn f (Metric.ball c r)) (hfin : circleImageLength f (Metric.ball c r) ζ ρ ≠ ⊤) :
∃ (u : ℂ) (v : ℂ), frontier (f '' Metric.ball c r) ∩ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) = {u, v}

A closed image crosscut of finite length meets the boundary of the image domain in a pair of points. For f holomorphic and injective on ball c r, and a genuine circular crosscut ball c r ∩ sphere ζ ρ at a boundary point ζ whose image has finite length,

frontier (f '' ball c r) ∩ closure (f '' (ball c r ∩ sphere ζ ρ)) = {u, v}.

The two ingredients are already in place and only have to be matched up: TauCeti.frontier_inter_closure_image_inter_sphere_eq_biUnion_clusterSetOn writes the left-hand side as the union of the cluster sets of f over frontier (ball c r) ∩ sphere ζ ρ, which is sphere c r ∩ sphere ζ ρ since 0 < r, and TauCeti.exists_biUnion_clusterSetOn_ball_inter_sphere_eq_pair evaluates that union to a pair.

Injectivity enters only through the first of the two, where it makes f '' ball c r open and so disjoint from its own frontier; that is what excludes the image crosscut itself from the boundary piece. The two points may coincide.

Membership of the two ends in frontier (f '' ball c r) is read off the statement: u and v lie in {u, v}, hence in the left-hand side, hence in frontier (f '' ball c r).

Crosscuts with a short image and close ends #

source
theorem TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair_dist_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)) (hfin : ∫⁻ (z : ℂ) in Metric.ball c r, ‖deriv f z‖ₑ ^ 2 ≠ ⊤) {ε : ℝ} (hε : 0 < ε) {R : ℝ} (hR : 0 < R) :
∃ ρ ∈ Set.Ioo 0 R, ∃ (u : ℂ) (v : ℂ), frontier (f '' Metric.ball c r) ∩ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) = {u, v} ∧ dist u v ≤ ε ∧ Metric.diam (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ≤ ε

A holomorphic injection of finite Dirichlet integral has, at every boundary point, crosscuts of arbitrarily small radius whose image is narrow and whose two ends are close together on the image boundary. For f holomorphic and injective on ball c r with ∫⁻ z in ball c r, ‖deriv f z‖ₑ ^ 2 ≠ ⊤, every tolerance ε > 0 and every bound R > 0 admit a radius ρ < R at which the image of ball c r ∩ sphere ζ ρ has diameter at most ε and the closed image crosscut meets frontier (f '' ball c r) in two points at distance at most ε.

The radius comes from TauCeti.exists_diam_image_ball_inter_sphere_le_and_circleImageLength_ne_top, the length--area selection of Conformal/ShortCrosscut.lean: below any prescribed bound it produces a radius at which TauCeti.circleImageLength f (ball c r) ζ ρ is finite — which is what TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair needs, so the ends are two points — and at which the image crosscut is no wider than ε. That width is passed on to the two ends by TauCeti.diam_frontier_inter_closure_image_inter_sphere_le: they lie in the boundary piece and so are no further apart than the image crosscut is wide.

Only 0 < r is asked of the disc, and only 0 < R of the prescribed bound: the radius is searched for below min R (2 * r) instead of below R, which is what makes ball c r ∩ sphere ζ ρ a genuine circular crosscut rather than the empty set.

source
theorem TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair_dist_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)) {ε : ℝ} (hε : 0 < ε) {R : ℝ} (hR : 0 < R) :
∃ ρ ∈ Set.Ioo 0 R, ∃ (u : ℂ) (v : ℂ), frontier (f '' Metric.ball c r) ∩ closure (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) = {u, v} ∧ dist u v ≤ ε ∧ Metric.diam (f '' (Metric.ball c r ∩ Metric.sphere ζ ρ)) ≤ ε

A conformal map of a disc has, at every boundary point, crosscuts of arbitrarily small radius whose image is narrow and whose two ends are close together on the image boundary. This is the case of TauCeti.exists_frontier_inter_closure_image_ball_inter_sphere_eq_pair_dist_le that a Riemann map falls under: for f injective on ball c r with bounded image the Dirichlet integral is the area of that image, hence finite by TauCeti.lintegral_enorm_deriv_sq_ne_top_of_isBounded.

This is the form the Jordan-domain boundary correspondence consumes. Its two ends u and v lie on frontier (f '' ball c r), which for a Jordan domain is a Jordan curve, and they are within ε of each other, so TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le cuts a small closed arc off that curve between them — once u ≠ v is known, which nothing here supplies.