Dynamic plans concentrated on geodesics

A dynamic plan on a metric space X is a measure η on the path space C(I, X). Its law at time t, η.timeMarginal t, is the pushforward of η along the evaluation at t, and its endpoint law η.endpointLaw is the pushforward along γ ↦ (γ 0, γ 1), a measure on X × X whose marginals are the laws at times 0 and 1. When η is concentrated on the geodesic paths TauCeti.geodesicPaths X, the laws at times s and t are coupled by the law of (γ s, γ t), and each coupled pair is at distance |s - t| times the distance between the endpoints of its geodesic. This gives the displacement bound W_p (η_s, η_t) ≤ |s - t| * ‖d‖_{Lᵖ(π)} for every exponent p, where π is the endpoint law.

Conversely, on a Polish metric space every law π of pairs of points almost all of which are joined by a geodesic (for instance, any law on a geodesic space) is the endpoint law of a dynamic plan concentrated on geodesics. The relation between a pair of points and the geodesic paths joining them is closed (TauCeti.isClosed_setOf_mem_geodesicPaths_endpoints), hence analytic in the Polish space (X × X) × C(I, X), so the Jankov–von Neumann uniformization theorem chooses, measurably in the pair of endpoints and for π-almost every pair, a geodesic joining them. The pushforward of π along this choice is the required dynamic plan. No global Borel choice of geodesics is claimed: the choice depends on π and is only defined π-almost everywhere. When almost every pair of points under π is joined by only one geodesic path, this dynamic plan is the only one: every plan concentrated on geodesics with endpoint law π is the pushforward of π along the chosen geodesics.

Applied to an optimal coupling π of μ and ν on a Polish geodesic space, for a finite nonzero exponent p, the laws at times 0 ≤ t ≤ 1 of this dynamic plan interpolate between μ and ν, with W_p (η_s, η_t) ≤ |s - t| * W_p (μ, ν).

Main definitions

• MeasureTheory.Measure.timeMarginal η t: the law at time t of a dynamic plan η.
• MeasureTheory.Measure.endpointLaw η: the joint law of the two endpoints of a dynamic plan η.
• MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan: a dynamic plan concentrated on geodesics whose endpoint law is a quadratic optimal coupling.

A dynamic plan is a plain Measure C(I, X), so these declarations live in the namespace of Mathlib's MeasureTheory.Measure, where dot notation such as η.timeMarginal t finds them.

Main results

• MeasureTheory.Measure.exists_measurable_ae_mem_geodesicPaths: on a Polish metric space, relative to an s-finite law of pairs of points almost all of which are joined by a geodesic, a geodesic joining almost every pair can be chosen measurably in the pair.
• MeasureTheory.Measure.exists_ae_mem_geodesicPaths_endpointLaw_eq: every such law of pairs of points is the endpoint law of a dynamic plan concentrated on geodesics.
• MeasureTheory.Measure.ae_exists_mem_geodesicPaths_endpointLaw: on a Polish metric space, almost every pair of endpoints of a dynamic plan concentrated on geodesics is joined by a geodesic path.
• MeasureTheory.Measure.eq_of_endpointLaw_eq_of_ae_subsingleton: on a Polish metric space, two dynamic plans concentrated on geodesics with the same endpoint law are equal when almost every pair of endpoints is joined by at most one geodesic path.
• TauCeti.ae_timeMarginal_mem_closedBall: if the laws at times 0 and 1 of a dynamic plan concentrated on geodesics are carried by closed balls about a point, so is its law at every time.
• TauCeti.eLpNorm_edist_map_eq: for a dynamic plan concentrated on geodesics, the Lᵖ displacement of its joint law at times s and t is |s - t| times that of its endpoint law.
• TauCeti.wassersteinEDist_timeMarginal_le: the displacement bound between the laws at two times of a dynamic plan concentrated on geodesics.
• TauCeti.exists_ae_mem_geodesicPaths_wassersteinEDist_timeMarginal_le: on a Polish geodesic space and for a finite nonzero exponent p, two finite measures with a coupling are the laws at times 0 and 1 of a dynamic plan concentrated on geodesics whose laws at times s and t are within |s - t| * W_p (μ, ν) of each other.

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.

