Proposition 3.2 - almost every level of $F_\sigma$ is regular

Proved

ExcursionCoupling.ae_level_regular

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

optimal-transportreal-analysis

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbf{R}$ and $F_\sigma = F_\mu - F_\nu$ . Then for Lebesgue-almost every level $h\neq 0$ : the set of generalized solutions of $F_\sigma = h$ is finite with an even number $2n$ of elements; each solution is an increasing or a decreasing point of the completed graph; and, enumerated in increasing order $x_1 < \dots < x_{2n}$ , the solutions strictly alternate between increasing and decreasing crossings, with equal numbers $n$ of each, starting with an increasing point when $h > 0$ and with a decreasing point when $h < 0$ .

This is the geometric heart of the excursion coupling: at almost every level the completed graph crosses the horizontal line $\mathbf{R}\times\{h\}$ in a finite alternating pattern, which is what makes the pairing of consecutive crossings in eq. (14) well defined.

Formalization Note The conclusion is packaged as the predicate regularLevel: an enumeration $x : \mathrm{Fin}(2n) \to \mathbf{R}$ , strictly monotone, with range the level set, each $(x_i,h)$ an increasing or decreasing point, and $(x_i,h)$ increasing iff ( $h>0$ iff $i$ is even) for the 0-based index $i$ .

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem ae_level_regular (μ ν : Measure ℝ)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hsing : μ ⟂ₘ ν) :
    ∀ᵐ h : ℝ ∂(volume : Measure ℝ), h ≠ 0 → regularLevel (Fsigma μ ν) h := 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.2, p. 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}$ (each of total mass $1$ );
they are mutually singular: there exists a Borel set $E$ with $\mu(E)=0$ and $\nu(E^{c})=0$ .

Notation. Write

F_\sigma(x)=\mu\big((-\infty,x]\big)-\nu\big((-\infty,x]\big)

(masses converted to reals, $\infty\mapsto 0$ ; here they are $\le 1$ ), $F_\sigma^-$ for its left-limit function (junk value where no left limit exists),

\text{completed graph}=\big\{(x,y)\;:\;y\text{ between }F_\sigma^-(x)\text{ and }F_\sigma(x)\text{ inclusive}\big\},\qquad L(h)=\big\{x:(x,h)\text{ in the completed graph}\big\}.

Conclusion. For Lebesgue-almost every $h\in\mathbb{R}$ , if $h\neq 0$ then $h$ is a regular level of $F_\sigma$ , meaning: there exist $n\in\mathbb{N}$ (possibly $n=0$ ) and strictly increasing reals $x_0<\dots<x_{2n-1}$ such that

(i) $L(h)=\{x_0,\dots,x_{2n-1}\}$ exactly — an even, finite number of generalized solutions, with $n=0$ (empty level set) allowed;
(ii) each $(x_i,h)$ $(x_{i}, h)$ is an increasing or a decreasing point of the completed graph:
- increasing: for some $\varepsilon>0$ every graph point $(x',h')$ with $x'\neq x_i$ , $|x'-x_i|<\varepsilon$ has $(h'-h)(x'-x_i)>0$ ;
- decreasing: the same with $<0$ ;
(iii) $(x_i,h)$ is an increasing point iff

(h>0)\iff(i\text{ even}).

Given $h\neq 0$ this means: for $h>0$ the increasing points are exactly those at even positions $x_0,x_2,\dots$ ; for $h<0$ exactly those at odd positions $x_1,x_3,\dots$ .

Edge cases.

Nothing is asserted about the level $h=0$ (the implication is vacuous there).
The statement holds only up to a Lebesgue-null exceptional set of levels.

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

Proposition 3.2 - almost every level of FσF_\sigmaFσ​ is regular

Proposition 3.2 - almost every level of $F_\sigma$ is regular