Geodesic segments as points of path space #

The path space of a topological space X is C(I, X), the continuous maps from the unit interval with the compact-open topology; when X is a pseudometric space, as below, this is the topology of uniform convergence since the domain is compact. This file singles out the geodesic segments inside it: TauCeti.geodesicPaths X is the set of paths γ with dist (γ s) (γ t) = |s - t| * dist (γ 0) (γ 1). These are exactly the restrictions to [0, 1] of the curves TauCeti.IsGeodesicSegment describes, so a pseudometric space is a geodesic space exactly when every pair of points is the pair of endpoints of a geodesic path.

The defining identity only involves finitely many evaluations at a time, so the set of geodesic paths is closed in path space, and on a metric space so is the relation between a pair of points and a geodesic path joining them. On a Polish space this relation is therefore a closed subset of a Polish space; this is the input that a measurable selection theorem needs to choose a geodesic measurably in its endpoints, which is how a law of pairs of points is lifted to a law of geodesics in optimal transport.

Main definitions #

TauCeti.geodesicPaths X: the geodesic segments of X, as a subset of C(I, X).
TauCeti.segmentPath: the affine segments of a real normed space, as a continuous map from pairs of endpoints to path space.

Main results #

TauCeti.mem_geodesicPaths_iff_isGeodesicSegment: a path is a geodesic path exactly when its extension to ℝ is a geodesic segment between its endpoints.
TauCeti.exists_mem_geodesicPaths_iff: two points are the endpoints of a geodesic path exactly when they are joined by a geodesic segment; TauCeti.isGeodesicSpace_iff_exists_mem_geodesicPaths restates the geodesic-space condition this way.
TauCeti.isClosed_geodesicPaths: the geodesic paths form a closed subset of path space.
TauCeti.isClosed_setOf_mem_geodesicPaths_endpoints: on a metric space, the relation between a pair of points and the geodesic paths joining them is closed.
TauCeti.segmentPath_mem_geodesicPaths: the affine segments of a real normed space are geodesic paths.
TauCeti.eq_segmentPath_of_mem_geodesicPaths: conversely, in a strictly convex real normed space every geodesic path is the affine segment between its endpoints.

References #

L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, Birkhäuser, 2nd ed. 2008, §2.1 and §7.2.
C. Villani, Optimal Transport: Old and New, Springer 2009, Chapter 7.

source

def TauCeti.geodesicPaths (X : Type u_1) [PseudoMetricSpace X] :

Set C(↑unitInterval, X)

The geodesic paths of X: the continuous paths γ : C(I, X) with dist (γ s) (γ t) = |s - t| * dist (γ 0) (γ 1) for all times s and t. These are the geodesic segments from γ 0 to γ 1, parametrised proportionally to arclength, viewed as points of path space.

Instances For

source

@[simp]

theorem TauCeti.mem_geodesicPaths_iff {X : Type u_1} [PseudoMetricSpace X] {γ : C(↑unitInterval, X)} :

γ ∈ geodesicPaths X ↔ ∀ (s t : ↑unitInterval), dist (γ s) (γ t) = |↑s - ↑t| * dist (γ 0) (γ 1)

Membership in the geodesic paths, unfolded.

source

theorem TauCeti.mem_geodesicPaths_iff_isGeodesicSegment {X : Type u_1} [PseudoMetricSpace X] {γ : C(↑unitInterval, X)} :

γ ∈ geodesicPaths X ↔ IsGeodesicSegment (Set.IccExtend ⋯ ⇑γ) (γ 0) (γ 1)

A path is a geodesic path exactly when its extension to ℝ, constant outside [0, 1], is a geodesic segment between its endpoints.

source

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

{ toFun := (Set.Icc 0 1).domRestrict γ, continuous_toFun := ⋯ } ∈ geodesicPaths X

The restriction to [0, 1] of a geodesic segment is a geodesic path.

source

theorem TauCeti.exists_mem_geodesicPaths_iff {X : Type u_1} [PseudoMetricSpace X] {x y : X} :

(∃ γ ∈ geodesicPaths X, γ 0 = x ∧ γ 1 = y) ↔ ∃ (γ : ℝ → X), IsGeodesicSegment γ x y

Two points are the endpoints of a geodesic path exactly when they are joined by a geodesic segment.

source

theorem TauCeti.isGeodesicSpace_iff_exists_mem_geodesicPaths {X : Type u_1} [PseudoMetricSpace X] :

IsGeodesicSpace X ↔ ∀ (x y : X), ∃ γ ∈ geodesicPaths X, γ 0 = x ∧ γ 1 = y

A pseudometric space is a geodesic space exactly when every pair of points is the pair of endpoints of a geodesic path.

source

theorem TauCeti.IsGeodesicSpace.exists_mem_geodesicPaths {X : Type u_1} [PseudoMetricSpace X] [IsGeodesicSpace X] (x y : X) :

∃ γ ∈ geodesicPaths X, γ 0 = x ∧ γ 1 = y

In a geodesic space, any two points are the endpoints of a geodesic path.

source

theorem TauCeti.isClosed_geodesicPaths {X : Type u_1} [PseudoMetricSpace X] :

IsClosed (geodesicPaths X)

The geodesic paths form a closed subset of path space.

source

theorem TauCeti.isClosed_setOf_mem_geodesicPaths_endpoints {X : Type u_1} [MetricSpace X] :

IsClosed {q : (X × X) × C(↑unitInterval, X) | q.2 ∈ geodesicPaths X ∧ (q.2 0, q.2 1) = q.1}

The relation between a pair of points of a metric space and the geodesic paths joining them is closed in (X × X) × C(I, X).

source

def TauCeti.segmentPath {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] :

C(E × E, C(↑unitInterval, E))

The affine segments of a real normed space, as a continuous map from pairs of endpoints to path space: segmentPath z is Mathlib's Path.segment z.1 z.2, the path t ↦ AffineMap.lineMap z.1 z.2 t from z.1 to z.2, depending continuously on both endpoints.

Instances For

source