Displacement interpolation as a relation

TauCeti.IsDisplacementInterpolation p μ says that the curve of probability laws μ, indexed by the unit interval, is induced by an optimal dynamic plan concentrated on constant-speed geodesics. It does not select an optimal coupling or a geodesic between each pair of endpoints. In particular different presentations are allowed, and different interpolations can join the same endpoint laws.

For finite endpoint distance, IsDisplacementInterpolation.wassersteinEDist_eq proves the constant-speed Wasserstein distance formula for 1 ≤ p ≤ ∞. For the characterization of geodesic segments in P_p(X) when 1 < p < ∞, see TauCeti.WassersteinSpace.isGeodesicSegment_iff_isDisplacementInterpolation in TauCeti.MeasureTheory.OptimalTransport.Wasserstein.Geodesic.Basic. Uniqueness of interpolation follows from uniqueness of the endpoint optimizer together with almost-everywhere uniqueness of the ground geodesics; neither condition alone is substituted for both.

On a separable real normed space the affine interpolation of an optimal coupling satisfies this relation. The affine interpolation induced by an optimal transport map is also a displacement interpolation, without assuming that the transport map is everywhere measurable.

References

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

theorem TauCeti.IsDisplacementInterpolation.wassersteinEDist_eq {p : ENNReal} {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [StandardBorelSpace X] {μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure X} (h : IsDisplacementInterpolation p μ) (hp : 1 ≤ p) (hfin : wassersteinEDist p ↑(μ 0) ↑(μ 1) ≠ ⊤) (s t : ↑unitInterval) : wassersteinEDist p ↑(μ s) ↑(μ t) = edist s t * wassersteinEDist p ↑(μ 0) ↑(μ 1)

A displacement interpolation at finite endpoint distance has constant Wasserstein speed, including at the exponents one and infinity.

theorem TauCeti.exists_isDisplacementInterpolation {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] [IsGeodesicSpace X] (hp : 1 ≤ p) (μ₀ μ₁ : MeasureTheory.ProbabilityMeasure X) (hfin : wassersteinEDist p ↑μ₀ ↑μ₁ ≠ ⊤) : ∃ (μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure X), IsDisplacementInterpolation p μ ∧ μ 0 = μ₀ ∧ μ 1 = μ₁

Probability laws at finite Wasserstein distance on a Polish geodesic space admit a displacement interpolation. No moment hypothesis on either endpoint is required.

theorem TauCeti.IsDisplacementInterpolation.eq_of_ae_subsingleton {p : ENNReal} {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] {μ ν : ↑unitInterval → MeasureTheory.ProbabilityMeasure X} (hμ : IsDisplacementInterpolation p μ) (hν : IsDisplacementInterpolation p ν) (h0 : ν 0 = μ 0) (h1 : ν 1 = μ 1) {π : MeasureTheory.Measure (X × X)} (hπ : ∀ (π' : MeasureTheory.Measure (X × X)), IsCoupling π' ↑(μ 0) ↑(μ 1) → MeasureTheory.eLpNorm (fun (z : X × X) => edist z.1 z.2) p π' = wassersteinEDist p ↑(μ 0) ↑(μ 1) → π' = π) (hgeo : ∀ᵐ (z : X × X) ∂π, {c : C(↑unitInterval, X) | c ∈ geodesicPaths X ∧ c 0 = z.1 ∧ c 1 = z.2}.Subsingleton) : μ = ν

Under a unique endpoint optimizer and almost-everywhere uniqueness of ground geodesics, two displacement interpolations with the same endpoint laws coincide. This applies also to the infinite exponent, unlike the converse characterization of geodesics.

theorem TauCeti.isDisplacementInterpolation_of_map_smul_add_smul {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure E} {π : MeasureTheory.Measure (E × E)} (hopt : MeasureTheory.eLpNorm (fun (z : E × E) => edist z.1 z.2) p π = wassersteinEDist p ↑(μ 0) ↑(μ 1)) (hmarg : ∀ (t : ↑unitInterval), ↑(μ t) = MeasureTheory.Measure.map (fun (z : E × E) => (1 - ↑t) • z.1 + ↑t • z.2) π) : IsDisplacementInterpolation p μ

Affine interpolation of an optimal coupling is a displacement interpolation. The formula specifies the curve, but no choice of optimizer is built into the relation. Completeness and strict convexity of the norm are not needed for this construction.

theorem ProbabilityTheory.HasLaw.isDisplacementInterpolation_smul_add_smul {p : ENNReal} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] {μ : ↑unitInterval → MeasureTheory.ProbabilityMeasure E} {T : E → E} (hT : HasLaw T ↑(μ 1) ↑(μ 0)) (hopt : MeasureTheory.eLpNorm (fun (z : E × E) => edist z.1 z.2) p (TauCeti.graphPlan T ↑(μ 0)) = TauCeti.wassersteinEDist p ↑(μ 0) ↑(μ 1)) (hmarg : ∀ (t : ↑unitInterval), ↑(μ t) = MeasureTheory.Measure.map (fun (x : E) => (1 - ↑t) • x + ↑t • T x) ↑(μ 0)) : TauCeti.IsDisplacementInterpolation p μ

The affine curve induced by an optimal transport map is a displacement interpolation. Transport-map feasibility is HasLaw, so an a.e.-measurable representative suffices.