Length spaces and geodesic spaces

A metric space is a length space when the distance between two points is the infimum of the lengths of the continuous curves joining them, and a geodesic space when that infimum is realised by a curve on [0, 1] whose distance function is the affine one, dist (γ s) (γ t) = |s - t| * dist x y. This file sets up both notions, together with the length of a curve that they are phrased in terms of, and proves that a geodesic space is a length space.

The length of a curve

The length of a curve γ : ℝ → X over a parameter interval [a, b] is the supremum of the sums ∑ i, edist (γ (u (i + 1))) (γ (u i)) over finite increasing families u in [a, b]. This is exactly Mathlib's total variation eVariationOn γ (Set.Icc a b), which this file uses directly. Two conventions are inherited deliberately:

• curves are functions on all of ℝ, read on a parameter interval, rather than functions on a subtype. This is the convention of Manifold.pathELength I γ a b, the Riemannian length to be compared against, and it avoids subtype juggling in the API;
• the value is an extended nonnegative real, since a continuous curve can have infinite length.

Mathlib's bundled Path x y is bridged to this convention in both directions, by TauCeti.IsCurveJoining.joined and TauCeti.isCurveJoining_extend.

Continuity is load-bearing

The infimum defining a length space must range over continuous curves. Dropping continuity makes every metric space a length space: the two-valued curve which is x on [0, 1) and y at 1 already has length edist x y, by eVariationOn.edist_le.

Main definitions

• TauCeti.IsCurveJoining γ x y — γ is continuous on [0, 1] and runs from x to y there.
• TauCeti.IsGeodesicSegment γ x y — γ parametrises a shortest curve from x to y proportionally to arclength on [0, 1].
• TauCeti.IsLengthSpace X — the distance is the infimum of the lengths of the joining curves.
• TauCeti.IsGeodesicSpace X — any two points are joined by a geodesic segment.

Main results

• TauCeti.exists_isCurveJoining_of_continuousOn shows that the parameter interval [0, 1] is no loss of generality.
• TauCeti.IsGeodesicSegment.eVariationOn_eq_edist — a geodesic segment realises the distance between any two of its points, and in particular between its endpoints.
• TauCeti.IsGeodesicSpace.toIsLengthSpace — a geodesic space is a length space; there the infimum is attained, by TauCeti.IsGeodesicSpace.exists_eVariationOn_eq.
• TauCeti.IsLengthSpace.pathConnectedSpace — a nonempty length space with finite distances is path connected.
• TauCeti.instIsGeodesicSpace — a real seminormed space is a geodesic space, its geodesic segments being the affine ones (TauCeti.isGeodesicSegment_lineMap).
• TauCeti.IsGeodesicSegment.eq_lineMap — in a strictly convex real normed torsor the affine segment is the only geodesic segment, so geodesic segments are unique in every metric space that embeds isometrically in one (TauCeti.IsGeodesicSegment.eqOn_of_isometry).

Curves joining two points

structure TauCeti.IsCurveJoining {X : Type u_1} [TopologicalSpace X] (γ : ℝ → X) (x y : X) : Prop

IsCurveJoining γ x y says that the curve γ, read on the parameter interval [0, 1], is continuous and runs from x to y.

• continuousOn : ContinuousOn γ (Set.Icc 0 1)

  A joining curve is continuous on its parameter interval.

• source : γ 0 = x

  A joining curve starts at x.

• target : γ 1 = y

  A joining curve ends at y.

