Two nearby points cut a small arc off a Jordan curve

TauCeti/Topology/JordanCurve/Separation.lean cuts a Jordan curve at two of its points into two arcs. That cutting is purely qualitative: it says nothing about the size of the two pieces. This file adds the quantitative statement, for a Jordan curve in a metric space: as the two cut points approach each other, one of the two arcs shrinks. Given ε > 0 there is a δ > 0 such that any two distinct points of the curve at distance less than δ cut off an arc of diameter at most ε.

The statement is not a formality — it is exactly where compactness of the curve enters. Two points of a Jordan curve that are close in the ambient space need not be close along the curve for any individual pair; what makes them close along the curve is that the parametrization by the circle is a homeomorphism of a compact space, hence uniformly continuous in both directions.

Why this is a layer-L5 prerequisite

Layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) is Carathéodory's boundary correspondence for a Jordan domain. Its analytic half runs the length–area method on the circular crosscuts of Conformal/Crosscut.lean: a crosscut of the disc at a boundary point is mapped by the Riemann map to a crosscut of Ω whose endpoints on ∂Ω are close, by the length–area estimate TauCeti.exists_diam_image_ball_inter_sphere_le. To convert that into the collar bound TauCeti.exists_continuousOn_closedBall_eqOn asks for, one needs the region the image crosscut cuts off to be small, and that region is bounded by the crosscut together with one of the two arcs into which its endpoints cut ∂Ω. So the missing geometric input is precisely that two nearby points of the Jordan curve ∂Ω cut off an arc of small diameter — which is what this file supplies, at the generality of an arbitrary Jordan curve in a metric space.

The argument

Everything is transported from the model curve, and the transport is quantitative, so the comparison of the chord with the arc on the circle comes first. It is not specific to Jordan curves and lives in TauCeti/Topology/Circle/Metric.lean: the chord is at most the arc (TauCeti.diam_circleExp_image_Icc_le), and conversely the shorter of the two arc lengths Circle.angleDiff separating two points is at most π / 2 times their chord (TauCeti.min_angleDiff_le_pi_div_two_mul_dist). The converse bound is the one that matters here: it is what turns a hypothesis about the ambient distance into a bound on an arc.

Together these give TauCeti.exists_isPreconnected_union_eq_compl_pair_circle_diam_le: two distinct points of the circle cut it into two preconnected pieces, the first of which stays of diameter at most π / 2 times their distance after the cut points are put back. The two pieces are Mathlib's open arcs Circle.path z w '' Set.Ioo 0 1 and Circle.path w z '' Set.Ioo 0 1, whose covering of the cut circle is Circle.compl_range_path together with Circle.range_path_inter_range_path, and each of them with its two endpoints lies in the closed arc Circle.range_path, a Circle.exp image of an interval of angles, on which the diameter bound is immediate. Only preconnectedness of the pieces is recorded, not the openness and path-connectedness of TauCeti.exists_isOpen_isPathConnected_union_eq_compl_pair_circle; that is all the transport below consumes.

The transport then runs both uniform continuities of the parametrization TauCeti.jordanParam of TauCeti/Topology/JordanCurve/Basic.lean at once: one converts "the two points are close in X" into "their parameters are close on the circle", the other converts "the parameter arc is short" into "its image has small diameter". That transport is carried out in one step, which builds a small arc. The main statement below then only has to locate that arc inside an arbitrary separating decomposition; that part is set-theoretic except for its closing step, which compares diameters and so still needs the curve to be bounded.

Identifying the arcs

The conclusion is stated so that it constrains any decomposition of C \ {p, q} into two arcs, rather than only the one this file happens to build: TauCeti.IsJordanCurve.exists_pos_forall_diam_le says that for A and B disjoint with union C \ {p, q} and separating preconnected sets — the exact conclusion of TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair — one of A ∪ {p, q}, B ∪ {p, q} has diameter at most ε. That works because the separating property applied to the two transported pieces pins each of them inside A or inside B, and a piece that swallows both makes the other one empty. Feeding it the arcs of that theorem gives the packaged form TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le, in which the first arc is the small one.

The two cut points are kept in the set whose diameter is bounded because that is the set a consumer needs: the small arc is used as a boundary curve, joined to a crosscut ending at p and q, so the endpoints must lie in the small set. It is also the stronger statement, Metric.diam A ≤ ε following by Metric.diam_mono. No incidence statement such as p ∈ closure A can be added at this generality, since A = ∅ and B = C \ {p, q} satisfy every hypothesis.

Generality

Unlike TauCeti/Topology/JordanCurve/Separation.lean, whose statements are for an arbitrary topological space, the results here need a metric on the ambient space to speak of Metric.diam and of two points being close, so X carries a PseudoMetricSpace instance. Nothing else is assumed: in particular the curve is not required to lie in ℂ, so ∂Ω may be met at whatever generality a consumer has it.

