The endpoints of a circular crosscut

For a point ζ on sphere c r and a radius ρ with 0 < ρ < 2 * r, the circle sphere ζ ρ cuts the disc ball c r in one open arc. This file identifies that arc, its closed companion, and its two endpoints exactly. If

• α = arg (c - ζ) is the direction from ζ to the centre, and
• φ = arccos (ρ / (2 * r)) is the half-angle of the crosscut,

then the open and closed arcs are the images under circleMap ζ ρ of (α - φ, α + φ) and [α - φ, α + φ], while the two bounding circles meet at the images of the endpoints. Since φ < π / 2, a crosscut spans less than a half turn, and the chord length along it is therefore unimodal about any one of its points; that is what makes a crosscut locally connected at its own endpoints, the last statement below.

This is the source-side endpoint interface needed by layer L5 of TauCetiRoadmap/ConformalMapping/README.md, the Jordan-domain case of Carathéodory boundary correspondence. Conformal/ShortCrosscut.lean makes the image of the open arc arbitrarily short, and Conformal/CutDiameter.lean asks local connectedness of the image boundary to join the two ends by a small boundary set. The results here name those two ends and package the open arc together with its closure; they do not assert the continuous boundary extension itself.

Main results

• TauCeti.arccos_div_two_mul_pos and TauCeti.arccos_div_two_mul_lt_pi_div_two bound the half-angle: it is positive, and below π / 2. These two facts are the standing hypotheses of almost every argument along a crosscut — they are what make the angular window nondegenerate and shorter than a period — and every crosscut file routes through them rather than re-deriving them from Real.arccos_pos and Real.arccos_lt_pi_div_two.
• TauCeti.ball_inter_sphere_eq_circleMap_image_Ioo and TauCeti.closedBall_inter_sphere_eq_circleMap_image_Icc identify the open and closed crosscut arcs.
• TauCeti.sphere_inter_sphere_eq_pair_circleMap identifies their two distinct endpoints.
• TauCeti.isPathConnected_ball_inter_sphere and TauCeti.closure_ball_inter_sphere give the corresponding topological packaging, and TauCeti.nonempty_frontier_ball_inter_closure_ball_inter_sphere records that a crosscut reaches the frontier of the disc.
• TauCeti.isPreconnected_ball_inter_sphere_inter_ball — a ball centred at a point of the closed crosscut meets the crosscut in a subarc: a crosscut spans less than a half turn, so along it the chord distance to a fixed one of its points falls and then rises, and the angles it keeps below a threshold form an interval. That last step is TauCeti.ordConnected_inter_setOf_dist_circleMap_lt and the chord length it runs on is measured by TauCeti.dist_circleMap_eq_two_mul_abs_sin; both live in TauCeti/Topology/Circle/Metric.lean, since neither mentions the disc. This is the local connectedness of a crosscut at its own endpoints, which Conformal/Crosscut/Image.lean spends to make the cluster set of a conformal map at an end of an image crosscut a continuum.

The half-width arccos (ρ / (2 * r)) is read off the cosine criterion of TauCeti/Topology/Circle/Metric.lean through Real.lt_cos_iff_mem_Ioo and Real.le_cos_iff_mem_Icc, the arccosine description of the angles at which the cosine exceeds a threshold, in TauCeti/Analysis/SpecialFunctions/Trigonometric/Arccos.lean.

Coordination with upstream Mathlib

Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort. Mathlib supplies circleMap, its periodicity and injectivity on one period, inverse trigonometric functions, and the generic fact that two circles in the plane meet in at most two points; none of the crosscut descriptions below is present there.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
• P. L. Duren, Univalent Functions, Ch. 3.

The half-angle

theorem TauCeti.arccos_div_two_mul_pos {r ρ : ℝ} (hr : 0 < r) (hρr : ρ < 2 * r) : 0 < Real.arccos (ρ / (2 * r))

The half-angle of a genuine circular crosscut is positive, so the crosscut occupies a nondegenerate arc of angles. This is Real.arccos_pos at ρ / (2 * r), the argument being below 1 exactly because ρ < 2 * r.

theorem TauCeti.arccos_div_two_mul_lt_pi_div_two {r ρ : ℝ} (hρ : 0 < ρ) (hr : 0 < r) : Real.arccos (ρ / (2 * r)) < Real.pi / 2

A genuine circular crosscut spans less than a half turn: its half-angle is below π / 2. This is Real.arccos_lt_pi_div_two at ρ / (2 * r), the argument being positive exactly because 0 < ρ.

The bound is what makes the chord distance along a crosscut unimodal (TauCeti.isPreconnected_ball_inter_sphere_inter_ball) and what keeps the closed arc of angles inside one period, so that TauCeti.circleMap is injective on it.

Metric and angular descriptions

