Wasserstein geodesics from optimal dynamic plans

Let η be a dynamic plan on a metric space X, concentrated on geodesic paths, whose endpoint law is an optimal coupling of its laws μ = η_0 and ν = η_1 at times 0 and 1, at finite cost. Its laws at intermediate times then form a constant-speed geodesic for the p-Wasserstein distance, for every exponent 1 ≤ p ≤ ∞:

W_p (η_s, η_t) = |s - t| * W_p (μ, ν).

The bound ≤ holds for any plan concentrated on geodesics (TauCeti.wassersteinEDist_timeMarginal_le). The reverse bound follows from the triangle inequality: W_p (μ, ν) is at most the sum of the three distances along 0 ≤ s ≤ t ≤ 1, each of which is bounded by its share of W_p (μ, ν), so none of the three bounds can be strict. In the same way, the joint law of the path at times s and t is an optimal coupling of η_s and η_t: every two-time projection of such a plan is optimal.

On a Polish geodesic space, every pair of finite measures at finite Wasserstein distance is the pair of endpoint laws of such a plan, obtained by lifting an optimal coupling to geodesic paths. Consequently the space P_p (X) of probability measures with finite p-th moment is itself a geodesic space. On a separable Banach space no measurable selection is needed: the affine segments lift every optimal coupling π, so the laws of (1 - t) • x + t • y under π form a geodesic segment of P_p (E).

Conversely, for 1 < p < ∞ every geodesic segment of P_p (X) over a complete separable metric space arises in this way. Lisini's superposition principle represents it by a law on absolutely continuous paths whose expected p-action is the action W_p (μ, ν) ^ p of the curve. Every such path has action at least the p-th power of the distance between its endpoints, and the endpoint law couples μ and ν, so almost every path has minimal action and is therefore a constant-speed geodesic (AbsolutelyContinuousOnInterval.isGeodesicSegment_of_curveAction_le). The same comparison gives the dynamic formulation of the Wasserstein distance: W_p (μ, ν) ^ p is the least expected action of a dynamic plan from μ to ν.

In a strictly convex separable Banach space E the affine segments are the only geodesics, so for 1 < p < ∞ the geodesic segments of P_p (E) from μ to ν are exactly the linear interpolations t ↦ ((1 - t) • x + t • y)₊ π of the optimal couplings π of μ and ν. The optimal coupling need not be unique.

Main definitions

• TauCeti.IsDisplacementInterpolation: a curve of probability laws induced by an optimal dynamic plan concentrated on constant-speed geodesics, without choosing a presentation.

Main results

• TauCeti.wassersteinEDist_timeMarginal_eq: the laws at intermediate times of a dynamic plan concentrated on geodesics, with optimal endpoint law of finite cost, form a constant-speed Wasserstein geodesic.
• TauCeti.eLpNorm_edist_map_eq_wassersteinEDist_timeMarginal and TauCeti.isOptimalCoupling_map_timeMarginal: every two-time projection of such a plan is an optimal coupling of its laws at those times.
• TauCeti.exists_ae_mem_geodesicPaths_wassersteinEDist_timeMarginal_eq: on a Polish geodesic space, two finite measures at finite p-Wasserstein distance are joined by such a plan.
• TauCeti.WassersteinSpace.exists_isGeodesicSegment_timeMarginal: the laws at intermediate times of such a plan between two points of P_p (X) trace a geodesic segment of P_p (X).
• TauCeti.WassersteinSpace.instIsGeodesicSpace: on a Polish geodesic space, P_p (X) is a geodesic space for every 1 ≤ p ≤ ∞.
• TauCeti.WassersteinSpace.isGeodesicSegment_iff_isDisplacementInterpolation: for 1 < p < ∞, the geodesic segments of P_p (X) are exactly the curves of laws of optimal dynamic plans concentrated on geodesic paths.
• TauCeti.wassersteinEDist_rpow_le_lintegral_curveAction and TauCeti.isLeast_wassersteinEDist_rpow_lintegral_curveAction: W_p (μ, ν) ^ p is the least expected p-action of a dynamic plan from μ to ν on a Polish geodesic space.
• TauCeti.WassersteinSpace.exists_isGeodesicSegment_map_smul_add_smul: on a separable Banach space, the laws of (1 - t) • x + t • y under an optimal coupling form a geodesic segment.
• TauCeti.WassersteinSpace.exists_isGeodesicSegment_isOptimalCoupling: for a finite exponent 1 ≤ p < ∞, the coupling (x, (1 - t) • x + t • y)₊ γ of the source with the law at time t is optimal.
• TauCeti.WassersteinSpace.exists_dist_sq_eq_integral_isGeodesicSegment_map_smul_add_smul: for the exponent 2, the interpolated plan can be chosen with ∫ ‖x - y‖² dπ = W₂ (μ, ν)².
• TauCeti.WassersteinSpace.isGeodesicSegment_iff_exists_isOptimalCoupling: on a strictly convex separable Banach space and for 1 < p < ∞, the geodesic segments of P_p (E) from μ to ν are exactly the linear interpolations of the optimal couplings of μ and ν.

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, §7.2.
• S. Lisini, Characterization of absolutely continuous curves in Wasserstein spaces, Calc. Var. Partial Differential Equations 28 (2007), 85--120.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapter 7.