Joining the two points by an injective path

A consumer that joins the small arc to another one — gluing two arcs along their two common endpoints into a closed curve — needs it as a path rather than as a set, and needs that path injective, since a path-connected set carries paths with arbitrary repetitions. The last two statements below supply exactly that, and nothing more: an injective path with the two prescribed endpoints, running inside the curve, whose range is of small diameter. They relate its range to neither of the two arcs of the cut above.

Their witness on the circle is Mathlib's arc Circle.path, injective by Circle.path_injective_of_ne and reversed by Path.symm when the counterclockwise direction is the long way round; transporting it along the parametrization, which is injective and continuous, gives an injective path along the curve. Its diameter is bounded by the same two uniform continuities, which are recorded here once and spent by both transports.

Main results

• TauCeti.exists_isPreconnected_union_eq_compl_pair_circle_diam_le — two distinct points cut the circle into two preconnected arcs, the first of which is of diameter at most π / 2 times their distance even after the two points are put back, and TauCeti.exists_path_injective_diam_range_le_circle — two distinct points of the circle are the endpoints of an injective path whose range has diameter at most π / 2 times their distance.
• TauCeti.IsJordanCurve.exists_pos_forall_diam_le — the main statement: for every ε > 0 there is a δ > 0 such that two distinct points p, q of a Jordan curve at distance less than δ cut it into two arcs one of which has diameter at most ε together with p and q.
• TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le — the same packaged with the cutting itself, producing the two arcs with the small one named first.
• TauCeti.IsJordanCurve.exists_pos_forall_exists_path_injective_diam_le — two nearby points of a Jordan curve are the endpoints of an injective path along it whose range is of diameter at most ε.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).

Cutting the circle into a short arc and a long one

theorem TauCeti.exists_isPreconnected_union_eq_compl_pair_circle_diam_le {z w : Circle} (hzw : z ≠ w) : ∃ (P : Set Circle) (Q : Set Circle), IsPreconnected P ∧ IsPreconnected Q ∧ P ∪ Q = {z, w}ᶜ ∧ Metric.diam (P ∪ {z, w}) ≤ Real.pi / 2 * dist z w

Two distinct points cut the circle into a short arc and a long one. The complement of {z, w} is the union of two preconnected sets, the first of which stays of diameter at most π / 2 * dist z w even after the two cut points are put back: it is P ∪ {z, w}, the closed short arc, that is bounded.

theorem TauCeti.exists_path_injective_diam_range_le_circle {z w : Circle} (hzw : z ≠ w) : ∃ (γ : Path z w), Function.Injective ⇑γ ∧ Metric.diam (Set.range ⇑γ) ≤ Real.pi / 2 * dist z w

Two points of the circle are joined by a short injective path. Two distinct points of the circle are the endpoints of an injective path whose range has diameter at most π / 2 times their distance.

The witness is Mathlib's arc Circle.path z w, injective by Circle.path_injective_of_ne, taken in the direction in which Circle.angleDiff is smaller, and its reverse otherwise; reversing changes neither the range (Path.symm_range) nor injectivity. Only the endpoints, the injectivity and the diameter bound are recorded: nothing is stated relating the range to either piece of the cut of TauCeti.exists_isPreconnected_union_eq_compl_pair_circle_diam_le.

The diameter bound is TauCeti.diam_range_circlePath_le — the arc bounds the chords across it — fed the comparison TauCeti.min_angleDiff_le_pi_div_two_mul_dist of the shorter arc with the chord, which is the comparison that bounds the short arc there too.

Cutting a Jordan curve

theorem TauCeti.IsJordanCurve.exists_pos_forall_diam_le {X : Type u_1} [PseudoMetricSpace X] {C : Set X} {ε : ℝ} (h : IsJordanCurve C) (hε : 0 < ε) : ∃ δ > 0, ∀ ⦃p : X⦄, p ∈ C → ∀ ⦃q : X⦄, q ∈ C → p ≠ q → dist p q < δ → ∀ (A B : Set X), A ∪ B = C \ {p, q} → Disjoint A B → (∀ ⦃S : Set X⦄, S ⊆ C \ {p, q} → IsPreconnected S → S ⊆ A ∨ S ⊆ B) → Metric.diam (A ∪ {p, q}) ≤ ε ∨ Metric.diam (B ∪ {p, q}) ≤ ε

