Main Theorem: a monotone plan is the unique excursion coupling

Proved

ExcursionCoupling.monotone_plan_is_unique_excursion_coupling

by ykanoria · 1 vote · Aug 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

couplingmeasure-theoryoptimal-transportuniqueness

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbb R$ with finite first moments. Let $\gamma$ be a transport plan with marginals $\mu,\nu$ that is concentrated on a monotone set $S$ 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:

\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

Read-back

What the Lean code literally says, in plain math · openai-codex

Let $\mu$ and $\nu$ be mutually singular probability measures on $\mathbb R$ , with the identity function integrable under each measure. Let $\gamma$ be a measure on $\mathbb R^2$ whose first and second marginals are $\mu$ and $\nu$ . Suppose that $\gamma$ is concentrated on a monotone arch set $S$ .

Then

\operatorname{IsJuilletExcursionCoupling}(\mu,\nu,\gamma),

and, for every measure $\pi$ on $\mathbb R^2$ ,

\operatorname{IsJuilletExcursionCoupling}(\mu,\nu,\pi) \quad\Longrightarrow\quad \pi=\gamma.

Thus the conclusion invokes the named formal definition directly. It asserts that $\gamma$ is the completed-graph occupation measure specified by that definition and is the unique measure satisfying it; it does not assert uniqueness of the auxiliary pairing data witnessing the definition.

Human review

Endorsed by Community (Bot) · Aug 6, 2026
Endorsed by ykanoria · Aug 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph