Moving sofa: related mathematical developments #
Infrastructure.Topology.Foundations.Development001.Infrastructure.Curves.Foundations.Development002.
Moving sofa: related mathematical developments #
JordanPick.JordanCurve.Arcs.JordanPick.JordanCurve.Brouwer.JordanPick.JordanCurve.Counting.JordanPick.JordanCurve.TauCeti.Analysis.Calculus.MetricVariation.TauCeti.Analysis.Normed.Module.Ball.Exterior.TauCeti.Analysis.Normed.Module.HalfSpace.TauCeti.Topology.EMetricSpace.BoundedVariation.External.TauCeti.Topology.Frontier.TauCeti.Topology.FilledHull.TauCeti.Analysis.Normed.Module.FilledHull.TauCeti.Topology.LocallyConnected.TauCeti.Topology.JordanCurve.Basic.TauCeti.Topology.JordanCurve.Path.
Arc scaffolding for the (continuous) Jordan curve theorem #
Reusable topology lemmas that split a topological circle into closed arcs, each homeomorphic to the unit interval. These feed Maehara's proof of the Jordan curve theorem.
Plane := EuclideanSpace ℝ (Fin 2) and the circle is Metric.sphere (0:Plane) 1.
Main deliverables:
circleHomeoSphere/spherePlaneHomeoCircle— the bridge between Mathlib'sCircle(unit circle inℂ) andsphere (0:Plane) 1.param— the angle parametrizationℝ → sphere (0:Plane) 1, continuous,2π-periodic, with explicit fibers and surjective.arcHomeoUnitInterval— a closed arcparam '' Icc a b(witha < b,b - a < 2π) is homeomorphic tounitInterval.sphere_split— two distinct points cut the circle into two closed arcs, each≃ₜ unitInterval, with union the whole circle and intersection the two points.jordanCurve_split— transport ofsphere_splitacross a homeomorphismsphere (0:Plane) 1 ≃ₜ K.exists_proper_arc— a proper closed subset of the circle sits inside a proper closed arc≃ₜ unitInterval.
The plane ℝ².
Equations
Instances For
1. The circle model bridge #
A linear isometry equivalence ℂ ≃ₗᵢ[ℝ] Plane, from the standard orthonormal
basis of EuclideanSpace ℝ (Fin 2).
Equations
Instances For
The underlying Equiv between Mathlib's Circle and the unit sphere of the
plane, induced by complexLIE.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Circle model bridge (as requested): sphere (0:Plane) 1 ≃ₜ Circle.
Instances For
2. The angle parametrization #
The angle parametrization ℝ → sphere (0:Plane) 1, θ ↦ the plane point at
angle θ on the unit circle.
Equations
Instances For
The parametrization is surjective.
The parametrization is 2π-periodic.
2. Closed arc ≃ₜ unitInterval #
Closed arc ≃ₜ unitInterval. A closed arc param '' Icc a b with
a < b and b - a < 2π is homeomorphic to the unit interval.
Equations
- JordanCurve.Arcs.arcHomeoUnitInterval hab h = (JordanCurve.Arcs.arcHomeoIcc h).symm.trans (iccHomeoI a b hab)
Instances For
2b. Interior of an arc is path-connected #
Interior of an arc is path-connected. If A ≃ₜ unitInterval via e and two
points x, y ∈ A are the endpoints ({e x, e y} = {0, 1}), then A \ {x, y} — the
arc with its endpoints removed — is path-connected.
arc_interior_joinedIn. For an arc A ≃ₜ unitInterval via e whose two
endpoints are x, y ({e x, e y} = {0, 1}), any two interior points u, v ∈ A
(neither equal to x nor y) are joined by a path inside A \ {x, y}.
3. The two-point split #
Two-point split. Two distinct points x, y on the circle cut it into
two closed arcs A₁, A₂, each homeomorphic to the unit interval, whose union
is the whole circle and whose intersection is exactly {x, y}.
4. Transport across a homeomorphism to a Jordan curve #
Transport to a Jordan curve. Given a homeomorphism f from the circle to
a space K and two distinct points, the images of the two arcs split K into two
closed arcs ≃ₜ unitInterval meeting exactly at {f x, f y}.
5. A proper closed arc containing a proper closed set #
Proper arc containing a set. A proper closed subset C of the circle is
contained in a proper closed arc A (homeomorphic to the unit interval).
Toward the 2D Brouwer fixed point theorem #
We build the classical topological proof of the two-dimensional Brouwer fixed point theorem, in four phases:
- Phase 1 — the once-around loop on
AddCircle 1is not homotopic (rel endpoints) to the constant loop. This is the mathematical heart: it is proved from the coveringℝ → AddCircle 1via unique path lifting (IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel). - Phase 1.5 — transport of Phase 1 across
AddCircle 1 ≃ₜ Circle ≃ₜ sphere (0 : ℝ²) 1to obtain a non-nullhomotopic loop on the geometric circle. - Phase 2 — no retraction of the disk onto its boundary circle: a retraction would give a null-homotopy of the Phase 1.5 loop.
- Phase 3 — Brouwer for the closed unit disk (
brouwer_disk): a fixed-point-free self-map yields a retraction (ray construction). - Phase 4 — the general convex/compact/nonempty statement
brouwerFPT.
The plane ℝ².
Equations
Instances For
The covering map ℝ → AddCircle 1.
The once-around loop t ↦ ↑t in AddCircle 1.
Equations
- JordanCurve.Brouwer.acLoop = { toFun := fun (t : ↑unitInterval) => ↑↑t, continuous_toFun := JordanCurve.Brouwer.acLoop._proof_1 }
Instances For
The lift of acLoop to ℝ starting at 0: the identity t ↦ ↑t.
Equations
- JordanCurve.Brouwer.idLift = { toFun := fun (t : ↑unitInterval) => ↑t, continuous_toFun := JordanCurve.Brouwer.idLift._proof_1 }
Instances For
Phase 1. The once-around loop is not homotopic rel endpoints to the constant loop.
Phase 1.5 — transport to the geometric circle sphere (0 : ℝ²) 1 #
The base point of the sphere loop.
Instances For
The once-around loop on the geometric circle sphere (0 : ℝ²) 1.
Equations
- JordanCurve.Brouwer.sLoop = { toFun := ⇑JordanCurve.Brouwer.acToSphere, continuous_toFun := JordanCurve.Brouwer.sLoop._proof_1 }.comp JordanCurve.Brouwer.acLoop
Instances For
Phase 1.5. The once-around loop on the geometric circle is not homotopic rel endpoints to the constant loop.
Phase 2 — no retraction of the disk onto its boundary circle #
The straight-line contraction point (1-t)·(loop s) + t·base in the disk.
Equations
- JordanCurve.Brouwer.diskPt t s = (1 - ↑t) • ↑(JordanCurve.Brouwer.sLoop s) + ↑t • ↑JordanCurve.Brouwer.sBase
Instances For
The contraction as a continuous map into the disk.
Equations
- JordanCurve.Brouwer.diskMap = { toFun := fun (p : ↑unitInterval × ↑unitInterval) => ⟨JordanCurve.Brouwer.diskPt p.1 p.2, ⋯⟩, continuous_toFun := JordanCurve.Brouwer.diskMap._proof_2 }
Instances For
Phase 2. There is no retraction of the closed disk onto its boundary circle.
Phase 3 — Brouwer for the closed unit disk #
Given a fixed-point-free self-map f of the disk, the ray from f x through x
exits the boundary circle at a point ρ x; this ρ is a retraction, forbidden
by Phase 2.
The direction vector x - f x of the ray.
Equations
- JordanCurve.Brouwer.dvec f x = ↑x - ↑(f x)
Instances For
Quadratic coefficient A = ‖x - f x‖².
Equations
- JordanCurve.Brouwer.Acoef f x = inner ℝ (JordanCurve.Brouwer.dvec f x) (JordanCurve.Brouwer.dvec f x)
Instances For
Coefficient B = ⟪f x, x - f x⟫.
Equations
- JordanCurve.Brouwer.Bcoef f x = inner ℝ (↑(f x)) (JordanCurve.Brouwer.dvec f x)
Instances For
Coefficient C = ‖f x‖² - 1 ≤ 0.
Instances For
Discriminant B² - A·C ≥ 0.
Equations
Instances For
The (larger) root parameter t = (-B + √disc)/A.
Equations
Instances For
The exit point ρ x = f x + t·(x - f x) on the boundary circle.
Equations
- JordanCurve.Brouwer.rhoPt f x = ↑(f x) + JordanCurve.Brouwer.tparam f x • JordanCurve.Brouwer.dvec f x
Instances For
The exit point lies on the unit circle.
On the boundary circle, ρ is the identity.
Continuity of the retraction #
Phase 3. Brouwer's fixed point theorem for the closed unit disk.
Phase 4 — general nonempty compact convex sets #
Transfer of the fixed-point property along a homeomorphism.
Brouwer on an arbitrary closed ball (by rescaling) #
Rescaling homeomorphism closedBall 0 R ≃ₜ closedBall 0 1 (x ↦ R⁻¹ • x).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Brouwer for a closed ball of arbitrary positive radius.
Nearest-point projection onto a nonempty compact convex set #
Any nonempty compact convex set s ⊆ ℝ² is a retract of any closed ball
containing it, via the (nonexpansive, hence continuous) nearest-point
projection. This yields Brouwer for all such s uniformly — in particular the
degenerate empty-interior case is handled without any dimension reduction.
The 2D Brouwer fixed point theorem. Every continuous self-map of a
nonempty compact convex subset of ℝ² has a fixed point. This matches the
JordanCurve.BrouwerFPT interface used to discharge the Jordan curve theorem.
The set s is contained in a closed ball closedBall 0 R; the nearest-point
projection r : closedBall 0 R → s is a continuous retraction, so the self-map
incl ∘ f ∘ r of the ball has (by brouwer_ball) a fixed point x, whose
coordinates lie in s, whence r x is a fixed point of f.
Counting plumbing for the Jordan curve theorem #
Pure-topology lemmas, independent of any geometry, used to turn the statement
"the complement of the curve has exactly two connected components" into the
numerical fact Nat.card (ConnectedComponents …) = 2.
The geometry side works with connectedComponentIn S x for S : Set Plane the
(open, nonempty) complement of the curve, and with two distinguished points in
the two components. This file provides:
nat_card_connectedComponents_eq_two— from two points in distinct components together covering everything, concludeNat.card (ConnectedComponents X) = 2.connectedComponents_subtype_eq_iff— the bridge identifying equality of classes of subtype points with equality ofconnectedComponentIn.
If a space X has two points a, b lying in distinct connected components
and every point's component is one of those two, then X has exactly two
connected components.
Bridge lemma. For two points x, y of a subset S, the connected
components of the corresponding subtype points agree iff their
connectedComponentIn S subsets agree. This lets the geometry side, which
phrases things via connectedComponentIn S, feed
nat_card_connectedComponents_eq_two.
The (continuous) Jordan Curve Theorem, via Brouwer — Maehara's proof #
Target (lean-eval jordan_curve, pure Mathlib): a continuous injection
r : S¹ → ℝ² has a complement with exactly two connected components.
Strategy (Maehara, The Jordan curve theorem via the Brouwer fixed point
theorem, Amer. Math. Monthly 1984). Reduce to the Brouwer fixed point theorem,
taken here as an explicit interface BrouwerFPT (to be discharged from upstream
Mathlib — PR #36770 is landing Brouwer — or built separately). The reduction uses:
- Lemma 2 (crossing) — two transversal paths in a rectangle must meet; proved directly from Brouwer via an explicit map of the square to its boundary.
- Lemma 1 — if
ℝ²∖Jis disconnected, each component hasJas its boundary; via the Tietze extension theorem + Brouwer. - Main construction — using the farthest pair
a,b ∈ Jand the pointsl,m,p,qon a vertical segment, showℝ²∖Jhas exactly one bounded component; with the unique unbounded component that gives exactly two.
This file is imported by the top-level JordanPick module and is complete:
sorry-free, with #print axioms JordanCurve.jordan_curve reporting only
[propext, Classical.choice, Quot.sound].
The plane ℝ² as used by the eval problem.
Equations
Instances For
Brouwer fixed point theorem (interface). Every continuous self-map of a
nonempty convex compact subset of the plane has a fixed point. Discharged
separately (upstream Mathlib PR #36770, or a standalone build). All of Maehara's
argument is BrouwerFPT → ….
Equations
Instances For
Lemma 2 (crossing lemma, Maehara). Two continuous paths in a rectangle
[a,b]×[c,d], one running from the left edge to the right edge (h), the other
from the bottom edge to the top edge (v), must meet. Proved directly from
Brouwer: if they were disjoint, the explicit normalized map
F(s,t) = ((v₁ t − h₁ s)/N, (h₂ s − v₂ t)/N) (with N the sup-norm of
h s − v t) sends the parameter square [-1,1]² to its boundary with no fixed
point. Coordinates are p 0, p 1 of p : Plane.
Foundational topology of a Jordan curve J = range r #
A Jordan curve is J = range r for r : S¹ → ℝ² continuous and injective. Here we
collect the purely topological facts about J and its complement that Maehara's
argument needs, independent of Brouwer:
The plane has rank 2 > 1; the engine for connectivity of ball-complements.
Task 1. The Jordan curve J = range r is compact (continuous image of the
compact circle S¹).
Task 1. The Jordan curve J = range r is closed (compact in a Hausdorff
space).
Task 2. The complement of the Jordan curve is open.
Task 3. A continuous injection of the compact circle into the plane is a closed embedding.
Task 3. r is a topological embedding.
Task 3. The Jordan curve J = range r is homeomorphic to the circle S¹.
Equations
- JordanCurve.jordanCurveHomeo r hcont hinj = ⋯.toHomeomorph
Instances For
PRELIM (a). Jᶜ has an unbounded connected component: pick any point in the
cobounded exterior {x | R < ‖x‖} of a ball containing J; that exterior is
connected, lies in Jᶜ, and is unbounded, so the component containing it is
unbounded.
PRELIM (a). Any two unbounded components of Jᶜ coincide: each unbounded
component must meet the connected cobounded exterior {x | R < ‖x‖}, which therefore
lies in a single component.
PRELIM (b). Each connected component of Jᶜ is open (Jᶜ is open and the
plane is locally connected).
PRELIM (b). Each connected component of Jᶜ is path-connected (it is open
and connected in the locally path-connected plane).
Maehara's Lemma 1 core: "an arc does not separate the plane". If A ⊆ ℝ²
is an arc (homeomorphic to the unit interval [0,1]) then its complement Aᶜ is
connected.
Proof (Brouwer + Tietze). If Aᶜ were disconnected it would have a bounded
component (there is a unique unbounded one, containing the cobounded exterior of a
disc through A); pick a point o in it. Since A ≃ₜ [0,1] and [0,1] is an
absolute retract (TietzeExtension), the identity A → A extends to a retraction
ρ : ℝ² → A. Glue ρ on the component K ∋ o with the identity elsewhere: the two
pieces agree on frontier K ⊆ A where ρ = id, giving a continuous
Q : ℝ² → ℝ²∖{o} that is the identity outside K. On a large disc D = closedBall o R
containing A and K, the map z ↦ o - R·(Q z - o)/‖Q z - o‖ (antipodal radial
projection about o) is a fixed-point-free continuous self-map of D, contradicting
Brouwer.
Maehara's Lemma 1. If ℝ²∖J is disconnected, each component has the whole
Jordan curve J = range r as its boundary. We state (and prove) the sharper
unconditional form: for any x in the complement, the frontier of its connected
component equals range r.
Proof (arc argument, via arc_not_separates). Write U for the component of x.
Always frontier U ⊆ range r (a boundary point outside the curve would lie in some
component of the open complement, forcing it into U — impossible for a frontier
point). If frontier U ⊊ range r, transport the proper closed set
C = r⁻¹(frontier U) ⊊ S¹ to a proper closed arc A₀ (via exists_proper_arc) and
push forward to A = r '' A₀, a proper arc with frontier U ⊆ A ⊊ range r. Then
Aᶜ is connected (arc_not_separates), yet U and (closure U)ᶜ split it into two
nonempty relatively open pieces (x ∈ U; a point of range r ∖ A lies in
(closure U)ᶜ) — contradicting connectedness.
Normalization foundation (Maehara farthest-pair setup) #
We prepare Maehara's WLOG normalization: the diameter of J = range r is realized
by a farthest pair a, b, and a similarity homeomorphism T moves a ↦ !₂[-1,0],
b ↦ !₂[1,0], scaling every distance by the fixed factor 2 / dist a b. This
reduces the geometric core (step_A, step_B) to normalized statements in which
the farthest pair sits at (±1, 0).
Task 1 (farthest pair). The compact curve range r contains a pair a, b
realizing the diameter of J, and a ≠ b (as r is injective on the sphere, which
has at least two points).
Setup lemmas for the normalized frame (Steps A, B) #
Setup 1 (the "lens"). In the normalized frame with the farthest pair at
a = !₂[-1,0], b = !₂[1,0] and diameter 2 (hfar), the whole curve lies in
the rectangle [-1,1] × [-2,2]. For z ∈ range r, both dist z a ≤ 2 and
dist z b ≤ 2, i.e. (z 0+1)²+(z 1)² ≤ 4 and (z 0-1)²+(z 1)² ≤ 4; these force
z 0 ∈ [-1,1] and (adding them) (z 0)²+(z 1)² ≤ 3, hence z 1 ∈ [-2,2].
arc_path (reusable reparametrization). A path in a set S ⊆ Plane
joining a to b can be reparametrized to a map h : ℝ → Plane on the interval
[-1,1], with h (-1) = a, h 1 = b, continuous on [-1,1], and staying in S.
This is exactly the shape required by the crossing lemma for the horizontal path
(endpoints on the left/right edges of a rectangle).
Setup 2 (segment meets curve). The vertical segment from s = !₂[0,-2] to
n = !₂[0,2] meets the curve. Proof via the crossing lemma with horizontal path
h a curve-path from a = !₂[-1,0] to b = !₂[1,0] (the curve is path-connected,
reparametrized by arc_path) staying in the rectangle [-1,1]×[-2,2]
(normalized_subset_rectangle), and vertical path v t = !₂[0, 2t] running from the
bottom edge y=-2 to the top edge y=2. Delivers a curve point on the vertical
axis.
Setup 3 (top of the axis). The intersection of the curve with the vertical
axis Jax = {p ∈ range r | p 0 = 0} is compact (closed subset of the compact
curve) and nonempty (segment_meets_curve), hence attains its y-maximum at some
point l ∈ range r with l 0 = 0.
Setup 4 (arc split at a, b). The curve range r splits at the farthest
pair a = !₂[-1,0], b = !₂[1,0] into two closed arcs J_n, J_s ⊆ Plane, each
≃ₜ unitInterval, with J_n ∪ J_s = range r and J_n ∩ J_s = {a, b}, labelled so
that the y-topmost axis point l lies in J_n.
Path-concatenation infrastructure and Maehara's interior points #
The tools below package repeated use of the crossing lemma: any bottom-to-top
path in the normalized rectangle meets each arc (vertical_meets_arc), together with
the plumbing (concatPath2, concatPath3) that glues path pieces into one
continuous path on [-1,1] whose image is the union of the pieces.
An arc J ⊆ Plane homeomorphic to unitInterval is path-connected.
An arc J ≃ₜ unitInterval joins any two of its points inside J.
Key reusable tool. Any path v running from the bottom edge (v (-1) 1 = -2)
to the top edge (v 1 1 = 2) of the normalized rectangle [-1,1]×[-2,2] must meet an
arc J that joins the left point a = !₂[-1,0] to the right point b = !₂[1,0] inside
the rectangle. Immediate from crossing, using arc_path for the horizontal path.
Path concatenation (2 pieces). Two path pieces on [-1,1] that chain up
(f 1 = g (-1)) glue to one path c on [-1,1] from f (-1) to g 1, whose image
is contained in the union of the pieces' images.
Path concatenation (3 pieces). Three chained path pieces on [-1,1] glue to
one path c on [-1,1] from f (-1) to h 1, with image in the union of the three
pieces' images.
Path concatenation (5 pieces). Five chained path pieces on [-1,1] glue to one
path c on [-1,1] from f1 (-1) to f5 1, with image in the union of the five
pieces' images.
Interior point m. The intersection J_n ∩ axis (axis = {p | p 0 = 0}) is
compact and nonempty (it contains l), hence attains its y-minimum at a point m.
The vertical segment m → s meets J_s. With s = !₂[0,-2] (below the
rectangle's bottom edge), the axis segment from the interior point m ∈ J_n down to
s must cross the southern arc J_s. Proof by contradiction: were it disjoint from
J_s, the concatenation s → m (axis), m → l (a path inside J_n \ {a,b}),
l → n (axis, n = !₂[0,2]) would give a bottom-to-top path in the rectangle
avoiding J_s, contradicting vertical_meets_arc (J_s joins a to b). The
crossing point lies on the segment, so it sits on the axis at height ≤ m 1.
Maehara's construction points. Bundles the five points of Maehara's figure
on the vertical axis x = 0:
l— the topmost intersection of the axis with the curve (inJ_n);m— the lowest point ofJ_non the axis;p— the highest point ofJ_son the axis lying at or belowm(the top of the southern arc on the segmentm → s, viams_meets_Js);q— the lowest point ofJ_son the axis;z₀— the midpoint!₂[0,(m 1 + p 1)/2]ofmandp.
The established y-ordering is q 1 ≤ p 1 ≤ z₀ 1 ≤ m 1 ≤ l 1. (Note p is the
J_s-max restricted to heights ≤ m 1; this is what makes p 1 ≤ m 1 — hence
the placement of z₀ between p and m — provable at this stage.)
First-exit lemma (A.1). A path α on [0,1] starting inside an open set O
and ending outside a closed superset C ⊇ O has a first exit time tw ∈ (0,1]:
α tw lies in the frontier layer C \ O, and α u ∈ O for all u < tw.
Curve meets the rectangle boundary only on the axis (A.2). Any curve point on
the frontier of the normalized rectangle [-1,1]×[-2,2] has y = 0 (so it is a or
b). The "lens" bound (p 0±1)²+(p 1)² ≤ 4 rules out the top/bottom edges outright
and pins the left/right edges to y = 0.
Lower boundary arc (A.2). The part of the rectangle frontier with y < 0 is
path-connected, contains the bottom axis point !₂[0,-2], lies in the rectangle, and
avoids the curve; moreover any frontier point with y < 0 lies in it.
Upper boundary arc (A.2). The part of the rectangle frontier with y > 0 is
path-connected, contains the top axis point !₂[0,2], lies in the rectangle, and
avoids the curve; moreover any frontier point with y > 0 lies in it.
Maehara Step A (normalized). The geometric core in normalized coordinates:
the farthest pair sits at !₂[-1,0], !₂[1,0] (so the diameter is 2).
Maehara Step A (geometric core). The complement ℝ²∖J of a Jordan curve
has at least one bounded connected component. Reduced to the normalized version
step_A_normalized via the farthest-pair similarity T.
Maehara Step B (geometric core). Bounded components of ℝ²∖J are unique.
Reduced to the normalized version step_B_normalized via the farthest-pair
similarity T.
The Jordan curve theorem reduced to Brouwer (Maehara). The eval jordan_curve
follows by discharging BrouwerFPT. Given the two geometric core facts — existence
(step_A_exists_bounded) and uniqueness (step_B_bounded_unique) of a bounded
component — together with the unique unbounded component (exists_unbounded_component,
unbounded_component_unique), the complement has exactly two components.
Jordan curve theorem (the eval statement).
Metric variation of a continuously differentiable curve #
For a continuously differentiable curve in a complete real normed space, its metric total variation equals the integral of the norm of its derivative.
The upper bound sums the fundamental theorem of calculus over finite partitions. For the reverse bound, the curve is clamped to the compact parameter interval. The resulting globally Lipschitz curve has bounded variation, and its associated vector measure has density given by the derivative on the interval.
Main result #
TauCeti.eVariationOn_eq_lintegral_enorm_derivWithin: metric variation equals the integral of the derivative norm.
Roadmap alignment #
This module advances the Regular reparametrization and limits target under
Layer 0: the reconciled Riemannian distance in
roadmap/HopfRinow/README.md. It supplies the vector metric-variation
identity used as an analytic prerequisite by the lower-semicontinuity
comparison; this file does not claim the broader
Hopf--Rinow dependency path.
Provenance #
The partition-comparison architecture follows
DoCarmoLib/Riemannian/Geodesic/HopfRinow/EVariationLePathELength.lean in the
Apache-2.0 frenzymath/Poincare-Conjecture source at revision
24f32e4d600878bfaac6bc2f2f9324175571c321. That source proves the forward
comparison with Riemannian path length. The reverse derivative-integral
comparison here is a Tau Ceti proof using Mathlib's clamped-curve and
vector-measure APIs; it is not asserted to be present in that source.
References #
- M. P. do Carmo, Riemannian Geometry, Chapter 7, Section 2.
- The source-first Lean snapshot above, revision
24f32e4d600878bfaac6bc2f2f9324175571c321, supplies the partition architecture viaeVariationOn_le_pathELength; the reverse inequality is original to this module.
Original authors: The Tau Ceti contributors, Archon Horizon (claude+codex), Axel Delaval, Chunlei Liu, Jinxuan Chen, Wanxu Yang, Zekun Sheng, Yuxuan Liao, Jie Xu.
For a C¹ curve in a real normed space, metric total variation is bounded
by the integral of the norm of its derivative.
For a C¹ curve in a complete real normed space, the integral of the norm
of its derivative is bounded by its metric total variation.
The metric total variation of a C¹ curve in a complete real normed space
equals the integral of the norm of its derivative.
The exterior of a closed ball is preconnected #
In a real normed space of dimension at least two the complement of a closed ball is preconnected:
it is the union, over the radii M exceeding the ball's, of the spheres of radius M, strung
together along a single ray from the centre.
The consequences for bounded sets — uniqueness of the unbounded component and the filled-hull
alternative — are in TauCeti/Analysis/Normed/Module/FilledHull.lean.
Main results #
TauCeti.isPreconnected_compl_closedBall— the exterior of a closed ball is preconnected in a real normed space of dimension at least two.
This is a prerequisite of the planar-separation step of the ConformalMapping roadmap (L5).
References #
- Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
The exterior of a closed ball is preconnected in a real normed space of dimension at least two.
Strict half-spaces of a real normed space are unbounded #
A strict half-space {y | φ y < u} cut out by a nonzero linear functional holds points of
arbitrarily large norm, and is therefore unbounded. Linearity alone suffices: φ need not be
continuous, so the results apply to a discontinuous functional on an infinite-dimensional space.
For such a φ the set need not be topologically open, which is why it is called strict rather
than open here.
Main results #
TauCeti.exists_apply_lt_and_lt_normandTauCeti.exists_lt_apply_and_lt_norm— either side of a nonzero linear functional holds points of arbitrarily large norm.TauCeti.not_isBounded_halfSpace_ltandTauCeti.not_isBounded_halfSpace_gt— either strict half-space is unbounded.
A strict half-space contains points of arbitrarily large norm. For a nonzero linear
functional φ, every bound u and every radius R admit a y with φ y < u and R < ‖y‖.
Linearity suffices; φ need not be continuous.
The other side of a nonzero linear functional also contains points of arbitrarily large
norm: every bound u and radius R admit a y with u < φ y and R < ‖y‖.
A strict half-space cut out by a nonzero linear functional is unbounded. No radius bounds
{y | φ y < u}. Linearity suffices; φ need not be continuous.
The half-space on the other side of a nonzero linear functional is unbounded. No radius
bounds {y | u < φ y} either. Linearity suffices; φ need not be continuous.
Limits of total variation bounds #
This file transfers eventual upper bounds on the total variations of a family of maps to a
liminf bound on the total variation of a pointwise limit.
Main results #
TauCeti.eVariationOn_le_liminf_of_eventually_le: an eventual bound on the total variations of a family of maps bounds the total variation of a pointwise limit by theliminfof the bounds.
The metric variation of a path in a subtype is unchanged by applying its coercion.
If the total variations of the maps F i on s are eventually bounded by u i, then the
total variation on s of a pointwise limit of the F i is at most liminf u.
External libraries #
The modules from Mathlib, lean-pool, TauCeti and jordan_pick that the development uses beyond its own files, collected in one place.
Three frontier lemmas: straddling, splitting a domain in two, and clinging to it from inside #
Three elementary facts about frontier, each the topological core of a step that a boundary
argument would otherwise carry out inside a concrete space.
A connected set that straddles a set meets its frontier #
A preconnected set that meets both a set V and its complement must meet frontier V: it cannot
cross from the inside of V to the outside without touching the boundary. This is the
intermediate-value principle in its purely topological form, and it is the mechanism by which a
path leaving a set produces a boundary point of that set.
Mathlib records the two extreme cases — frontier_eq_empty_iff and nonempty_frontier_iff say
that in a preconnected space the frontier of V is empty exactly when V is ∅ or univ — but
not this relative form, which is the one an argument along a segment or a path needs. No hypothesis
is placed on V; only preconnectedness of the straddling set is used.
The proof is the standard clopen argument: the complement of frontier V is the disjoint union of
the two open sets interior V and interior Vᶜ (compl_frontier_eq_union_interior), so a
preconnected set avoiding the frontier lies inside one of them, and then it misses V entirely or
is contained in V entirely.
Where the boundary of the image of one side of a split domain can lie #
Split a set U into two pieces s and t that a map f sends to disjoint open sets, plus a
remainder u. Then frontier (f '' s) ⊆ f '' u ∪ frontier (f '' U)
(TauCeti.frontier_image_subset_image_union_frontier_image): the boundary of the image of one side
consists of images of the remainder — the cut — and of boundary points of the whole image, and of
nothing else.
The proof is a three-way case split. A point p of frontier (f '' s) lies in closure (f '' U),
so if it is not on frontier (f '' U) it is a value f w with w in one of the three covering
sets. It cannot come from s, since f '' s is open and therefore disjoint from its own frontier;
and it cannot come from t, since f '' t is then an open neighbourhood of p, which must meet
f '' s, contradicting disjointness of the two images. So w ∈ u.
The source carries no topology; the sides enter topologically only through their images, which are
asked to be open and disjoint, and that is all the argument uses of them. What is asked of the
sides themselves is purely set-theoretic: s ⊆ U and the covering U ⊆ s ∪ t ∪ u. In particular
t need not lie in U, and neither side need be open or disjoint from the other. A consumer whose
map is open and injective on two disjoint open sides supplies both image hypotheses, as the
conformal one below does through the open mapping theorem and Disjoint.image.
What a set's frontier sees of a subset #
A subset A of a set V cannot reach frontier V except through its own frontier:
(TauCeti.frontier_inter_closure_eq_frontier_inter_frontier). The reason is that closure A is
A ∪ frontier A, and a point of A on frontier V is already on frontier A: it is adherent to
A and, since interior A ⊆ interior V, it is not interior to A. So the part of frontier V
that A clings to has two interchangeable descriptions — as the reach of closure A, and as the
meeting of two frontiers. The first is the one an argument about limits of points of A produces;
the second is the one a diameter estimate consumes, frontier being where the estimates of a
domain-splitting argument live.
Consumers #
All three lemmas serve layer L5 of TauCetiRoadmap/ConformalMapping/README.md, Carathéodory's
boundary correspondence. The first does so through
TauCeti/Analysis/Normed/Module/DiamFrontier.lean: a ray leaving a bounded set crosses its
frontier, which is what makes the frontier of such a set as wide as the set itself. The second is
the splitting step of TauCeti/Analysis/Complex/Conformal/CutDiameter.lean, where s and t are
the two sides of a circular crosscut of a domain and u is the crosscut arc. The third is what
lets TauCeti/Analysis/Complex/Conformal/ClusterSet.lean identify the boundary piece that one
side of such a crosscut cuts off, whose description as a union of cluster sets is naturally a
statement about a closure. Nothing here is specific to those uses; no lemma mentions a metric, let
alone a holomorphic map.
Main results #
IsPreconnected.inter_frontier_nonempty— a preconnected set meeting both a set and its complement meets the frontier of that set.TauCeti.frontier_image_subset_image_union_frontier_image— for a set split into two sides with disjoint open images plus a remainder, the frontier of the image of the side lying in that set lies on the image of the remainder and on the frontier of the image of the whole.TauCeti.frontier_inter_closure_eq_frontier_inter_frontier— the frontier of a set meets the closure of a subset exactly where it meets that subset's frontier.
A preconnected set that meets both a set and its complement meets its frontier. If S is
preconnected and contains a point of V and a point outside V, then S meets frontier V.
Nothing is assumed about V; the argument is that (frontier V)ᶜ is the union of the two disjoint
open sets interior V and interior Vᶜ, so a preconnected set missing the frontier is confined to
one of them and therefore cannot straddle V.
The boundary of the image of one side of a split domain lies on the image of the remainder
and on the boundary of the image of the domain. If U is covered by two sets s, t with
disjoint open images together with a third set u, and s ⊆ U, then
frontier (f '' s) ⊆ f '' u ∪ frontier (f '' U).
The conclusion is about s, the side that is asked to lie in U. The argument treats the two
sides alike apart from that, so a consumer with t ⊆ U in hand bounds t as well by swapping
their roles.
A frontier point of f '' s lies in closure (f '' U), so if it is not a frontier point of
f '' U it is a value f w with w in one of the three covering sets: w ∈ s would place it
inside the open set f '' s, which is disjoint from its own frontier, and w ∈ t inside the open
set f '' t, which meets f '' s because the point is in its closure, contradicting disjointness
of the two images. So w ∈ u.
The source carries no topology at all: U and the three sets covering it are constrained only by
the two set-theoretic hypotheses hsU : s ⊆ U and hcov : U ⊆ s ∪ t ∪ u, while every topological
hypothesis, and the conclusion, lives in the target. In particular t need not lie in U, and
the two sides need be neither open nor disjoint nor separated by injectivity — only their images
need be open and disjoint, which is what the argument uses and what an injective open map on two
disjoint open sides supplies.
The frontier of a set meets the closure of a subset exactly where it meets that subset's
frontier. For any A ⊆ V,
Writing closure A as A ∪ frontier A, the first piece brings nothing new: a point of A on
frontier V is adherent to A and is kept out of interior A by interior A ⊆ interior V, so it
already lies on frontier A. Only the inclusion A ⊆ V is used — V need be neither open nor
closed, and A is arbitrary.
So the part of frontier V that A clings to may be described either as its meeting with
closure A or as its meeting with frontier A. An argument about limits of points of A produces
the first; a diameter estimate obtained by splitting V into pieces consumes the second.
Filling in the bounded complementary components of a set #
The filled hull TauCeti.filledHull K of a subset K of a topological space with a bornology
is K together with the bounded connected components of its complement: the points whose component
in Kᶜ is bounded. Points of K qualify vacuously, their component in Kᶜ being empty. Filling a
circle gives the closed disc it bounds; filling a segment, or any set whose complement is connected
and unbounded, changes nothing.
This file is the topological layer: the definition and the structural facts, which ask only for a
topology and a bornology, being about components and boundedness and nothing else. That filling
does not make a set wider needs a real normed space and lives in
TauCeti/Analysis/Normed/Module/FilledHull.lean.
The shape in which the structural side is spent is IsPreconnected.subset_filledHull: a
preconnected set disjoint from K is trapped inside the filled hull as soon as it meets it, since
it then lies in a single bounded component. Together with the width bound of the normed file it
says that a connected set that a small K cuts off from infinity is itself small, with no
regularity asked of K; that composite is IsPreconnected.diam_le_diam_of_disjoint there.
The negation of membership — that the component of a point in the complement of K is unbounded
— already occurs, unfolded, in the winding-number layer: it is the hypothesis of
TauCeti.Contour.windingNumber_eq_zero_of_unbounded_component in
TauCeti/Analysis/Contour/Winding/UnboundedComponent.lean and of its cycle form
TauCeti.Contour.Cycle.windingNumber_eq_zero_of_unbounded_component in
TauCeti/Analysis/Contour/Cycle/Winding.lean, both of which say that the winding number vanishes
off the filled hull of the trace. Those statements are left as they stand: they are about the
unbounded side, which needs no name, whereas everything here is about the filled side.
The hull is deliberately not claimed to be closed, connected, or idempotent — none of which is
needed downstream, and the first two of which fail without hypotheses on K.
Roadmap role #
Plane separation for Jordan curves was the open frontier item of layer L5 of
TauCetiRoadmap/ConformalMapping/README.md, the Carathéodory boundary correspondence. The
enclosure step now runs through IsPreconnected (K \ {f z₀}) and the winding-number two-sidedness
theorem
(TauCeti.image_inter_ball_subset_filledHull_of_diam_lt_of_isPreconnected_sdiff_singleton),
which IsJordanCurve.isPathConnected_sdiff_singleton discharges; Caratheodory.lean is
unconditional.
The inside of J is filledHull J \ J in the vocabulary defined here. Nothing here assumes
separation, or any other regularity of K.
Main results #
TauCeti.filledHull— the filled hull, andTauCeti.subset_filledHull,TauCeti.filledHull_monoits two structural properties.TauCeti.filledHull_eq_self— filling a set whose complement is preconnected and unbounded changes nothing.IsPreconnected.subset_filledHull— a preconnected set disjoint fromKthat meets the filled hull lies in it.TauCeti.subset_filledHull_of_frontier_subset— a bounded set whose frontierKswallows lies in the filled hull, with no connectivity asked of it.
The filled hull of a set K: the points whose connected component in the complement of K
is bounded. Equivalently, K together with the bounded connected components of Kᶜ; a point of
K belongs because its component in Kᶜ is empty.
Equations
- TauCeti.filledHull K = {x : E | Bornology.IsBounded (connectedComponentIn Kᶜ x)}
Instances For
A set lies in its filled hull. For x ∈ K the component of x in Kᶜ is empty, and the
empty set is bounded.
Filling is monotone. Enlarging K shrinks the complement, hence shrinks each component of
it, hence can only turn unbounded components into bounded ones.
Filling changes nothing when the complement is connected and unbounded. The complement is
then a single component and that component is unbounded, so no point outside K is filled in. This
is the case of a segment in the plane, and of any set that does not separate the space.
A preconnected set that a set cuts off from infinity lies in its filled hull. If S is
preconnected and disjoint from K, then S lies in a single connected component of Kᶜ; meeting
the filled hull says that component is bounded, so all of S is in the hull.
A bounded set whose frontier lies in K is cut off from infinity by K. A point of
S \ K lies in interior S, since every non-interior point of S lies on frontier S ⊆ K. Its
connected component in Kᶜ cannot leave interior S: were it to, it would meet
frontier (interior S) ⊆ frontier S ⊆ K by IsPreconnected.inter_frontier_nonempty,
while lying in Kᶜ. So that component is bounded because S is. Points of S ∩ K lie in the
filled hull directly.
Unlike IsPreconnected.subset_filledHull this asks nothing of the connectivity of S and
nothing about the hull being met, at the price of asking K to swallow the whole frontier — the
same trade as between TauCeti.diam_le_diam_of_frontier_subset and
IsPreconnected.diam_le_diam_of_disjoint.
The width of a filled hull #
The filled hull TauCeti.filledHull K — K together with the bounded connected components of its
complement — is defined in TauCeti/Topology/FilledHull.lean, where it needs only a topology and a
bornology. In a real normed space the one substantial fact is that filling does not make a set
wider:
TauCeti.filledHull_subset_closedConvexHull—filledHull K ⊆ closedConvexHull ℝ K,
whence TauCeti.diam_filledHull: a set and its filled hull have the same diameter. The
mechanism is separation: a point x outside the closed convex hull of K is cut off
from it by a continuous linear functional (geometric_hahn_banach_point_closed), and the open
half-space {y | φ y < u} so produced is a convex — hence preconnected — subset of Kᶜ containing
x, and it is unbounded (TauCeti.not_isBounded_halfSpace_lt). So the component of x in Kᶜ is
unbounded and x is not in the filled hull. Nonemptiness of K is needed only to know that
φ ≠ 0; for K = ∅ and a zero-dimensional space the convex-hull statement is false, the hull then
being everything and the convex hull empty. The diameter statements survive that case
unhypothesised, because filledHull ∅ is empty in a nontrivial space
(TauCeti.filledHull_empty) and the single point of the zero space otherwise, of diameter 0
either way.
Because the width of a filled hull is controlled, so is that of anything inside it, and the shape
in which this is spent is IsPreconnected.subset_filledHull: a preconnected set disjoint from K
is trapped inside the filled hull as soon as it meets it. Their composite,
IsPreconnected.diam_le_diam_of_disjoint, says that a connected set that a small K cuts off
from infinity is itself small, with no regularity asked of K.
Roadmap role #
The filled hull is the vocabulary in which the enclosure step of layer L5 of
TauCetiRoadmap/ConformalMapping/README.md is stated. That step is now unconditional: the
preconnectedness/winding-number route in TauCeti/Analysis/Complex/Conformal/Crosscut/Inside.lean
places one image piece of a crosscut in the filled hull without plane separation. In the diameter
bound that follows, TauCeti/Analysis/Complex/Conformal/Crosscut/SmallJordanCurve.lean encloses a
short image crosscut in an arbitrarily small Jordan curve J, and
IsPreconnected.diam_le_diam_of_disjoint makes the cut-off piece no wider than J.
This is a different route to a diameter bound from TauCeti.diam_le_diam_of_frontier_subset of
TauCeti/Analysis/Normed/Module/DiamFrontier.lean, which bounds a set by any bounded set
containing its frontier: there the enclosing set must be known to contain the whole frontier, here
only that the set is cut off from infinity. The frontier route is the special case of the enclosure
route obtained from TauCeti.subset_filledHull_of_frontier_subset; the enclosure route does not
require the whole frontier to be caught.
Generality #
The width statements are stated for an arbitrary real normed space — nothing about the plane is used, and the separation argument is the general Hahn–Banach one.
Main results #
TauCeti.filledHull_subset_closedConvexHull— a filled hull lies in the closed convex hull.TauCeti.diam_filledHullandTauCeti.isBounded_filledHull— filling preserves the diameter, and a filled hull is bounded exactly when the set filled is.TauCeti.diam_le_diam_of_subset_filledHullandIsPreconnected.diam_le_diam_of_disjoint— a set inside the filled hull of a boundedK, in particular a preconnected set thatKcuts off from infinity, is no wider thanK.TauCeti.isBounded_closedConvexHull,TauCeti.diam_closedConvexHull— the closed forms of the two convex-hull facts the width argument runs on.TauCeti.connectedComponentIn_compl_eq_of_unbounded_component— the unbounded connected component of the complement of a bounded set is unique (dimension at least two).TauCeti.mem_filledHull_or_mem_filledHull_of_notMem_connectedComponentIn— of two points in different components, at least one lies in the filled hull (dimension at least two).
A closed convex hull is bounded exactly when the set is. The closed form of
isBounded_convexHull, the closure adding nothing.
Taking the closed convex hull preserves the diameter. The closed form of convexHull_diam,
the closure adding nothing by Metric.diam_closure.
The filled hull lies in the closed convex hull. A point outside the closed convex hull of a
nonempty K is separated from it by a continuous linear functional; the open half-space this
produces is convex, avoids K, and is unbounded, so the component of the point in Kᶜ is
unbounded.
Nonemptiness of K is what forces the separating functional to be nonzero, and so the half-space to
be unbounded; without it the statement fails in the zero space, where filledHull ∅ = univ.
The filled hull of the empty set is empty in a nontrivial space: the whole space is
connected and unbounded, so every component of ∅ᶜ = univ is unbounded.
A filled hull is bounded exactly when the set filled is. One direction is
TauCeti.subset_filledHull; the other holds because the hull lies in the closed convex hull.
Filling preserves the diameter. The hull contains K, and for nonempty K it is contained
in the closed convex hull of K, which by TauCeti.diam_closedConvexHull is exactly as wide as
K; filledHull ∅ is a subsingleton, of diameter 0 like ∅ itself. An unbounded K has an
unbounded hull by TauCeti.isBounded_filledHull, and both diameters are then 0.
Anything a bounded K cuts off from infinity is no wider than K. A set inside the filled
hull is no wider than the hull by Metric.diam_mono, and the hull is no wider than K by
TauCeti.diam_filledHull.
A preconnected set that a bounded K cuts off from infinity is no wider than K. If S is
preconnected, disjoint from K, and meets the filled hull of K, then it lies inside that hull by
IsPreconnected.subset_filledHull, which is no wider than K by
TauCeti.diam_filledHull. No regularity is asked of K.
The unbounded component of the complement of a bounded set is unique in a real normed space of dimension at least two.
Two points in different components of the complement of a bounded set cannot both lie outside the filled hull in a real normed space of dimension at least two.
Local connectedness of continuous images of compact spaces #
Local connectedness is not preserved by continuous images in general — every metric space is a
continuous image of a discrete one — but it is preserved by quotient maps, and hence by the
continuous images that are automatically quotient maps: those of a compact space in a Hausdorff
one. This file proves that, in the type-level form and in the set-level form
TauCeti.locallyConnectedSpace_image_of_isCompact that a subset of a topological space needs.
The quotient step itself is Mathlib's. Topology.IsCoinducing.locallyConnectedSpace states that
a topology coinduced by a locally connected one is locally connected, which reaches quotient maps
through IsQuotientMap.isCoinducing and is strictly more general, since coinducing does not ask
for surjectivity. What is added here is the passage from that to a continuous surjection out of a
compact space, which is closed and therefore a quotient map.
The intended consumer is layer L5 of the conformal-mapping roadmap, Carathéodory's boundary
correspondence: a conformal map that extends continuously to the closure of its domain carries a
locally connected boundary to a locally connected boundary, which is the necessary half of
Carathéodory's continuity theorem. That application is in
TauCeti/Analysis/Complex/Conformal/LocallyConnectedBoundary.lean; nothing here is specific to it.
Main results #
TauCeti.locallyConnectedSpace_of_continuous_surjective— the continuous image of a compact locally connected space in a Hausdorff space is locally connected.TauCeti.locallyConnectedSpace_image_of_isCompact— the set-level form:f '' sis locally connected for a compact, locally connectedson whichfis continuous.
References #
- Mathlib,
Mathlib.Topology.Connected.LocallyConnected,Topology.IsCoinducing.locallyConnectedSpace: a topology coinduced by a locally connected topology is locally connected. This is the quotient-map result applied below.
The continuous image of a compact locally connected space in a Hausdorff space is locally
connected. A continuous surjection out of a compact space onto a Hausdorff one is closed, hence
a quotient map, hence coinducing, so Topology.IsCoinducing.locallyConnectedSpace applies.
The set-level form: a compact, locally connected set has locally connected continuous
images. Stated with the subtype topologies on s and on f '' s, which is how a boundary or a
closure of a subset of a normed space is met in practice.
Jordan curves #
A Jordan curve — a simple closed curve — is a subset of a topological space homeomorphic to
the circle. This file introduces the predicate TauCeti.IsJordanCurve and its basic API.
The circle is Mathlib's Circle, the unit circle of ℂ as a topological group; the notion itself
is purely topological, so TauCeti.IsJordanCurve is stated for a subset of an arbitrary
topological space. ℂ is mentioned only by the two concrete curves towards the end of the file:
the model curve, a circle Metric.sphere c r of positive radius, and the frontier of a bounded
convex set with nonempty interior. The model is built from the complex affine change of coordinates
w ↦ (w - c) / r, so it uses the field structure of ℂ and not only its metric, and the convex
frontier is obtained from the model by transport.
Phrasing the predicate as the set is homeomorphic to the circle, rather than the set is the
range of a continuous map on [0, 1] that is injective except for matching endpoints, is what
makes it usable: over a Hausdorff ambient space the two agree, because there a continuous injection
out of a compact space is an embedding, but the parametrized form buries that argument in every
use. Passing from a parametrization to the predicate is TauCeti.IsJordanCurve.image, which turns
a continuous injective map defined on a set already known to be a Jordan curve — a circle in ℂ,
say — into a proof that its image is one; TauCeti.IsJordanCurve.of_image runs the other way,
transporting the property back to a compact set from an image already known to be a Jordan curve.
Main definitions #
TauCeti.IsJordanCurve— a set homeomorphic to the circle.TauCeti.jordanParam— the parametrization of a Jordan curve by the circle underlying a homeomorphism of the curve withCircle.
Main results #
TauCeti.IsJordanCurve.isCompact,TauCeti.IsJordanCurve.isPathConnected,TauCeti.IsJordanCurve.nonemptyandTauCeti.IsJordanCurve.not_subsingleton— a Jordan curve is a nonempty compact path-connected set with more than one point.TauCeti.IsJordanCurve.imageandTauCeti.IsJordanCurve.of_image— being a Jordan curve transfers in both directions along a map that is continuous and injective on the set, provided the codomain is Hausdorff (and, in the direction that transports the property back from the image, the source set is known to be compact).TauCeti.IsJordanCurve.image_homeomorphandTauCeti.isJordanCurve_image_homeomorph_iff— being a Jordan curve is invariant under a homeomorphism of the ambient spaces; no separation axiom is needed.TauCeti.continuous_jordanParam,TauCeti.jordanParam_injective,TauCeti.isInducing_jordanParam,TauCeti.range_jordanParam,TauCeti.jordanParam_applyandTauCeti.jordanParam_apply_apply— the parametrization of a Jordan curve by the circle is a continuous injection, is inducing, traces out exactly the curve, and undoese; this is what carries a statement about the circle to one about an arbitrary Jordan curve.TauCeti.sphereCircleHomeomorphandTauCeti.isJordanCurve_sphere— a circle of positive radius inℂis a Jordan curve, by the affine change of coordinatesw ↦ (w - c) / r.TauCeti.isJordanCurve_frontier_of_convex— the frontier of a bounded convex subset ofℂwith nonempty interior is a Jordan curve. This isTauCeti.isJordanCurve_spherewith the disc weakened to an arbitrary convex body, the affine change of coordinates being replaced by Mathlib's gauge rescaling.TauCeti.locallyConnectedSpace_sphereandTauCeti.IsJordanCurve.locallyConnectedSpace— a circle inℂ, and hence every Jordan curve, is locally connected.
Motivation #
This is the vocabulary layer L5 of the conformal-mapping roadmap
(TauCetiRoadmap/ConformalMapping/README.md) is stated in: its milestone, the Carathéodory
boundary correspondence, is about the Riemann map of a Jordan domain, and the roadmap records
that the pinned Mathlib has no Jordan-curve vocabulary to state it against. The complex-analytic
half — Jordan domains, the discs among them, and the boundary of a domain that a conformal map
carries onto a disc — is in TauCeti/Analysis/Complex/Conformal/Jordan/Domain.lean.
Local connectedness of a Jordan curve is what that milestone needs of the hypothesis side: the
route to the extension theorem for a Jordan domain Ω runs through Carathéodory's continuity
theorem, whose hypothesis is that frontier Ω be locally connected, and
TauCeti.IsJordanCurve.locallyConnectedSpace is what discharges it (as
TauCeti.IsJordanDomain.locallyConnectedSpace_frontier). Mathlib knows the circle is compact,
connected and path connected, but records no local connectedness for it, and the property is not
preserved by continuous images, so it is proved here from
TauCeti.locallyConnectedSpace_image_of_isCompact.
References #
- C. Jordan, Cours d'analyse de l'École Polytechnique, vol. 3 (1887).
- Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
A Jordan curve, or simple closed curve, in a topological space: a subset homeomorphic to the circle.
The predicate is Nonempty (C ≃ₜ Circle) rather than a chosen homeomorphism, so that it is a
Prop; TauCeti.isJordanCurve_iff recovers the homeomorphism from another module, where the
definition itself is not exposed.
Equations
- TauCeti.IsJordanCurve C = Nonempty (↑C ≃ₜ Circle)
Instances For
A set is a Jordan curve exactly when it is homeomorphic to the circle. This is the interface
to TauCeti.IsJordanCurve outside its defining module.
A Jordan curve is compact: the circle is.
A Jordan curve in a Hausdorff space is closed.
A Jordan curve is path connected: the circle is.
A Jordan curve is connected.
A Jordan curve is nonempty.
A Jordan curve has more than one point: the circle contains both 1 and -1. Together with
TauCeti.IsJordanCurve.isConnected this rules out the degenerate curves, so a Jordan curve is a
nondegenerate continuum.
A Jordan curve is carried to a Jordan curve by a continuous injection. Only continuity and injectivity on the curve are needed, the curve supplying the compactness that upgrades them to a homeomorphism onto the image.
A compact set carried onto a Jordan curve by a continuous injection is a Jordan curve.
This is the converse of TauCeti.IsJordanCurve.image; compactness of the source has to be assumed
here, since it is no longer inherited from the curve. It is the form in which the predicate is
verified when the curve is the unknown rather than the parameter: one exhibits a continuous
injective map of the set onto a set already known to be a Jordan curve, as the boundary
correspondence does with the boundary of a disc.
The image of a Jordan curve under a homeomorphism of the ambient spaces is a Jordan curve.
Unlike TauCeti.IsJordanCurve.image this needs no separation axiom on the codomain, because
Homeomorph.image supplies the homeomorphism onto the image outright.
Being a Jordan curve is invariant under a homeomorphism of the ambient spaces. This is the
characteristic form of TauCeti.IsJordanCurve.image_homeomorph: the backward direction is that
lemma applied to e.symm, which no consumer then has to spell out.
The parametrization by the circle #
Every transport of a statement about Circle to a Jordan curve goes through the parametrization
jordanParam e attached to a homeomorphism e, so its properties — continuity, injectivity,
range, and that it is inducing — are collected here rather than rebuilt at each use, both by the
cutting of a curve at one or two of its points
(TauCeti/Topology/JordanCurve/Separation.lean) and by the quantitative form of that cutting
(TauCeti/Topology/JordanCurve/SmallArc.lean).
The parametrization of a Jordan curve by the circle underlying a homeomorphism e: the
composite of e.symm with the inclusion of the curve into the ambient space.
Equations
- TauCeti.jordanParam e u = ↑(e.symm u)
Instances For
The parametrization TauCeti.jordanParam of a Jordan curve by the circle is continuous.
The parametrization TauCeti.jordanParam of a Jordan curve by the circle is injective: this is
the simplicity of the curve.
The parametrization TauCeti.jordanParam of a Jordan curve by the circle is inducing, so
preconnectedness of a subset of the curve may be tested on its preimage of parameters.
The parametrization TauCeti.jordanParam of a Jordan curve by the circle traces out exactly the
curve.
The defining equation of TauCeti.jordanParam: the parameter u names the point e.symm u of
the curve, read in the ambient space. This is the general application lemma, so a consumer never has
to unfold the definition.
The parametrization TauCeti.jordanParam of a Jordan curve by the circle undoes e: it sends
the parameter e ⟨p, hp⟩ of a point p of the curve back to p. Simp proves this from
TauCeti.jordanParam_apply; it is stated for the rw steps that produce the point p itself
rather than a coerced parameter.
The model curve: a circle in ℂ #
Circle is by definition the unit sphere of ℂ, but it is a def rather than an
abbreviation, so its topology is only definitionally the subtype topology. This identification is
the one place where that unfolding happens; the lemmas below then compute with the unit sphere
alone.
Equations
Instances For
The affine parametrization w ↦ (w - c) / r of a circle of centre c and positive radius r
in ℂ by the unit circle. It is the restriction to the spheres of the inverse of Mathlib's ambient
affineHomeomorph r c, so only the membership equivalence is proved here.
Equations
- TauCeti.sphereCircleHomeomorph c hr = ((affineHomeomorph (↑r) c ⋯).symm.subtype ⋯).trans TauCeti.unitSphereCircleHomeomorph
Instances For
The parametrization of sphere c r by the unit circle divides out the affine change of
coordinates.
A circle of positive radius in ℂ is a Jordan curve.
The frontier of a bounded convex subset of ℂ with nonempty interior is a Jordan curve.
This is TauCeti.isJordanCurve_sphere with the disc weakened to an arbitrary convex body, which it
recovers at s = Metric.ball c r. The model curve transports because Mathlib's gauge rescaling
supplies an ambient homeomorphism e : ℂ ≃ₜ ℂ carrying frontier s onto the unit circle
(exists_homeomorph_image_interior_closure_frontier_eq_unitBall), so the affine change of
coordinates above is simply replaced by a nonlinear one and no further topology is needed.
The set is asked neither to be open nor to be nonempty: what a convex set needs in order to have a
one-dimensional frontier is that it be solid, and that is (interior s).Nonempty. Without it the
statement fails — a segment is convex and bounded, and is its own frontier.
Local connectedness #
A circle in ℂ is locally connected. It is the image of the compact interval [-π, π],
which is convex and hence locally connected, under the continuous θ ↦ c + r * exp (θ * I), so
TauCeti.locallyConnectedSpace_image_of_isCompact applies. A sphere of negative radius is empty,
and vacuously locally connected.
The circle is locally connected. Circle is the unit circle of ℂ, so this is the unit
case of TauCeti.locallyConnectedSpace_sphere transported along TauCeti.sphereCircleHomeomorph.
Mathlib records the circle as compact, connected and path connected, but not as locally
connected.
A Jordan curve is locally connected, being homeomorphic to the circle.
This is the form in which the hypothesis of Carathéodory's continuity theorem — that the boundary
of the domain be locally connected — is met by a Jordan domain, which is what layer L5 of the
conformal-mapping roadmap is about; see TauCeti.IsJordanDomain.locallyConnectedSpace_frontier.
Jordan curves traced by paths #
A path whose two endpoints agree is a parametrised closed curve, but its range need not be a
Jordan curve: the path may pause, retrace an arc, or cross itself. This file supplies the exact
criterion needed to exclude those degeneracies. If a closed path has no repeated values except
for its two endpoint parameters, its range is a Jordan curve
(TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints).
The proof uses the quotient model of the circle already in Mathlib. The extension of a path
γ : Path x x to ℝ has equal values at 0 and 1, so
AddCircle.liftIco 1 0 γ.extend factors it through the additive circle ℝ / ℤ. The hypothesis on
repetitions says precisely that this factor is injective, and its range is the range of γ. The
additive circle is itself a Jordan curve, AddCircle.homeomorphCircle identifying it with
Circle, so TauCeti.IsJordanCurve.image carries that along the factor: the compactness argument
upgrading a continuous injection to a homeomorphism onto its image is already packaged there and is
not repeated here.
The condition is stated directly rather than bundled as a new notion of simple closed path. This is the only operation needed here, and keeping it as a theorem hypothesis avoids introducing a second simplicity vocabulary alongside Mathlib's path API.
Gluing two arcs #
The criterion has one immediate use that is worth naming on its own: two arcs — ranges of
injective paths — that share their two endpoints and meet nowhere else glue to a Jordan curve
(TauCeti.isJordanCurve_range_union_range_of_inter_eq_pair). The closed path traversed is
γ.trans δ.symm, whose range is range γ ∪ range δ; the meeting hypothesis is what turns a
coincidence between a value of γ and a value of δ into a coincidence of endpoints, and
injectivity of each of the two paths handles the coincidences internal to one of them. The
endpoints are not asked to be distinct: injectivity of δ already forces that, since a path with
equal endpoints repeats the value at the two distinct parameters 0 and 1.
Main results #
TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints— the range of a closed path whose only possible repetition is its pair of endpoints is a Jordan curve.TauCeti.isJordanCurve_range_union_range_of_inter_eq_pair— two arcs with the same two endpoints, meeting exactly there, glue to a Jordan curve.
Roadmap role #
This is the topological gluing step used by layer L5 of
TauCetiRoadmap/ConformalMapping/README.md, the Carathéodory boundary correspondence. A
finite-length image crosscut is already packaged as a path with exactly this simplicity property in
TauCeti/Analysis/Complex/Conformal/Crosscut/Path.lean; when its two boundary ends coincide, the
first result below identifies the closure of that crosscut as a Jordan curve, and when they are
distinct the second closes that crosscut up with an arc of the boundary of the image domain. The
coincident-end specialization is in TauCeti/Analysis/Complex/Conformal/Crosscut/Jordan.lean and
the distinct-end one in TauCeti/Analysis/Complex/Conformal/Crosscut/Arc.lean.
The range of a simple closed path is a Jordan curve. Let γ : Path x x be a closed path.
If equality γ s = γ t forces either s = t or the unordered pair of parameters to be {0, 1},
then range γ is homeomorphic to the circle.
The disjunction records both orientations of the exceptional endpoint pair explicitly. No local
injectivity or embedding hypothesis is needed, and no separation assumption on the ambient space
beyond the Hausdorffness that TauCeti.IsJordanCurve.image asks for.
Gluing two arcs along their endpoints #
Two arcs meeting exactly at their common endpoints glue to a Jordan curve. Let
γ δ : Path x y be injective and let their ranges meet in exactly the two endpoints,
range γ ∩ range δ = {x, y}. Then range γ ∪ range δ is a Jordan curve.
The curve traversed is γ.trans δ.symm, a closed path at x whose range is range γ ∪ range δ
by Path.trans_range and Path.symm_range. Its only repetitions are the ones
TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints allows: a coincidence between two parameters on
the same half is excluded by injectivity of that half, and one between the two halves lands in
{x, y}, so it is either the pair {0, 1} of endpoint parameters or the single parameter 1 / 2
at which the two halves are joined.
Distinctness of x and y is a consequence rather than a hypothesis: δ 0 = δ 1 would contradict
injectivity of δ.
Moving sofa: related mathematical developments #
Curve.Foundations.Development002.Curve.Foundations.Development003.
Moving sofa: related mathematical developments #
Curve.Jordan.Separation.Curve.Jordan.Interior.Curve.Jordan.OrientationTransport.Curve.Jordan.AreaTransport.Curve.Jordan.ClosedArea.Curve.Jordan.SignedArea.Curve.Jordan.SupportingOrientation.Curve.Jordan.Subarc.Curve.Reparametrization.Curve.SegmentAreaProperties.Curve.Jordan.SubarcArea.
Curve / Jordan / Separation #
Curve / Jordan / Interior #
A Jordan curve has a point in its bounded complementary component.
The frontier of the bounded complementary component of a Jordan curve is the curve itself.
Curve / Jordan / Orientation Transport #
Endpoint-preserving continuous parameter changes preserve Jordan orientation.
Exchanging the parameter endpoints reverses Jordan orientation.
Curve / Jordan / Area Transport #
A monotone or antitone transition between oriented Jordan paths determines their signed areas.
Curve / Jordan / Closed Area #
Same-carrier closed Jordan parametrizations have signed areas determined by orientation.
Curve / Jordan / Signed Area #
Curve / Jordan / Supporting Orientation #
Curve / Jordan / Subarc #
Reversing the parameter of a closed path preserves injectivity away from the identified terminal endpoint.
Parameter reversal sends the reversed closed interval to the original interval image.
Convex interpolation between ordered interval points is strictly increasing.
The two closed pieces outside an interior parameter interval trace exactly the closed curve with the open interval image removed.
Convex interpolation between the interval endpoints covers the interval.
The initial restriction of a cyclically concatenated closed path traces the complement of an interior parameter interval.
If a closed parameter interval traces a nondegenerate segment injectively, its open interval traces the segment with its endpoints removed.
A nondegenerate segment in a closed Jordan curve, away from the base point, is traced by an interior parameter interval.
The endpoints of an injectively parametrized nondegenerate segment are the parameter-interval endpoints, in one of the two possible orders.
Removing a supporting chord from a counterclockwise closed Jordan path yields the oriented complementary arc.
Curve / Reparametrization #
Curve / Segment Area Properties #
Curve / Jordan / Subarc Area #
A proper restriction of a closed BV Jordan parametrization realizes an arc with the same signed area as the restricted path.
The suffix of the cyclic rotation, after the complementary arc, is an increasing reparametrization of the removed interval.
Removing a supporting chord from a counterclockwise closed BV Jordan path gives the complementary arc, and closed signed area splits into arc area and the oriented chord area.
Moving sofa: related mathematical developments #
Curve.PositiveGraphOrientation.Curve.PositiveGraphRegion.
The counterclockwise loop around a positive graph #
For a < b and a continuous f : ℝ → ℝ vanishing at a and b and positive on (a, b),
MovingSofa.positiveGraphLoop traverses the graph of f from (b, 0) to (a, 0) and then the
base segment from (a, 0) back to (b, 0). The main result
MovingSofa.positiveGraphLoop_counterclockwise shows that this is a counterclockwise once-traversed
Jordan parametrization whose bounded complementary component is the open subgraph
{p | a < p 0 ∧ p 0 < b ∧ 0 < p 1 ∧ p 1 < f (p 0)}.
Traverse the graph from right to left and return along the horizontal axis.
Equations
Instances For
The region enclosed by the counterclockwise loop around a positive graph #
MovingSofa.positiveGraphLoop_counterclockwise identifies the bounded complementary component
of the loop around the graph of a positive f with the open subgraph of f. This file records
the resulting description of the closed subgraph: the loop traces exactly the frontier of either
region, and the closed subgraph is the open one together with that frontier.