Two nearby points cut a small arc off a Jordan curve. For every ε > 0 there is a δ > 0 with the following property: if p and q are two distinct points of a Jordan curve C at distance less than δ, then in any splitting of C \ {p, q} into two disjoint pieces A and B that separate it — that is, such that every preconnected subset of C \ {p, q} lies in one of them — one of the two pieces has diameter at most ε together with the two cut points: the bound is on A ∪ {p, q} or on B ∪ {p, q}, the corresponding closed arc.

Bounding the closed arc rather than the open one is what a consumer needs: the small arc is used as a boundary curve joined to a crosscut ending at p and q, so the endpoints have to be inside the set that is small. It is also strictly stronger, Metric.diam A ≤ ε following by Metric.diam_mono. Note that no incidence statement such as p ∈ closure A can be added at this generality: A = ∅, B = C \ {p, q} satisfies every hypothesis.

The hypotheses on A and B are exactly the conclusion of TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair, so the statement constrains that cutting without having to reproduce it; TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le records the combination.

theorem TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le {X : Type u_1} [PseudoMetricSpace X] {C : Set X} {ε : ℝ} (h : IsJordanCurve C) (hε : 0 < ε) : ∃ δ > 0, ∀ ⦃p : X⦄, p ∈ C → ∀ ⦃q : X⦄, q ∈ C → p ≠ q → dist p q < δ → ∃ (A : Set X) (B : Set X), IsPathConnected A ∧ IsPathConnected B ∧ Disjoint A B ∧ A ∪ B = C \ {p, q} ∧ (∀ ⦃S : Set X⦄, S ⊆ C \ {p, q} → IsPreconnected S → S ⊆ A ∨ S ⊆ B) ∧ Metric.diam (A ∪ {p, q}) ≤ ε

Two nearby points cut a small arc off a Jordan curve, in packaged form: for every ε > 0 there is a δ > 0 such that two distinct points of a Jordan curve at distance less than δ cut it into two arcs, the first of which has diameter at most ε once its two endpoints are put back, that is, A ∪ {p, q} is small.

This is the form the Carathéodory boundary argument consumes: the small closed arc A ∪ {p, q}, together with the crosscut whose endpoints are p and q, bounds the region that has to be shown to have small diameter, so the endpoints must be inside the set that is bounded. For the form that instead constrains an arbitrary separating decomposition, see TauCeti.IsJordanCurve.exists_pos_forall_diam_le.

Joining the two points by an injective path

theorem TauCeti.IsJordanCurve.exists_pos_forall_exists_path_injective_diam_le {X : Type u_1} [PseudoMetricSpace X] {C : Set X} {ε : ℝ} (h : IsJordanCurve C) (hε : 0 < ε) : ∃ δ > 0, ∀ ⦃p : X⦄, p ∈ C → ∀ ⦃q : X⦄, q ∈ C → p ≠ q → dist p q < δ → ∃ (γ : Path p q), Function.Injective ⇑γ ∧ Set.range ⇑γ ⊆ C ∧ Metric.diam (Set.range ⇑γ) ≤ ε

Two nearby points of a Jordan curve are joined by a small injective path along it. For every ε > 0 there is a δ > 0 such that two distinct points p, q of a Jordan curve C at distance less than δ are the endpoints of an injective path whose range lies on C and has diameter at most ε.

Injectivity is what a consumer joining this path to a second one needs — gluing two arcs along their common endpoints into a closed curve is a statement about paths — and it is not available from the path-connectedness of the arcs of TauCeti.IsJordanCurve.exists_pos_forall_exists_diam_le, which yields a path but no control of its repetitions.

The transport is that of TauCeti.IsJordanCurve.exists_pos_forall_exists_isPreconnected_diam_union_pair_le, run on the circle statement TauCeti.exists_path_injective_diam_range_le_circle instead of on the cut into two arcs: the parametrization TauCeti.jordanParam e is injective and continuous, so it carries the injective path of parameters to an injective path along C, and both uniform continuities are spent exactly as before.

Nothing is claimed here about the two arcs of C \ {p, q}: neither which of them the path traverses, nor that its range is one of them together with the endpoints. What the conclusion offers is a subset of C containing p and q, of diameter at most ε, traversed injectively.

theorem TauCeti.IsJordanCurve.exists_isCompact_isPreconnected_notMem_sdiff_subset_ball {X : Type u_1} [PseudoMetricSpace X] {C : Set X} (hJ : IsJordanCurve C) {a : X} (ha : a ∈ C) {r : ℝ} (hr : 0 < r) : ∃ S ⊆ C, IsCompact S ∧ IsPreconnected S ∧ a ∉ S ∧ C \ S ⊆ Metric.ball a r

A Jordan curve has, near any of its points, a compact preconnected arc missing that point whose complement lies in a given ball around it. The compact arc S is the image of a closed circle arc under the Jordan parametrization, chosen small enough that its complement C \ S — the open window through a — stays inside ball a r.