Proposition 3.6 - uniqueness on paired routes

Proved

ExcursionCoupling.coupling_eq_of_concentrated_on_paired_routes

by ykanoria · Aug 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

couplingmeasure-theoryoptimal-transportuniqueness

Let $\mu$ and $\nu$ be mutually singular Borel probability measures on $\mathbf{R}$ , let $F_\sigma=F_\mu-F_\nu$ , and let $\Gamma$ be the set of paired routes obtained by pairing consecutive increasing and decreasing crossings at every nonzero regular level of the completed graph of $F_\sigma$ .

If $\pi$ and $\pi'$ are two transport plans with first marginal $\mu$ and second marginal $\nu$ , and both are concentrated on $\Gamma$ , then

\pi'=\pi.

Thus the prescribed marginals uniquely determine the coupling carried by the completed-graph paired routes, including when the marginals have atoms. This is the uniqueness theorem for the excursion coupling.

Formalization Note Concentration is stated as zero mass on $\Gamma^{\mathrm c}$ . The measures $\pi$ and $\pi'$ are not separately assumed to be probability measures because either marginal identity already fixes their total mass to one.

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem coupling_eq_of_concentrated_on_paired_routes
    (mu nu : Measure Real)
    [IsProbabilityMeasure mu] [IsProbabilityMeasure nu]
    (hsing : mu ⟂ₘ nu)
    (pi pi' : Measure (Real × Real))
    (hpiFst : pi.map Prod.fst = mu) (hpiSnd : pi.map Prod.snd = nu)
    (hpiConc : pi (pairedRoutes (Fsigma mu nu))ᶜ = 0)
    (hpi'Fst : pi'.map Prod.fst = mu) (hpi'Snd : pi'.map Prod.snd = nu)
    (hpi'Conc : pi' (pairedRoutes (Fsigma mu nu))ᶜ = 0) :
    pi' = pi := by sorry

end ExcursionCoupling

Source

Nicolas Juillet, On a solution to the Monge transport problem on the real line arising from the strictly concave case, arXiv:1907.00681v1 (2019), https://arxiv.org/abs/1907.00681; Proposition 3.6, pp. 18-19, especially eq. (17)

View graph