def TauCeti.IsDisplacementInterpolation {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (p : ENNReal) (μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure X) : Prop

A curve of probability laws is a displacement interpolation if it is the curve of time marginals of a probability dynamic plan on constant-speed geodesics with optimal endpoint law. The optimality uses eLpNorm, so it includes the infinite exponent and infinite values.

theorem TauCeti.isDisplacementInterpolation_iff {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure X} : IsDisplacementInterpolation p μ ↔ ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), MeasureTheory.IsProbabilityMeasure η ∧ (∀ᵐ (c : C(↑unitInterval, X)) ∂η, c ∈ geodesicPaths X) ∧ (∀ (t : ↑unitInterval), η.timeMarginal t = ↑(μ t)) ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p ↑(μ 0) ↑(μ 1)

The dynamic-plan characterization of displacement interpolation.

theorem TauCeti.wassersteinEDist_timeMarginal_eq {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] {η : MeasureTheory.Measure C(↑unitInterval, X)} [MeasureTheory.IsFiniteMeasure η] (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) (hp : 1 ≤ p) (hopt : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1)) (hfin : wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1) ≠ ⊤) (s t : ↑unitInterval) : wassersteinEDist p (η.timeMarginal s) (η.timeMarginal t) = edist s t * wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1)

Wasserstein geodesics from optimal dynamic plans. Let η be a finite dynamic plan concentrated on geodesic paths whose endpoint law is an optimal coupling, at finite cost, of its laws at times 0 and 1. For 1 ≤ p, its laws at times s and t are at p-Wasserstein distance exactly |s - t| times that between its laws at times 0 and 1.

theorem TauCeti.eLpNorm_edist_map_eq_wassersteinEDist_timeMarginal {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] {η : MeasureTheory.Measure C(↑unitInterval, X)} [MeasureTheory.IsFiniteMeasure η] (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) (hp : 1 ≤ p) (hopt : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1)) (hfin : wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1) ≠ ⊤) (s t : ↑unitInterval) : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p (MeasureTheory.Measure.map (fun (γ : C(↑unitInterval, X)) => (γ s, γ t)) η) = wassersteinEDist p (η.timeMarginal s) (η.timeMarginal t)

Two-time projections are optimal. For a dynamic plan as in TauCeti.wassersteinEDist_timeMarginal_eq, the joint law at times s and t realizes the p-Wasserstein distance between the laws at those times.

theorem TauCeti.isOptimalCoupling_map_timeMarginal {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] {η : MeasureTheory.Measure C(↑unitInterval, X)} [MeasureTheory.IsFiniteMeasure η] (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hopt : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1)) (hfin : wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1) ≠ ⊤) (s t : ↑unitInterval) : IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) (MeasureTheory.Measure.map (fun (γ : C(↑unitInterval, X)) => (γ s, γ t)) η) (η.timeMarginal s) (η.timeMarginal t)