noncomputable def MeasureTheory.Measure.timeMarginal {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) (t : ↑unitInterval) : Measure X

The law at time t of a dynamic plan η on the path space C(I, X): the pushforward of η along the evaluation γ ↦ γ t.

noncomputable def MeasureTheory.Measure.endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) : Measure (X × X)

The endpoint law of a dynamic plan η on the path space C(I, X): the pushforward of η along γ ↦ (γ 0, γ 1), the joint law of the initial and final points of a path.

theorem MeasureTheory.Measure.timeMarginal_def {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) (t : ↑unitInterval) : η.timeMarginal t = map (fun (γ : C(↑unitInterval, X)) => γ t) η

The law at time t is the pushforward along the evaluation at t.

theorem MeasureTheory.Measure.endpointLaw_def {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) : η.endpointLaw = map (fun (γ : C(↑unitInterval, X)) => (γ 0, γ 1)) η

The endpoint law is the pushforward along the pair of endpoints.

instance MeasureTheory.Measure.isFiniteMeasure_timeMarginal {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) [IsFiniteMeasure η] (t : ↑unitInterval) : IsFiniteMeasure (η.timeMarginal t)

A finite dynamic plan has finite laws at every time.

instance MeasureTheory.Measure.isFiniteMeasure_endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) [IsFiniteMeasure η] : IsFiniteMeasure η.endpointLaw

A finite dynamic plan has a finite endpoint law.

instance MeasureTheory.Measure.isProbabilityMeasure_timeMarginal {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) [IsProbabilityMeasure η] (t : ↑unitInterval) : IsProbabilityMeasure (η.timeMarginal t)

A probability dynamic plan has probability laws at every time.

instance MeasureTheory.Measure.isProbabilityMeasure_endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) [IsProbabilityMeasure η] : IsProbabilityMeasure η.endpointLaw

A probability dynamic plan has a probability endpoint law.

instance MeasureTheory.Measure.sFinite_endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) [SFinite η] : SFinite η.endpointLaw

An s-finite dynamic plan has an s-finite endpoint law.

theorem ContinuousMap.measurable_endpoints {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] : Measurable fun (γ : C(↑unitInterval, X)) => (γ 0, γ 1)

The pair of endpoints γ ↦ (γ 0, γ 1) of a path is a measurable function on C(I, X).

theorem MeasureTheory.Measure.timeMarginal_apply {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) (t : ↑unitInterval) {s : Set X} (hs : MeasurableSet s) : (η.timeMarginal t) s = η {γ : C(↑unitInterval, X) | γ t ∈ s}

The value of the law at time t on a measurable set s is the η-measure of the paths lying in s at time t.

theorem MeasureTheory.Measure.endpointLaw_apply {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) {s : Set (X × X)} (hs : MeasurableSet s) : η.endpointLaw s = η {γ : C(↑unitInterval, X) | (γ 0, γ 1) ∈ s}

The value of the endpoint law on a measurable set s is the η-measure of the paths whose pair of endpoints lies in s.

@[simp]

theorem MeasureTheory.Measure.fst_endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) : η.endpointLaw.fst = η.timeMarginal 0

The first marginal of the endpoint law is the law at time 0.

@[simp]

theorem MeasureTheory.Measure.snd_endpointLaw {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) : η.endpointLaw.snd = η.timeMarginal 1

The second marginal of the endpoint law is the law at time 1.

theorem MeasureTheory.Measure.isCoupling_map_timeMarginal {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) (s t : ↑unitInterval) : TauCeti.IsCoupling (map (fun (γ : C(↑unitInterval, X)) => (γ s, γ t)) η) (η.timeMarginal s) (η.timeMarginal t)

