The monotone quantile coupling of two real laws

Two probability laws on ℝ are simultaneously represented by their quantile functions: each is the law of its own quantile function under the uniform law on the open unit interval. Reading the two quantile functions off the same uniform variable produces the monotone coupling

μ.quantileCoupling ν = (volume.restrict (Ioo 0 1)).map fun t ↦ (μ.quantile t, ν.quantile t),

the classical monotone rearrangement of the two laws: both coordinates are nondecreasing functions of one and the same variable, by MeasureTheory.Measure.monotoneOn_quantile. It is a genuine transport plan of μ and ν, and its transport objective for the ground distance of ℝ is the L^p (0,1) distance of the two quantile functions. Every p-Wasserstein distance of two real laws is therefore at most that explicit one-dimensional integral.

The reverse inequality — that the monotone coupling is optimal, so that the bound below is an identity for every exponent 1 ≤ p ≤ ∞ — is a rearrangement inequality for the costs |x - y| ^ p, proved in TauCeti.MeasureTheory.OptimalTransport.Wasserstein.Rearrangement as TauCeti.wassersteinEDist_eq_eLpNorm_quantile_sub.

Main definitions

• MeasureTheory.Measure.quantileCoupling — the monotone coupling of two real laws.

Main statements

• MeasureTheory.Measure.isCoupling_quantileCoupling — the monotone coupling is a transport plan;
• MeasureTheory.Measure.ae_fst_le_snd_quantileCoupling — it is concentrated on ordered pairs whenever the cdfs are ordered;
• MeasureTheory.Measure.quantileCoupling_Iic_prod_Ioi — its mass on a quadrant Iic a ×ˢ Ioi b is the positive part of cdf μ a - cdf ν b;
• TauCeti.eLpNorm_edist_quantileCoupling — its transport objective is the L^p (0,1) distance of the two quantile functions;
• TauCeti.wassersteinEDist_le_eLpNorm_quantile_sub — the resulting upper bound on the Wasserstein distance of two real laws.

References

• C. Villani, Topics in Optimal Transportation, GSM 58, AMS 2003, §2.2, where the monotone rearrangement of two real laws is built from the quantile functions.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §2.2.

noncomputable def MeasureTheory.Measure.quantileCoupling (μ ν : Measure ℝ) : Measure (ℝ × ℝ)

The monotone coupling of two laws on ℝ: the joint law of the two quantile functions read off a single uniform variable on the open unit interval. Both coordinates are nondecreasing in that variable, which is what makes the plan the monotone rearrangement of the two laws.

theorem MeasureTheory.Measure.quantileCoupling_def (μ ν : Measure ℝ) : μ.quantileCoupling ν = map (fun (t : ℝ) => (μ.quantile t, ν.quantile t)) (volume.restrict (Set.Ioo 0 1))

The monotone coupling is the pushforward of the uniform law along the pair of quantile functions. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

theorem MeasureTheory.Measure.isCoupling_quantileCoupling (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : TauCeti.IsCoupling (μ.quantileCoupling ν) μ ν

The monotone coupling is a transport plan of the two laws: inverse transform sampling identifies each of its marginals.

instance MeasureTheory.Measure.isProbabilityMeasure_quantileCoupling (μ ν : Measure ℝ) : IsProbabilityMeasure (μ.quantileCoupling ν)

The monotone coupling of any two laws on ℝ is a probability measure, being a pushforward of the uniform law on the open unit interval.

@[simp]

theorem MeasureTheory.Measure.map_swap_quantileCoupling (μ ν : Measure ℝ) : map Prod.swap (μ.quantileCoupling ν) = ν.quantileCoupling μ

Exchanging the coordinates of the monotone coupling of μ and ν gives the monotone coupling of ν and μ.

theorem MeasureTheory.Measure.ae_fst_le_snd_quantileCoupling (μ ν : Measure ℝ) (h : ∀ (x : ℝ), ↑(ProbabilityTheory.cdf ν) x ≤ ↑(ProbabilityTheory.cdf μ) x) : ∀ᵐ (z : ℝ × ℝ) ∂μ.quantileCoupling ν, z.1 ≤ z.2

If the cdfs are ordered, the common-uniform quantile coupling is concentrated on ordered pairs. Thus the stochastic comparison is realized by random variables satisfying X ≤ Y almost surely.

@[simp]

theorem MeasureTheory.Measure.quantileCoupling_Iic_prod_Ioi (μ ν : Measure ℝ) (a b : ℝ) : (μ.quantileCoupling ν) (Set.Iic a ×ˢ Set.Ioi b) = ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) a - ↑(ProbabilityTheory.cdf ν) b)

The monotone coupling on a quadrant. The monotone coupling of two real laws gives the quadrant Iic a ×ˢ Ioi b the positive part of the gap cdf μ a - cdf ν b: the uniform levels t with μ.quantile t ≤ a and b < ν.quantile t are those with cdf ν b < t ≤ cdf μ a.

theorem TauCeti.eLpNorm_edist_quantileCoupling (p : ENNReal) (μ ν : MeasureTheory.Measure ℝ) : MeasureTheory.eLpNorm (fun (z : ℝ × ℝ) => edist z.1 z.2) p (μ.quantileCoupling ν) = MeasureTheory.eLpNorm (fun (t : ℝ) => μ.quantile t - ν.quantile t) p (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The transport objective of the monotone coupling is the L^p (0,1) distance of the two quantile functions.

theorem TauCeti.wassersteinEDist_le_eLpNorm_quantile_sub (p : ENNReal) (μ ν : 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 p-Wasserstein distance of two real laws is at most the L^p (0,1) distance of their quantile functions, the transport objective of the monotone coupling.