Two-time projections are optimal, in the language of optimal couplings: for a finite exponent, the joint law at times s and t of a dynamic plan as in TauCeti.wassersteinEDist_timeMarginal_eq is an optimal coupling of its laws at those times for the cost d ^ p.

theorem TauCeti.wassersteinEDist_timeMarginal_rpow_le_lintegral_edist {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] (η : MeasureTheory.Measure C(↑unitInterval, X)) (hp0 : p ≠ 0) (hp : p ≠ ⊤) : wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1) ^ p.toReal ≤ ∫⁻ (c : C(↑unitInterval, X)), edist (c 0) (c 1) ^ p.toReal ∂η

The endpoint law of a dynamic plan couples its laws at times 0 and 1, so for a finite nonzero exponent p the p-th power of the p-Wasserstein distance between these laws is at most the expected p-th power of the distance between the endpoints of its paths.

theorem TauCeti.wassersteinEDist_rpow_le_lintegral_curveAction {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] {η : MeasureTheory.Measure C(↑unitInterval, X)} (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑γ) 0 1) (hp : 1 ≤ p) (hp' : p ≠ ⊤) : wassersteinEDist p (η.timeMarginal 0) (η.timeMarginal 1) ^ p.toReal ≤ ∫⁻ (γ : C(↑unitInterval, X)), curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) 0 1 ∂η

The action bounds the transport cost. For 1 ≤ p < ∞, the expected p-action of a dynamic plan concentrated on paths absolutely continuous on [0, 1] is at least the p-th power of the p-Wasserstein distance between its laws at times 0 and 1.

theorem TauCeti.lintegral_curveAction_eq_eLpNorm_rpow {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] {η : MeasureTheory.Measure C(↑unitInterval, X)} (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) (hp0 : p ≠ 0) (hp : p ≠ ⊤) : ∫⁻ (γ : C(↑unitInterval, X)), curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) 0 1 ∂η = MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw ^ p.toReal

The action of a plan on geodesics. For a finite nonzero exponent p, the expected p-action of a dynamic plan concentrated on geodesic paths is the p-th power of the Lᵖ size of the ground distance under its endpoint law.

theorem TauCeti.exists_ae_mem_geodesicPaths_wassersteinEDist_timeMarginal_eq {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [IsGeodesicSpace X] (hp : 1 ≤ p) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (hfin : wassersteinEDist p μ ν ≠ ⊤) : ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), MeasureTheory.IsFiniteMeasure η ∧ (∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) ∧ η.timeMarginal 0 = μ ∧ η.timeMarginal 1 = ν ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p μ ν ∧ ∀ (s t : ↑unitInterval), wassersteinEDist p (η.timeMarginal s) (η.timeMarginal t) = edist s t * wassersteinEDist p μ ν

Existence of Wasserstein geodesics. On a Polish geodesic space and for 1 ≤ p, two finite measures μ and ν at finite p-Wasserstein distance are the laws at times 0 and 1 of a finite dynamic plan concentrated on geodesic paths, whose endpoint law is an optimal coupling of μ and ν and whose laws at times s and t are at distance exactly |s - t| * W_p (μ, ν).