theorem TauCeti.circleMap_mem_closedBall_iff {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (θ : ℝ) : circleMap ζ ρ θ ∈ Metric.closedBall c r ↔ ρ ≤ 2 * r * Real.cos (θ - (c - ζ).arg)

A point of sphere ζ ρ, in angular coordinates, lies in closedBall c r exactly when its angle satisfies the weak cosine inequality complementary to TauCeti.circleMap_mem_ball_iff.

This is the general criterion TauCeti.circleMap_mem_closedBall_iff_sq at dist ζ c = r, where the two squared radii cancel and the surviving condition ρ ^ 2 ≤ 2 * ρ * r * cos (θ - arg (c - ζ)) may be divided by ρ > 0.

@[simp]

theorem TauCeti.dist_circleMap_le_iff {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (θ : ℝ) : dist (circleMap ζ ρ θ) c ≤ r ↔ ρ ≤ 2 * r * Real.cos (θ - (c - ζ).arg)

The simp-normal form of TauCeti.circleMap_mem_closedBall_iff.

theorem TauCeti.circleMap_mem_sphere_iff {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (θ : ℝ) : circleMap ζ ρ θ ∈ Metric.sphere c r ↔ ρ = 2 * r * Real.cos (θ - (c - ζ).arg)

A point of sphere ζ ρ, in angular coordinates, lies on sphere c r exactly when its angle satisfies the corresponding cosine equality.

@[simp]

theorem TauCeti.dist_circleMap_eq_iff {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (θ : ℝ) : dist (circleMap ζ ρ θ) c = r ↔ ρ = 2 * r * Real.cos (θ - (c - ζ).arg)

The simp-normal form of TauCeti.circleMap_mem_sphere_iff.

The open and closed arcs

theorem TauCeti.ball_inter_sphere_eq_circleMap_image_Ioo {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : Metric.ball c r ∩ Metric.sphere ζ ρ = circleMap ζ ρ '' Set.Ioo ((c - ζ).arg - Real.arccos (ρ / (2 * r))) ((c - ζ).arg + Real.arccos (ρ / (2 * r)))

A genuine circular crosscut is exactly one open angular arc.

theorem TauCeti.closedBall_inter_sphere_eq_circleMap_image_Icc {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : Metric.closedBall c r ∩ Metric.sphere ζ ρ = circleMap ζ ρ '' Set.Icc ((c - ζ).arg - Real.arccos (ρ / (2 * r))) ((c - ζ).arg + Real.arccos (ρ / (2 * r)))

The closure-side companion of TauCeti.ball_inter_sphere_eq_circleMap_image_Ioo: a genuine circular crosscut together with its two endpoints is one closed angular arc.

The endpoints and topological packaging

theorem TauCeti.circleMap_crosscut_endpoints_ne {r ρ : ℝ} (hρ : 0 < ρ) (hρr : ρ < 2 * r) (c ζ : ℂ) : circleMap ζ ρ ((c - ζ).arg - Real.arccos (ρ / (2 * r))) ≠ circleMap ζ ρ ((c - ζ).arg + Real.arccos (ρ / (2 * r)))

The two angular endpoints of a genuine circular crosscut are distinct.

theorem TauCeti.sphere_inter_sphere_eq_pair_circleMap {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : Metric.sphere c r ∩ Metric.sphere ζ ρ = {circleMap ζ ρ ((c - ζ).arg - Real.arccos (ρ / (2 * r))), circleMap ζ ρ ((c - ζ).arg + Real.arccos (ρ / (2 * r)))}

The two circles bounding a genuine circular crosscut meet at exactly its two angular endpoints.

theorem TauCeti.isPathConnected_ball_inter_sphere {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : IsPathConnected (Metric.ball c r ∩ Metric.sphere ζ ρ)

A genuine circular crosscut is path connected: it is the image of an open real interval under the continuous circle parametrization.

theorem TauCeti.isPathConnected_closedBall_inter_sphere {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : IsPathConnected (Metric.closedBall c r ∩ Metric.sphere ζ ρ)

A genuine circular crosscut together with its endpoints is path connected.

theorem TauCeti.closure_ball_inter_sphere {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : closure (Metric.ball c r ∩ Metric.sphere ζ ρ) = Metric.closedBall c r ∩ Metric.sphere ζ ρ

Closing a genuine open circular crosscut adds exactly its two endpoints.

theorem TauCeti.nonempty_frontier_ball_inter_closure_ball_inter_sphere {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) : (frontier (Metric.ball c r) ∩ closure (Metric.ball c r ∩ Metric.sphere ζ ρ)).Nonempty

A circular crosscut of a disc reaches the boundary of the disc. A crosscut spanning less than a half turn has two endpoints (TauCeti.sphere_inter_sphere_eq_pair_circleMap), and either of them lies on sphere c r, the frontier of the disc, and in the closure of the crosscut (TauCeti.closure_ball_inter_sphere).

This is the form in which Conformal/Crosscut/Image.lean, whose statements are about an arbitrary domain, asks a cut to leave the domain at all.

theorem TauCeti.isPreconnected_ball_inter_sphere_inter_ball {c ζ : ℂ} {r ρ : ℝ} (hζ : dist ζ c = r) (hρ : 0 < ρ) (hρr : ρ < 2 * r) {e : ℂ} (he : e ∈ Metric.closedBall c r ∩ Metric.sphere ζ ρ) (δ : ℝ) : IsPreconnected (Metric.ball c r ∩ Metric.sphere ζ ρ ∩ Metric.ball e δ)

A ball centred at a point of the closed crosscut meets the crosscut in a subarc. A genuine circular crosscut spans an angle 2 * arccos (ρ / (2 * r)) < π, so along it the chord distance to a fixed one of its points is unimodal; the part of the crosscut inside any ball centred at such a point is therefore the image of an interval of angles, and in particular preconnected.

This is the local connectedness of a crosscut at its own endpoints, which is what the cluster set of a map along a crosscut needs in order to be a continuum (TauCeti.isConnected_clusterSetOn). The radius δ is arbitrary: for large δ the trace is the whole crosscut.