Theorem 1.1 - existence of the excursion coupling

Proved

ExcursionCoupling.excursion_coupling_exists

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

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)

View graph