theorem TauCeti.isCurveJoining_extend {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : IsCurveJoining (⇑γ.extend) x y

The extension to ℝ of a bundled path is a joining curve.

theorem TauCeti.IsCurveJoining.joined {X : Type u_1} [TopologicalSpace X] {γ : ℝ → X} {x y : X} (h : IsCurveJoining γ x y) : Joined x y

A joining curve restricts to a bundled path, so it witnesses Joined.

theorem TauCeti.IsCurveJoining.edist_le {X : Type u_1} [TopologicalSpace X] {γ : ℝ → X} {x y : X} [WeakPseudoEMetricSpace X] (h : IsCurveJoining γ x y) : edist x y ≤ eVariationOn γ (Set.Icc 0 1)

A joining curve is at least as long as the distance between the points it joins.

theorem TauCeti.edist_le_iInf_eVariationOn {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (x y : X) : edist x y ≤ ⨅ (γ : ℝ → X), ⨅ (_ : IsCurveJoining γ x y), eVariationOn γ (Set.Icc 0 1)

One half of the length-space condition holds in any space: no curve joining x to y is shorter than edist x y.

theorem TauCeti.exists_isCurveJoining_of_continuousOn {X : Type u_1} [TopologicalSpace X] {γ : ℝ → X} {x y : X} [WeakPseudoEMetricSpace X] {a b : ℝ} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (ha : γ a = x) (hb : γ b = y) : ∃ (γ' : ℝ → X), IsCurveJoining γ' x y ∧ eVariationOn γ' (Set.Icc 0 1) = eVariationOn γ (Set.Icc a b)

A continuous curve joining x to y on an arbitrary parameter interval can be renormalised to [0, 1] without changing its length. This is how curves produced on other parameter intervals enter the length-space condition below.

Length spaces

class TauCeti.IsLengthSpace (X : Type u_2) [PseudoEMetricSpace X] : Prop

A length space is a space in which the distance between two points is the infimum of the lengths of the continuous curves joining them.

• edist_eq_iInf (x y : X) : edist x y = ⨅ (γ : ℝ → X), ⨅ (_ : IsCurveJoining γ x y), eVariationOn γ (Set.Icc 0 1)

  The distance between two points is the infimum of the lengths of the curves joining them.

theorem TauCeti.IsLengthSpace.of_exists_eVariationOn_lt {X : Type u_1} [PseudoEMetricSpace X] (h : ∀ (x y : X) (c : ENNReal), edist x y < c → ∃ (γ : ℝ → X), IsCurveJoining γ x y ∧ eVariationOn γ (Set.Icc 0 1) < c) : IsLengthSpace X

To check that a space is a length space it suffices to produce, for every pair of points and every bound strictly above their distance, a joining curve shorter than that bound.

theorem TauCeti.IsLengthSpace.exists_eVariationOn_lt {X : Type u_1} [PseudoEMetricSpace X] {x y : X} [IsLengthSpace X] {c : ENNReal} (hc : edist x y < c) : ∃ (γ : ℝ → X), IsCurveJoining γ x y ∧ eVariationOn γ (Set.Icc 0 1) < c

In a length space, joining curves of length arbitrarily close to the distance exist.

theorem TauCeti.IsLengthSpace.joined {X : Type u_2} [PseudoMetricSpace X] [IsLengthSpace X] (x y : X) : Joined x y

Any two points of a length space with finite distances are joined by a continuous curve.

theorem TauCeti.IsLengthSpace.pathConnectedSpace {X : Type u_2} [PseudoMetricSpace X] [IsLengthSpace X] [Nonempty X] : PathConnectedSpace X

A nonempty length space with finite distances is path connected. This is not an instance: PathConnectedSpace is a goal about a bare topological space, and searching a metric structure and a length-space structure on every such goal is not worth it.

theorem TauCeti.IsLengthSpace.exists_eVariationOn_lt_ofReal {X : Type u_2} [PseudoMetricSpace X] [IsLengthSpace X] {x y : X} {r : ℝ} (hr : dist x y < r) : ∃ (γ : ℝ → X), IsCurveJoining γ x y ∧ eVariationOn γ (Set.Icc 0 1) < ENNReal.ofReal r

The metric form of TauCeti.IsLengthSpace.exists_eVariationOn_lt.

Geodesic segments and geodesic spaces

structure TauCeti.IsGeodesicSegment {X : Type u_1} [PseudoMetricSpace X] (γ : ℝ → X) (x y : X) : Prop

IsGeodesicSegment γ x y says that the curve γ, read on the parameter interval [0, 1], runs from x to y with dist (γ s) (γ t) = |s - t| * dist x y: it is a shortest curve from x to y, parametrised proportionally to arclength.

• source : γ 0 = x

  A geodesic segment starts at x.

• target : γ 1 = y

  A geodesic segment ends at y.

• dist_eq (s : ℝ) : s ∈ Set.Icc 0 1 → ∀ t ∈ Set.Icc 0 1, dist (γ s) (γ t) = |s - t| * dist x y

  A geodesic segment is affinely parametrised by arclength.

theorem TauCeti.IsGeodesicSegment.lipschitzOnWith {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : LipschitzOnWith (dist x y).toNNReal γ (Set.Icc 0 1)

A geodesic segment is Lipschitz on its parameter interval, with constant dist x y.

theorem TauCeti.IsGeodesicSegment.dist_source_apply {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : dist x (γ t) = t * dist x y

The point at time t of a geodesic segment from x to y is at distance t * dist x y from x.

theorem TauCeti.IsGeodesicSegment.edist_source_apply {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : edist x (γ t) = ENNReal.ofReal (t * dist x y)

The extended distance from the source along a geodesic segment.

theorem TauCeti.IsGeodesicSegment.dist_apply_target {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : dist (γ t) y = (1 - t) * dist x y

The point at time t of a geodesic segment from x to y is at distance (1 - t) * dist x y from y.

theorem TauCeti.IsGeodesicSegment.tendsto_nhdsGT_zero {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) (hxy : 0 < dist x y) : Filter.Tendsto γ (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin x {x}ᶜ)

A geodesic segment between two points at positive distance leaves its source immediately: as t → 0⁺, its point at time t tends to x without being x.

theorem TauCeti.IsGeodesicSegment.continuousOn {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : ContinuousOn γ (Set.Icc 0 1)

theorem TauCeti.IsGeodesicSegment.isCurveJoining {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : IsCurveJoining γ x y

theorem TauCeti.isGeodesicSegment_const {X : Type u_1} [PseudoMetricSpace X] (x : X) : IsGeodesicSegment (fun (x_1 : ℝ) => x) x x

The constant curve is a geodesic segment from a point to itself.

theorem TauCeti.IsGeodesicSegment.reverse {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : IsGeodesicSegment (fun (t : ℝ) => γ (1 - t)) y x

Running a geodesic segment backwards gives a geodesic segment between the same points.

theorem TauCeti.IsGeodesicSegment.comp_lineMap {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : IsGeodesicSegment (fun (t : ℝ) => γ ((AffineMap.lineMap a b) t)) (γ a) (γ b)

The piece of a geodesic segment between the times a and b, reparametrised over [0, 1], is a geodesic segment from γ a to γ b.

theorem TauCeti.IsGeodesicSegment.dist_apply_apply_midpoint {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : dist (γ s) (γ (midpoint ℝ s t)) = dist (γ s) (γ t) / 2

The point of a geodesic segment at the midpoint of two times s and t is at distance dist (γ s) (γ t) / 2 from γ s.

theorem TauCeti.IsGeodesicSegment.dist_apply_midpoint_apply {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {s t : ℝ} (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) : dist (γ (midpoint ℝ s t)) (γ t) = dist (γ s) (γ t) / 2

The point of a geodesic segment at the midpoint of two times s and t is at distance dist (γ s) (γ t) / 2 from γ t.

theorem TauCeti.IsGeodesicSegment.comp_isometry {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} {Y : Type u_2} [PseudoMetricSpace Y] {f : X → Y} (h : IsGeodesicSegment γ x y) (hf : Isometry f) : IsGeodesicSegment (f ∘ γ) (f x) (f y)

An isometry maps a geodesic segment from x to y to a geodesic segment from f x to f y.

theorem TauCeti.IsGeodesicSegment.congr {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} {γ' : ℝ → X} (h : IsGeodesicSegment γ x y) (h' : Set.EqOn γ' γ (Set.Icc 0 1)) : IsGeodesicSegment γ' x y

Being a geodesic segment depends only on the values of the curve on [0, 1].

theorem TauCeti.isGeodesicSegment_of_dist_le {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h0 : γ 0 = x) (h1 : γ 1 = y) (h : ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, s ≤ t → dist (γ s) (γ t) ≤ (t - s) * dist x y) : IsGeodesicSegment γ x y

A curve from x to y whose pieces obey the affine bound dist (γ s) (γ t) ≤ (t - s) * dist x y for 0 ≤ s ≤ t ≤ 1 is a geodesic segment: the triangle inequality along 0 ≤ s ≤ t ≤ 1 turns each bound into an equality.

theorem TauCeti.IsGeodesicSegment.eVariationOn_le {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : eVariationOn γ (Set.Icc a b) ≤ ENNReal.ofReal ((b - a) * dist x y)

No piece of a geodesic segment is longer than the affine bound its parametrisation predicts. The reverse inequality is eVariationOn.edist_le, so the two together identify the length of every piece.

theorem TauCeti.IsGeodesicSegment.eVariationOn_eq_edist {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hab : a ≤ b) : eVariationOn γ (Set.Icc a b) = edist (γ a) (γ b)

A geodesic segment realises the distance between any two of its points.

theorem TauCeti.IsGeodesicSegment.eVariationOn_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) : eVariationOn γ (Set.Icc 0 1) = edist x y

A geodesic segment from x to y has length edist x y.

class TauCeti.IsGeodesicSpace (X : Type u_2) [PseudoMetricSpace X] : Prop

A geodesic space is a space in which any two points are joined by a geodesic segment.

• exists_isGeodesicSegment (x y : X) : ∃ (γ : ℝ → X), IsGeodesicSegment γ x y

  Any two points are joined by a geodesic segment.

theorem TauCeti.IsGeodesicSpace.exists_eVariationOn_eq {X : Type u_1} [PseudoMetricSpace X] [IsGeodesicSpace X] (x y : X) : ∃ (γ : ℝ → X), IsCurveJoining γ x y ∧ eVariationOn γ (Set.Icc 0 1) = edist x y

In a geodesic space the infimum defining the length-space condition is attained.

theorem TauCeti.IsGeodesicSpace.of_isometryEquiv {X : Type u_1} [PseudoMetricSpace X] {Y : Type u_2} [PseudoMetricSpace Y] [IsGeodesicSpace X] (e : X ≃ᵢ Y) : IsGeodesicSpace Y

A space isometric to a geodesic space is a geodesic space.

instance TauCeti.IsGeodesicSpace.toIsLengthSpace {X : Type u_1} [PseudoMetricSpace X] [IsGeodesicSpace X] : IsLengthSpace X

A geodesic space is a length space.

Seminormed spaces

theorem TauCeti.isGeodesicSegment_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) : IsGeodesicSegment (⇑(AffineMap.lineMap x y)) x y

In a real normed torsor the affine segment from x to y is a geodesic segment.

theorem TauCeti.IsGeodesicSpace.of_normedAddTorsor {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] : IsGeodesicSpace P

A real normed torsor is a geodesic space. This is stated as a theorem rather than an instance because the acting space V would have to be guessed before the torsor structure is found; the instance below covers the case of a seminormed space acting on itself.

instance TauCeti.instIsGeodesicSpace {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : IsGeodesicSpace E

theorem TauCeti.IsGeodesicSegment.eq_lineMap {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {γ : ℝ → P} {x y : P} (h : IsGeodesicSegment γ x y) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : γ t = (AffineMap.lineMap x y) t

Geodesic segments of a strictly convex space are affine. In a strictly convex real normed torsor, the point at time t ∈ [0, 1] of a geodesic segment from x to y is AffineMap.lineMap x y t. Without strict convexity this fails: in ℝ² with the sup norm, the curve running first diagonally and then vertically is a geodesic segment from (0, 0) to (1, 2).

theorem TauCeti.IsGeodesicSegment.eqOn_of_isometry {X : Type u_1} {V : Type u_2} {P : Type u_3} [MetricSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {f : X → P} (hf : Isometry f) {γ γ' : ℝ → X} {x y : X} (h : IsGeodesicSegment γ x y) (h' : IsGeodesicSegment γ' x y) : Set.EqOn γ γ' (Set.Icc 0 1)

Uniqueness of geodesic segments. In a metric space that embeds isometrically in a strictly convex real normed torsor, two geodesic segments with the same endpoints agree on [0, 1]: their images are both the affine segment between the images of the endpoints.