The Wasserstein distance of two real laws at exponent one

On the real line the transport problem for the ground distance is solved explicitly: for two probability laws μ and ν on ℝ,

W₁ (μ, ν) = ∫⁻ s, ‖cdf μ s - cdf ν s‖ₑ,

the area between the two cumulative distribution functions. This is an identity in [0, ∞] and needs no moment hypothesis: its two sides are infinite together, so laws with divergent first moments are covered as they stand.

One measure-theoretic identity, proved in TauCeti.MeasureTheory.Integral.LayerCake, drives it, TauCeti.lintegral_enorm_sub_eq_lintegral_measure_symmDiff: the L¹ distance of two real functions is the integral, over the levels s, of the measure of the set where exactly one of them is at most s. On the two coordinates of a transport plan it rewrites the transport objective as an integral of plan masses, each at least the gap between the two cumulative distribution functions at that level, since a set on which exactly one coordinate is small carries at least the difference of the two marginal masses. On the two quantile functions it rewrites the objective of the monotone plan as the integral of exactly those gaps, by the Galois property of the quantile. Lower bound and attained value therefore meet.

The quantile form of this identity, W₁ (μ, ν) = ‖μ.quantile - ν.quantile‖_{L¹ (0, 1)}, is the exponent-one case of TauCeti.wassersteinEDist_eq_eLpNorm_quantile_sub, which holds for every exponent 1 ≤ p ≤ ∞; the cumulative-distribution form is special to the exponent one.

Main statements

• TauCeti.lintegral_enorm_quantile_sub_eq_lintegral_enorm_cdf_sub — the L¹ (0, 1) distance of the two quantile functions is the area between the two cumulative distribution functions;
• TauCeti.wassersteinEDist_one_eq_lintegral_enorm_cdf_sub — the Wasserstein distance at exponent one is that area.

References

• S. S. Vallender, Calculation of the Wasserstein distance between probability distributions on the line, Theory of Probability and its Applications 18 (1974), 784--786.
• C. Villani, Topics in Optimal Transportation, GSM 58, AMS 2003, §2.2.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §2.2.

theorem TauCeti.enorm_cdf_sub_le_measure_symmDiff {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (ℝ × ℝ)} (hπ : IsCoupling π μ ν) (s : ℝ) : ‖↑(ProbabilityTheory.cdf μ) s - ↑(ProbabilityTheory.cdf ν) s‖ₑ ≤ π (symmDiff {z : ℝ × ℝ | z.1 ≤ s} {z : ℝ × ℝ | z.2 ≤ s})

On a transport plan of two real laws, the set of pairs whose two coordinates are separated by the level s has mass at least the gap between the two cumulative distribution functions at s.

theorem TauCeti.lintegral_enorm_quantile_sub_eq_lintegral_enorm_cdf_sub (μ ν : MeasureTheory.Measure ℝ) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, ‖μ.quantile t - ν.quantile t‖ₑ = ∫⁻ (s : ℝ), ‖↑(ProbabilityTheory.cdf μ) s - ↑(ProbabilityTheory.cdf ν) s‖ₑ

The L¹ (0, 1) distance of the two quantile functions is the area between the two cumulative distribution functions.

theorem TauCeti.wassersteinEDist_one_eq_lintegral_enorm_cdf_sub (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist 1 μ ν = ∫⁻ (s : ℝ), ‖↑(ProbabilityTheory.cdf μ) s - ↑(ProbabilityTheory.cdf ν) s‖ₑ

The one-dimensional Kantorovich formula. The Wasserstein distance at exponent one of two probability laws on ℝ is the area between their cumulative distribution functions.