Documentation

TauCeti.MeasureTheory.OptimalTransport.Wasserstein.Geodesic.Unique

Uniqueness of Wasserstein geodesics #

Let X be a complete separable metric space and 1 < p < ∞. Two laws μ and ν of finite p-th moment can be joined by several geodesic segments of P_p (X), for two independent reasons. Two points of X joined by two geodesics give two geodesic segments between the Dirac laws at these points. In the plane, the laws (δ_(0,0) + δ_(1,1)) / 2 and (δ_(1,0) + δ_(0,1)) / 2 have two optimal couplings, matching each point to either of its two neighbours, and their linear interpolations are two geodesic segments, although the plane is uniquely geodesic.

This file proves that these are the only obstructions. If the optimal coupling π of μ and ν for the cost d ^ p is unique, and π-almost every pair of points is joined by only one geodesic of X, then any two geodesic segments of P_p (X) from μ to ν agree on [0, 1] (TauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_ae_subsingleton). By Lisini's superposition principle each geodesic segment is the curve of laws of a dynamic plan concentrated on geodesic paths whose endpoint law is an optimal coupling of μ and ν, hence is π (TauCeti.WassersteinSpace.exists_ae_mem_geodesicPaths_of_isGeodesicSegment). When geodesics are almost surely unique such a plan is determined by its endpoint law (MeasureTheory.Measure.eq_of_endpointLaw_eq_of_ae_subsingleton), so the two geodesic segments have the same laws at all times.

In a strictly convex separable Banach space E 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 ν (TauCeti.WassersteinSpace.isGeodesicSegment_iff_exists_isOptimalCoupling), so when the optimal coupling is unique they are exactly the linear interpolation of π. On a finite-dimensional real inner product space, Brenier's theorem makes the quadratic optimal coupling out of an absolutely continuous law μ unique, and the graph plan of the Brenier map T. Every geodesic segment of P₂ (E) out of μ is then McCann's displacement interpolation t ↦ ((1 - t) • id + t • T)₊ μ, and in particular there is only one.

Main results #

References #

source
theorem TauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_ae_subsingleton {p : ENNReal} [Fact (1 ≤ p)] {X : Type u_1} [MetricSpace X] [CompleteSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ ν : WassersteinSpace p X} {π : MeasureTheory.Measure (X × X)} (hπ : ∀ (π' : MeasureTheory.Measure (X × X)), IsOptimalCoupling (fun (z : X × X) => edist z.1 z.2 ^ p.toReal) π' ↑↑μ ↑↑ν → π' = π) (hgeo : ∀ᵐ (z : X × X) ∂π, {c : C(↑unitInterval, X) | c ∈ geodesicPaths X ∧ c 0 = z.1 ∧ c 1 = z.2}.Subsingleton) {γ γ' : ℝ → WassersteinSpace p X} (h : IsGeodesicSegment γ μ ν) (h' : IsGeodesicSegment γ' μ ν) :
Set.EqOn γ γ' (Set.Icc 0 1)

Uniqueness of Wasserstein geodesics. Let X be a complete separable metric space and 1 < p < ∞. Suppose that every optimal coupling of μ and ν for the cost d ^ p is π, and that π-almost every pair of points of X is joined by at most one geodesic path. Then any two geodesic segments of P_p (X) from μ to ν agree on [0, 1].

source
theorem TauCeti.WassersteinSpace.isGeodesicSegment_iff_coe_eq_map_smul_add_smul {p : ENNReal} [Fact (1 ≤ p)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ ν : WassersteinSpace p E} {π : MeasureTheory.Measure (E × E)} (hπ : ∀ (π' : MeasureTheory.Measure (E × E)), IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) π' ↑↑μ ↑↑ν → π' = π) {γ : ℝ → WassersteinSpace p E} :
IsGeodesicSegment γ μ ν ↔ ∀ 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) under a unique optimal coupling. Let E be a strictly convex separable Banach space and 1 < p < ∞. If every optimal coupling of μ and ν for the cost d ^ p is π, then a curve γ is a geodesic segment of P_p (E) from μ to ν exactly when for every t ∈ [0, 1] the law γ t is the law of (1 - t) • x + t • y under π.

source
theorem TauCeti.WassersteinSpace.isGeodesicSegment_iff_coe_eq_map_smul_add_smul_of_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : WassersteinSpace 2 E} (hμ : (↑↑μ).AbsolutelyContinuous ρ) {T : E → E} (hT : IsKantorovichOptimalTransportMap (fun (z : E × E) => ENNReal.ofReal (‖z.1 - z.2‖ ^ 2 / 2)) (↑↑μ) (↑↑ν) T) {γ : ℝ → WassersteinSpace 2 E} :
IsGeodesicSegment γ μ ν ↔ ∀ t ∈ Set.Icc 0 1, ↑↑(γ t) = MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) ↑↑μ

Geodesics out of an absolutely continuous law are McCann's interpolation. Let E be a finite-dimensional real inner product space, let μ and ν be laws of finite second moment with μ absolutely continuous with respect to an additive Haar measure, and let T be a Brenier map, an optimal transport map from μ to ν for the cost ‖x - y‖ ^ 2 / 2. Then a curve γ is a geodesic segment of P₂ (E) from μ to ν exactly when for every t ∈ [0, 1] the law γ t is the image of μ under x ↦ (1 - t) • x + t • T x.

source
theorem TauCeti.WassersteinSpace.eqOn_of_isGeodesicSegment_of_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {ρ : MeasureTheory.Measure E} [ρ.IsAddHaarMeasure] {μ ν : WassersteinSpace 2 E} (hμ : (↑↑μ).AbsolutelyContinuous ρ) {γ γ' : ℝ → WassersteinSpace 2 E} (h : IsGeodesicSegment γ μ ν) (h' : IsGeodesicSegment γ' μ ν) :
Set.EqOn γ γ' (Set.Icc 0 1)

Uniqueness of geodesics out of an absolutely continuous law. On a finite-dimensional real inner product space, if μ is absolutely continuous with respect to an additive Haar measure, any two geodesic segments of P₂ (E) from μ to ν agree on [0, 1].