theorem TauCeti.isLeast_wassersteinEDist_rpow_lintegral_curveAction {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [IsGeodesicSpace X] (hp : 1 ≤ p) (hp' : p ≠ ⊤) (μ ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (hfin : wassersteinEDist p μ ν ≠ ⊤) : IsLeast {A : ENNReal | ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), (∀ᵐ (γ : C(↑unitInterval, X)) ∂η, AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑γ) 0 1) ∧ η.timeMarginal 0 = μ ∧ η.timeMarginal 1 = ν ∧ ∫⁻ (γ : C(↑unitInterval, X)), curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) 0 1 ∂η = A} (wassersteinEDist p μ ν ^ p.toReal)

The dynamic formulation of the Wasserstein distance. On a Polish geodesic space and for 1 ≤ p < ∞, the p-th power of the p-Wasserstein distance between two finite measures at finite distance is the least expected p-action of a dynamic plan concentrated on paths absolutely continuous on [0, 1] with laws μ and ν at times 0 and 1. The minimum is attained by the plan of exists_ae_mem_geodesicPaths_wassersteinEDist_timeMarginal_eq.

theorem TauCeti.WassersteinSpace.exists_isGeodesicSegment_timeMarginal {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [Fact (1 ≤ p)] {η : MeasureTheory.Measure C(↑unitInterval, X)} (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) {μ ν : WassersteinSpace p X} (h0 : η.timeMarginal 0 = ↑↑μ) (h1 : η.timeMarginal 1 = ↑↑ν) (hopt : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p ↑↑μ ↑↑ν) : ∃ (γ : ℝ → WassersteinSpace p X), IsGeodesicSegment γ μ ν ∧ ∀ (t : ↑unitInterval), ↑↑(γ ↑t) = η.timeMarginal t

Wasserstein geodesics from optimal dynamic plans, as geodesic segments of P_p (X). The laws at intermediate times of a probability dynamic plan concentrated on geodesic paths, whose endpoint law is an optimal coupling of two laws μ and ν of finite p-th moment, trace a geodesic segment of P_p (X) from μ to ν.

instance TauCeti.WassersteinSpace.instIsGeodesicSpace {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [Fact (1 ≤ p)] [IsGeodesicSpace X] : IsGeodesicSpace (WassersteinSpace p X)

P_p (X) is a geodesic space. On a Polish geodesic space, the space of probability measures with finite p-th moment, with the p-Wasserstein distance, is a geodesic space for every 1 ≤ p ≤ ∞: the laws at intermediate times of a dynamic plan lifting an optimal coupling to geodesic paths form a geodesic segment.

theorem TauCeti.WassersteinSpace.exists_ae_mem_geodesicPaths_of_isGeodesicSegment {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [Fact (1 ≤ p)] (hp1 : 1 < p) (hp : p ≠ ⊤) {γ : ℝ → WassersteinSpace p X} {μ ν : WassersteinSpace p X} (h : IsGeodesicSegment γ μ ν) : ∃ (η : MeasureTheory.Measure C(↑unitInterval, X)), MeasureTheory.IsProbabilityMeasure η ∧ (∀ᵐ (c : C(↑unitInterval, X)) ∂η, c ∈ geodesicPaths X) ∧ (∀ (t : ↑unitInterval), η.timeMarginal t = ↑↑(γ ↑t)) ∧ MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw = wassersteinEDist p ↑↑μ ↑↑ν

Wasserstein geodesics are induced by optimal dynamic plans. Let X be a complete separable metric space and 1 < p < ∞. A geodesic segment γ of P_p (X) from μ to ν is the curve of laws of a probability dynamic plan concentrated on geodesic paths of X, whose law at each time t ∈ [0, 1] is γ t and whose endpoint law is an optimal coupling of μ and ν. No geodesic structure is assumed on X.

theorem TauCeti.WassersteinSpace.isGeodesicSegment_iff_isDisplacementInterpolation {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [Fact (1 ≤ p)] (hp1 : 1 < p) (hp : p ≠ ⊤) {γ : ℝ → WassersteinSpace p X} : IsGeodesicSegment γ (γ 0) (γ 1) ↔ IsDisplacementInterpolation p fun (t : ↑unitInterval) => ↑(γ ↑t)

Characterization of Wasserstein geodesics. Let X be a complete separable metric space and 1 < p < ∞. A curve γ in P_p (X) is a geodesic segment on [0, 1] exactly when it is the curve of laws of a probability dynamic plan concentrated on geodesic paths of X whose endpoint law is an optimal coupling of γ 0 and γ 1.

theorem TauCeti.WassersteinSpace.exists_isGeodesicSegment_map_smul_add_smul {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [Fact (1 ≤ p)] {μ ν : WassersteinSpace p E} {π : MeasureTheory.Measure (E × E)} (hπ : IsCoupling π ↑↑μ ↑↑ν) (hπopt : MeasureTheory.eLpNorm (fun (z : E × E) => edist z.1 z.2) p π = wassersteinEDist p ↑↑μ ↑↑ν) : ∃ (γ : ℝ → WassersteinSpace p E), IsGeodesicSegment γ μ ν ∧ ∀ t ∈ Set.Icc 0 1, ↑↑(γ t) = MeasureTheory.Measure.map (fun (z : E × E) => (1 - t) • z.1 + t • z.2) π

Linear interpolation of an optimal plan. On a separable Banach space E and for 1 ≤ p ≤ ∞, let π be an optimal coupling of two laws μ and ν of finite p-th moment. The laws of (1 - t) • x + t • y under π, for t ∈ [0, 1], trace a geodesic segment of P_p (E) from μ to ν.

theorem TauCeti.WassersteinSpace.exists_isGeodesicSegment_isOptimalCoupling {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [Fact (1 ≤ p)] (hp : p ≠ ⊤) {μ ν : WassersteinSpace p E} {γ : MeasureTheory.Measure (E × E)} (hγ : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) γ ↑↑μ ↑↑ν) : ∃ (c : ℝ → WassersteinSpace p E), IsGeodesicSegment c μ ν ∧ ∀ t ∈ Set.Icc 0 1, IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) (MeasureTheory.Measure.map (fun (z : E × E) => (z.1, (1 - t) • z.1 + t • z.2)) γ) ↑↑μ ↑↑(c t)

The interpolation of an optimal coupling γ of two laws μ and ν of P_p (E) for the cost d ^ p, for a finite exponent 1 ≤ p < ∞, is a geodesic segment μ_t from μ to ν, and (x, (1 - t) • x + t • y)₊ γ is an optimal coupling of μ and μ_t.

theorem TauCeti.WassersteinSpace.exists_dist_sq_eq_integral_isGeodesicSegment_map_smul_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] (μ ν : WassersteinSpace 2 E) : ∃ (π : MeasureTheory.Measure (E × E)), IsCoupling π ↑↑μ ↑↑ν ∧ MeasureTheory.MemLp (fun (z : E × E) => z.1 - z.2) 2 π ∧ dist μ ν ^ 2 = ∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π ∧ ∃ (γ : ℝ → WassersteinSpace 2 E), IsGeodesicSegment γ μ ν ∧ ∀ t ∈ Set.Icc 0 1, ↑↑(γ t) = MeasureTheory.Measure.map (fun (z : E × E) => (1 - t) • z.1 + t • z.2) π

Quadratic linear interpolation. On a separable Banach space E, two laws μ and ν of finite second moment have an optimal coupling π for the quadratic cost: the displacement x - y is square integrable under π, with ∫ ‖x - y‖² dπ = W₂ (μ, ν)², and the laws of (1 - t) • x + t • y under π, for t ∈ [0, 1], trace a geodesic segment of P₂ (E) from μ to ν.

theorem TauCeti.WassersteinSpace.isGeodesicSegment_iff_exists_isOptimalCoupling {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [Fact (1 ≤ p)] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ ν : WassersteinSpace p E} {γ : ℝ → WassersteinSpace p E} : IsGeodesicSegment γ μ ν ↔ ∃ (π : MeasureTheory.Measure (E × E)), IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) π ↑↑μ ↑↑ν ∧ ∀ t ∈ Set.Icc 0 1, ↑↑(γ t) = MeasureTheory.Measure.map (fun (z : E × E) => (1 - t) • z.1 + t • z.2) π

The geodesics of P_p (E) are the linear interpolations of optimal couplings. Let E be a strictly convex separable Banach space and 1 < p < ∞. A curve γ is a geodesic segment of P_p (E) from μ to ν exactly when there is an optimal coupling π of μ and ν for the cost d ^ p such that for every t ∈ [0, 1] the law γ t is the law of (1 - t) • x + t • y under π. The optimal coupling need not be unique (Ambrosio–Gigli–Savaré, §7.2).