The joint law at times s and t of a dynamic plan couples its laws at those two times.

theorem MeasureTheory.Measure.timeMarginal_mono {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {η η' : Measure C(↑unitInterval, X)} (h : η ≤ η') (t : ↑unitInterval) : η.timeMarginal t ≤ η'.timeMarginal t

The law at time t is monotone in the dynamic plan.

@[simp]

theorem MeasureTheory.Measure.timeMarginal_smul {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (c : ENNReal) (η : Measure C(↑unitInterval, X)) (t : ↑unitInterval) : (c • η).timeMarginal t = c • η.timeMarginal t

Scaling a dynamic plan by c scales its law at every time by c.

theorem MeasureTheory.Measure.timeMarginal_map {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {α : Type u_2} [MeasurableSpace α] (μ : Measure α) {F : α → C(↑unitInterval, X)} (hF : Measurable F) (t : ↑unitInterval) : (map F μ).timeMarginal t = map (fun (a : α) => (F a) t) μ

The law at time t of the image of a measure μ under a measurable family of paths F is the image of μ under a ↦ F a t.

theorem MeasureTheory.Measure.ae_timeMarginal_iff {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {η : Measure C(↑unitInterval, X)} {t : ↑unitInterval} {p : X → Prop} (hp : MeasurableSet {x : X | p x}) : (∀ᵐ (x : X) ∂η.timeMarginal t, p x) ↔ ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, p (γ t)

A measurable property holds almost everywhere for the law at time t exactly when almost every path has it at time t.

theorem MeasureTheory.Measure.ae_eq_of_timeMarginal_eq_dirac {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [MeasurableSingletonClass X] {η : Measure C(↑unitInterval, X)} {t : ↑unitInterval} {x : X} (h : η.timeMarginal t = dirac x) : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ t = x

If the law at time t is the Dirac mass at x, almost every path passes through x at time t.

theorem MeasureTheory.Measure.timeMarginal_withDensity_apply_of_ae_eq {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {η : Measure C(↑unitInterval, X)} {w : C(↑unitInterval, X) → ENNReal} {c : ENNReal} {t : ↑unitInterval} {s : Set X} (hs : MeasurableSet s) (hw : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ t ∈ s → w γ = c) : ((η.withDensity w).timeMarginal t) s = c * η {γ : C(↑unitInterval, X) | γ t ∈ s}

If the density w equals c at almost every path lying in s at time t, then the law at time t of η weighted by w gives s the mass c * η {γ | γ t ∈ s}.

theorem MeasureTheory.Measure.ae_mem_geodesicPaths_map_segmentPath {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] (π : Measure (E × E)) : ∀ᵐ (c : C(↑unitInterval, E)) ∂map (⇑TauCeti.segmentPath) π, c ∈ TauCeti.geodesicPaths E

Lifting a law of pairs of points to their affine segments gives a plan concentrated on constant-speed geodesics, without requiring completeness or strict convexity.

@[simp]

theorem MeasureTheory.Measure.endpointLaw_map_segmentPath {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] (π : Measure (E × E)) : (map (⇑TauCeti.segmentPath) π).endpointLaw = π

The endpoint law of the affine-segment lift is the original law of pairs of points.

theorem MeasureTheory.Measure.timeMarginal_map_segmentPath {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] (π : Measure (E × E)) (t : ↑unitInterval) : (map (⇑TauCeti.segmentPath) π).timeMarginal t = map (fun (z : E × E) => (1 - ↑t) • z.1 + ↑t • z.2) π

The law at time t of the affine-segment lift is affine interpolation of the endpoint law.

theorem MeasureTheory.Measure.exists_measurable_ae_mem_geodesicPaths {X : Type u_2} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (π : Measure (X × X)) [SFinite π] (hπ : ∀ᵐ (z : X × X) ∂π, ∃ γ ∈ TauCeti.geodesicPaths X, γ 0 = z.1 ∧ γ 1 = z.2) : ∃ (G : X × X → C(↑unitInterval, X)), Measurable G ∧ ∀ᵐ (z : X × X) ∂π, G z ∈ TauCeti.geodesicPaths X ∧ (G z) 0 = z.1 ∧ (G z) 1 = z.2

Measurable choice of geodesics. On a Polish metric space, relative to an s-finite law π of pairs of points almost all of which are joined by a geodesic path, there is a Borel map choosing, for π-almost every pair z, a geodesic path from z.1 to z.2.

theorem MeasureTheory.Measure.exists_ae_mem_geodesicPaths_endpointLaw_eq {X : Type u_2} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (π : Measure (X × X)) [SFinite π] (hπ : ∀ᵐ (z : X × X) ∂π, ∃ γ ∈ TauCeti.geodesicPaths X, γ 0 = z.1 ∧ γ 1 = z.2) : ∃ (η : Measure C(↑unitInterval, X)), SFinite η ∧ (∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ TauCeti.geodesicPaths X) ∧ η.endpointLaw = π

Lifting a law of pairs to geodesics. On a Polish metric space, every s-finite law π of pairs of points almost all of which are joined by a geodesic path is the endpoint law of an s-finite dynamic plan concentrated on geodesic paths.

theorem MeasureTheory.Measure.ae_exists_mem_geodesicPaths_endpointLaw {X : Type u_2} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (η : Measure C(↑unitInterval, X)) [SFinite η] (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ TauCeti.geodesicPaths X) : ∀ᵐ (z : X × X) ∂η.endpointLaw, ∃ γ ∈ TauCeti.geodesicPaths X, γ 0 = z.1 ∧ γ 1 = z.2

The endpoints of a plan on geodesics are joined by geodesics. On a Polish metric space, if an s-finite dynamic plan η is concentrated on geodesic paths, then almost every pair of points under its endpoint law is joined by a geodesic path.

theorem MeasureTheory.Measure.eq_of_endpointLaw_eq_of_ae_subsingleton {X : Type u_2} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] {η η' : Measure C(↑unitInterval, X)} [SFinite η] (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ TauCeti.geodesicPaths X) (hη' : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η', γ ∈ TauCeti.geodesicPaths X) (h : η.endpointLaw = η'.endpointLaw) (huniq : ∀ᵐ (z : X × X) ∂η.endpointLaw, {γ : C(↑unitInterval, X) | γ ∈ TauCeti.geodesicPaths X ∧ γ 0 = z.1 ∧ γ 1 = z.2}.Subsingleton) : η = η'

A plan on geodesics is determined by its endpoint law when geodesics are unique. On a Polish metric space, let η and η' be dynamic plans concentrated on geodesic paths with the same endpoint law, and suppose that almost every pair of points under this law is joined by at most one geodesic path. Then η = η'.

structure MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan {X : Type u_2} [MetricSpace X] [MeasurableSpace X] (η : Measure C(↑unitInterval, X)) (μ₀ μ₁ : ProbabilityMeasure X) : Prop

A quadratic optimal dynamic plan from μ₀ to μ₁: a measure on path space concentrated on constant-speed geodesics whose endpoint law is an optimal coupling for the squared-distance cost. The optimal-coupling field forces the plan to have total mass one when the endpoints are probability laws.

• ae_mem_geodesicPaths : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ TauCeti.geodesicPaths X

  Almost every path of the dynamic plan is a constant-speed geodesic.

• endpointLaw_isOptimalCoupling : TauCeti.IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ 2) η.endpointLaw ↑μ₀ ↑μ₁

  The joint law of the two endpoints is a quadratic optimal coupling.

theorem MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan.endpointLaw_isCoupling {X : Type u_2} [MetricSpace X] [MeasurableSpace X] {η : Measure C(↑unitInterval, X)} {μ₀ μ₁ : ProbabilityMeasure X} (hη : η.IsQuadraticOptimalDynamicPlan μ₀ μ₁) : TauCeti.IsCoupling η.endpointLaw ↑μ₀ ↑μ₁

The endpoint law of a quadratic optimal dynamic plan couples its prescribed endpoints.

theorem MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan.timeMarginal_zero {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {η : Measure C(↑unitInterval, X)} {μ₀ μ₁ : ProbabilityMeasure X} (hη : η.IsQuadraticOptimalDynamicPlan μ₀ μ₁) : η.timeMarginal 0 = ↑μ₀

The time-zero marginal of a quadratic optimal dynamic plan is its source law.

theorem MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan.timeMarginal_one {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {η : Measure C(↑unitInterval, X)} {μ₀ μ₁ : ProbabilityMeasure X} (hη : η.IsQuadraticOptimalDynamicPlan μ₀ μ₁) : η.timeMarginal 1 = ↑μ₁

The time-one marginal of a quadratic optimal dynamic plan is its target law.

theorem MeasureTheory.Measure.IsQuadraticOptimalDynamicPlan.isProbabilityMeasure {X : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {η : Measure C(↑unitInterval, X)} {μ₀ μ₁ : ProbabilityMeasure X} (hη : η.IsQuadraticOptimalDynamicPlan μ₀ μ₁) : IsProbabilityMeasure η

A quadratic optimal dynamic plan between probability laws is itself a probability measure on path space.

theorem TauCeti.ae_timeMarginal_mem_closedBall {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] {η : MeasureTheory.Measure C(↑unitInterval, X)} (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) {x : X} {r₀ r₁ : ℝ} (h₀ : ∀ᵐ (y : X) ∂η.timeMarginal 0, y ∈ Metric.closedBall x r₀) (h₁ : ∀ᵐ (y : X) ∂η.timeMarginal 1, y ∈ Metric.closedBall x r₁) (t : ↑unitInterval) : ∀ᵐ (y : X) ∂η.timeMarginal t, y ∈ Metric.closedBall x ((1 - ↑t) * (r₀ + r₁) + r₁)

Geodesic plans stay near their endpoints. If a dynamic plan η concentrated on geodesic paths has its laws at times 0 and 1 carried by the closed balls of radii r₀ and r₁ about x, then its law at time t is carried by the closed ball of radius (1 - t) (r₀ + r₁) + r₁ about x: the point at time t is within 1 - t times the endpoint distance of the endpoint at time 1.

theorem TauCeti.eLpNorm_edist_map_eq {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] {η : MeasureTheory.Measure C(↑unitInterval, X)} (hη : ∀ᵐ (γ : C(↑unitInterval, X)) ∂η, γ ∈ geodesicPaths X) (p : ENNReal) (s t : ↑unitInterval) : MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p (MeasureTheory.Measure.map (fun (γ : C(↑unitInterval, X)) => (γ s, γ t)) η) = edist s t * MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p η.endpointLaw

The displacement along geodesics. For a dynamic plan η concentrated on geodesic paths, the Lᵖ size of the ground distance under the joint law at times s and t is |s - t| times its Lᵖ size under the endpoint law.

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

The displacement bound along geodesics. For a dynamic plan η concentrated on geodesic paths, the p-Wasserstein distance between its laws at times s and t is at most |s - t| times the Lᵖ size of the ground distance under its endpoint law.

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

Geodesic interpolation of an optimal coupling. On a Polish geodesic space, for a finite nonzero exponent p, two finite measures μ and ν admitting a coupling are the laws at times 0 and 1 of a finite dynamic plan η concentrated on geodesic paths whose laws at any two times s and t are within |s - t| * W_p (μ, ν) of each other. The dynamic plan lifts an optimal coupling of μ and ν.