Theorem 1.1 - existence of the excursion coupling

Open

ExcursionCoupling.excursion_coupling_exists

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

couplingmeasure-theoryoptimal-transport

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbf{R}$ . Then there exists a probability measure $\pi$ on $\mathbf{R}\times\mathbf{R}$ with first marginal $\mu$ and second marginal $\nu$ that is concentrated on the set $\Gamma$ of paired routes: the pairs $(x^h_{2k-1},x^h_{2k})$ (for levels $h>0$ ) and $(x^h_{2k},x^h_{2k-1})$ (for $h<0$ ) of consecutive generalized solutions of $F_\sigma = h$ at regular levels, as in eq. (14) of the source.

This is the existence half of the excursion coupling of Theorem 1.1: the geometric pairing of crossings at almost every level assembles into an actual transport plan of $(\mu,\nu)$ . Proposition 3.2 makes the pairing well defined and Proposition 3.3 provides the marginals.

Formalization Note Concentration is stated as $\pi(\Gamma^c)=0$ with $\Gamma$ the pairedRoutes set; the specific level-uniform law constructed in the source is not prescribed, only its defining support and marginal properties, which is the content needed by Proposition 3.5 and the Main Theorem.

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem excursion_coupling_exists (μ ν : Measure ℝ)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hsing : μ ⟂ₘ ν) :
    ∃ π : Measure (ℝ × ℝ), IsProbabilityMeasure π ∧
      π.map Prod.fst = μ ∧ π.map Prod.snd = ν ∧
      π (pairedRoutes (Fsigma μ ν))ᶜ = 0 := 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; Theorem 1.1 (case 1) and Remark 1.2, p. 5; construction in Section 3.1, pp. 12-16, eq. (14)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Hypotheses.

$\mu,\nu$ are Borel probability measures on $\mathbb{R}$ (total mass $1$ each);
they are mutually singular: there is a Borel set $E$ with $\mu(E)=0$ and $\nu(E^{c})=0$ .

Write $F_\sigma(x)=\mu\big((-\infty,x]\big)-\nu\big((-\infty,x]\big)$ (masses converted to reals, $\infty\mapsto 0$ ).

Conclusion. The theorem asserts the existence (plain $\exists$ , no uniqueness) of a Borel measure $\pi$ on $\mathbb{R}\times\mathbb{R}$ such that:

(i) $\pi$ is a probability measure;
(ii) the pushforward of $\pi$ under $(x,y)\mapsto x$ equals $\mu$ ;
(iii) the pushforward under $(x,y)\mapsto y$ equals $\nu$ ;
(iv) $\pi$ assigns measure $0$ to the complement of the set $\Gamma$ of paired routes of $F_\sigma$ :

\pi\big(\Gamma^{c}\big)=0

(the measure is evaluated on this set as an outer measure; no measurability of $\Gamma$ is asserted).

What $\Gamma$ is. $\Gamma$ is the set of pairs $(a,b)$ for which there exists $h\neq 0$ such that:

$h$ is a regular level of $F_\sigma$ — i.e. the generalized level set

L(h)=\big\{x\;:\;h\text{ lies between the left limit }F_\sigma^-(x)\text{ (junk value where no left limit exists) and }F_\sigma(x)\text{ inclusive}\big\}

consists of exactly $2n$ points $x_0<\dots<x_{2n-1}$ for some $n\in\mathbb{N}$ (possibly $0$ ), each an increasing or decreasing point of the completed graph, with $(x_i,h)$ increasing iff ( $h>0\iff i$ even);

$(a,h)$ is an increasing point and $(b,h)$ a decreasing point — increasing/decreasing meaning: on the completed graph and, for some $\varepsilon>0$ , every graph point $(x',h')$ with $x'\neq x$ , $|x'-x|<\varepsilon$ has $(h'-h)(x'-x)>0$ , resp. $<0$ ;
and either
- $h>0$ , $a<b$ , and no point of the open interval $(a,b)$ lies in $L(h)$ ; or
- $h<0$ , $b<a$ , and no point of $(b,a)$ lies in $L(h)$ .

View graph