The monotone rearrangement is optimal for every Wasserstein exponent

For two probability laws μ and ν on ℝ and every exponent 1 ≤ p ≤ ∞,

W_p (μ, ν) = ‖μ.quantile - ν.quantile‖_{Lᵖ (0, 1)},

and the monotone coupling MeasureTheory.Measure.quantileCoupling attains it. For p < ∞ the right-hand side is (∫₀¹ |μ.quantile t - ν.quantile t| ^ p dt) ^ (1 / p), and at p = ∞ it is the essential supremum of |μ.quantile - ν.quantile| on (0, 1), by the eLpNorm convention. All of these are identities in [0, ∞] and need no moment hypothesis.

The upper bound is TauCeti.wassersteinEDist_le_eLpNorm_quantile_sub; the content here is the lower bound, a rearrangement inequality for the costs |x - y| ^ p. It rests on two facts.

• The Fréchet–Hoeffding bound. Every plan of μ and ν puts mass at least cdf μ a - cdf ν b on the quadrant Iic a ×ˢ Ioi b, and the monotone coupling puts exactly the positive part of that gap there. By the level-set formula for a positive part, the monotone coupling therefore has the least expected hinge cost (y - x - r)⁺ for every threshold r, and symmetrically for (x - y - r)⁺.
• Powers are mixtures of hinges. For 1 < p, |x - y| ^ p is the integral over r > 0 of p (p - 1) r ^ (p - 2) ((y - x - r)⁺ + (x - y - r)⁺), and for p = 1 it is the sum of the two hinges at r = 0 (TauCeti.edist_rpow_eq_lintegral and TauCeti.ofReal_sub_sub_add_ofReal_sub_sub). Integrating the hinge inequalities against this nonnegative weight gives the inequality for the power cost.

The exponent ∞ then follows from the finite exponents: both sides are limits of their finite-exponent values, by TauCeti.tendsto_wassersteinEDist_atTop and TauCeti.tendsto_eLpNorm_atTop.

Main statements

• TauCeti.ofReal_cdf_sub_le_measure — the Fréchet–Hoeffding bound on quadrants, attained by the monotone coupling (MeasureTheory.Measure.quantileCoupling_Iic_prod_Ioi);
• TauCeti.lintegral_ofReal_sub_sub_quantileCoupling_le — the monotone coupling minimizes every hinge cost;
• TauCeti.lintegral_edist_rpow_quantileCoupling_le and MeasureTheory.Measure.isOptimalCoupling_quantileCoupling — the monotone coupling is an optimal plan for the cost |x - y| ^ p whenever 1 ≤ p;
• TauCeti.wassersteinEDist_eq_eLpNorm_quantile_sub — the quantile formula for W_p, for every 1 ≤ p ≤ ∞, unfolded at the two kinds of exponent as TauCeti.wassersteinEDist_eq_lintegral_rpow_enorm_quantile_sub (the integral and root, for p < ∞, with p-th power TauCeti.wassersteinEDist_rpow_eq_lintegral_rpow_enorm_quantile_sub) and TauCeti.wassersteinEDist_top_eq_essSup_enorm_quantile_sub (the essential supremum, for p = ∞).

References

• C. Villani, Topics in Optimal Transportation, GSM 58, AMS 2003, §2.2, where the monotone rearrangement is shown optimal for the costs h (x - y) with h convex.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §2.2.
• S. Cambanis, G. Simons and W. Stout, Inequalities for E k(X, Y) when the marginals are fixed, Z. Wahrscheinlichkeitstheorie verw. Gebiete 36 (1976), 285–294.

theorem TauCeti.ofReal_cdf_sub_le_measure {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (ℝ × ℝ)} (hπ : IsCoupling π μ ν) (a b : ℝ) : ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) a - ↑(ProbabilityTheory.cdf ν) b) ≤ π (Set.Iic a ×ˢ Set.Ioi b)

The Fréchet–Hoeffding bound on a quadrant. Every transport plan of two real laws gives the quadrant Iic a ×ˢ Ioi b mass at least cdf μ a - cdf ν b: the pairs with first coordinate at most a carry mass cdf μ a, and at most cdf ν b of it has second coordinate at most b.

theorem TauCeti.lintegral_ofReal_sub_sub_quantileCoupling_le {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (ℝ × ℝ)} (hπ : IsCoupling π μ ν) (r : ℝ) : ∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (z.2 - z.1 - r) ∂μ.quantileCoupling ν ≤ ∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (z.2 - z.1 - r) ∂π

The monotone coupling minimizes every hinge cost. For every threshold r, no transport plan of two real laws has smaller expected hinge cost (y - x - r)⁺ than the monotone coupling.

theorem TauCeti.lintegral_edist_rpow_quantileCoupling_le {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (ℝ × ℝ)} (hπ : IsCoupling π μ ν) {p : ℝ} (hp : 1 ≤ p) : ∫⁻ (z : ℝ × ℝ), edist z.1 z.2 ^ p ∂μ.quantileCoupling ν ≤ ∫⁻ (z : ℝ × ℝ), edist z.1 z.2 ^ p ∂π

The rearrangement inequality for powers of the distance. For every exponent 1 ≤ p, no transport plan of two real laws has a smaller expected cost |x - y| ^ p than the monotone coupling.

theorem TauCeti.wassersteinEDist_eq_eLpNorm_quantile_sub {p : ENNReal} (hp : 1 ≤ p) (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p μ ν = MeasureTheory.eLpNorm (fun (t : ℝ) => μ.quantile t - ν.quantile t) p (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The one-dimensional quantile formula. For every exponent 1 ≤ p ≤ ∞, the p-Wasserstein distance of two probability laws on ℝ is the Lᵖ (0, 1) distance of their quantile functions. The identity holds in [0, ∞], without moment hypotheses.

theorem TauCeti.wassersteinEDist_eq_lintegral_rpow_enorm_quantile_sub {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p μ ν = (∫⁻ (t : ℝ) in Set.Ioo 0 1, ‖μ.quantile t - ν.quantile t‖ₑ ^ p.toReal) ^ (1 / p.toReal)

The quantile formula at a finite exponent. For 1 ≤ p < ∞, the p-Wasserstein distance of two probability laws on ℝ is (∫₀¹ |μ.quantile t - ν.quantile t| ^ p dt) ^ (1 / p).

theorem TauCeti.wassersteinEDist_rpow_eq_lintegral_rpow_enorm_quantile_sub {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist p μ ν ^ p.toReal = ∫⁻ (t : ℝ) in Set.Ioo 0 1, ‖μ.quantile t - ν.quantile t‖ₑ ^ p.toReal

The quantile formula for the transport cost. For 1 ≤ p < ∞, the p-th power of the p-Wasserstein distance of two probability laws on ℝ is ∫₀¹ |μ.quantile t - ν.quantile t| ^ p dt.

theorem TauCeti.wassersteinEDist_top_eq_essSup_enorm_quantile_sub (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : wassersteinEDist ⊤ μ ν = essSup (fun (t : ℝ) => ‖μ.quantile t - ν.quantile t‖ₑ) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The quantile formula at the exponent ∞. The ∞-Wasserstein distance of two probability laws on ℝ is the essential supremum of |μ.quantile - ν.quantile| on (0, 1).

theorem MeasureTheory.Measure.isOptimalCoupling_quantileCoupling (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {p : ℝ} (hp : 1 ≤ p) : TauCeti.IsOptimalCoupling (fun (z : ℝ × ℝ) => edist z.1 z.2 ^ p) (μ.quantileCoupling ν) μ ν

The monotone rearrangement is optimal. For every exponent 1 ≤ p, the monotone coupling of two real laws is an optimal transport plan for the cost |x - y| ^ p.