Prove2Me

Main Theorem: a monotone plan is the unique excursion coupling

Proved
ExcursionCoupling.monotone_plan_is_unique_excursion_coupling

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

couplingmeasure-theoryoptimal-transportuniqueness

Let μ⊥ν\mu\perp\nu be mutually singular Borel probability measures on R\mathbb R with finite first moments. Let γ\gamma be a transport plan with marginals μ,ν\mu,\nu that is concentrated on a monotone set SS of non-crossing, non-connecting, consistently oriented arches.

Then γ\gamma is Juillet's excursion coupling in the exact sense of the named formal definition IsJuilletExcursionCoupling. Moreover, it is the unique measure satisfying that definition:

IsEC⁡(μ,ν,γ),IsEC⁡(μ,ν,π)⟹π=γ.\operatorname{IsEC}(\mu,\nu,\gamma), \qquad \operatorname{IsEC}(\mu,\nu,\pi)\Longrightarrow\pi=\gamma.

The named definition says that the measure is exactly the completed-graph occupation measure from Juillet, Theorem 1.1, with the prescribed marginals; it is not merely a support condition. Propositions 3.5 and 3.6 remain separate milestones used to prove this final identification and uniqueness.

Formalization Note Finite first moments are expressed by integrability of the identity function.

Preamble
import Definitions.Def_JuilletExcursionCoupling

open MeasureTheory Set Function
Formal statement
namespace ExcursionCoupling

theorem monotone_plan_is_unique_excursion_coupling
    (mu nu : Measure Real)
    [IsProbabilityMeasure mu] [IsProbabilityMeasure nu]
    (hsing : mu ⟂ₘ nu)
    (hmu1 : Integrable (fun x : Real => x) mu)
    (hnu1 : Integrable (fun x : Real => x) nu)
    (gamma : Measure (Real × Real))
    (hgammaFst : gamma.map Prod.fst = mu)
    (hgammaSnd : gamma.map Prod.snd = nu)
    (S : Set (Real × Real))
    (hS : IsMonotoneArchSet S) (hgammaConc : gamma Sᶜ = 0) :
    IsJuilletExcursionCoupling mu nu gamma ∧
      ∀ pi : Measure (Real × Real),
        IsJuilletExcursionCoupling mu nu pi ->
        pi = gamma := 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), Main Theorem, mutually singular case of implication 3 => 4, pp. 2-3 and 16-19; Theorem 1.1 and Remark 1.2, p. 5; Proposition 3.5, pp. 16-18; Proposition 3.6, pp. 18-19

View graph