Proposition 3.5 - monotone plans are concentrated on the paired routes

Proved

ExcursionCoupling.monotone_plan_concentrated_on_paired_routes

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}$ with finite first moments, and let $\gamma$ be a transport plan with marginals $\mu$ and $\nu$ concentrated on a monotone set $S$ of arches - non-crossing, non-connecting, and consistently oriented in the sense of Definition 0.3. Then $\Gamma\cap S$ is still a monotone set and $\gamma$ is concentrated on $\Gamma\cap S$ , where $\Gamma$ is the set of paired routes of eq. (14).

This is the uniqueness-side characterization of the excursion coupling: any monotone transport plan must already use only the routes that pair consecutive crossings of the level sets of $F_\sigma$ . In the Main Theorem of the paper this is the key step of the implication from monotonicity to the excursion coupling, identifying the limit of the $L^p$ -optimal plans for the strictly concave costs $|x-y|^p$ , $p\to 1^-$ .

Formalization Note Concentration on a set $T$ is stated as $\gamma(T^c)=0$ ; finite first moments as integrability of the identity function.

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem monotone_plan_concentrated_on_paired_routes
    (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hsing : μ ⟂ₘ ν)
    (hμ1 : Integrable (fun x : ℝ => x) μ) (hν1 : Integrable (fun x : ℝ => x) ν)
    (γ : Measure (ℝ × ℝ)) (hγfst : γ.map Prod.fst = μ) (hγsnd : γ.map Prod.snd = ν)
    (S : Set (ℝ × ℝ)) (hS : IsMonotoneArchSet S) (hconc : γ Sᶜ = 0) :
    IsMonotoneArchSet (pairedRoutes (Fsigma μ ν) ∩ S) ∧
      γ (pairedRoutes (Fsigma μ ν) ∩ S)ᶜ = 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; Proposition 3.5, p. 16 (proof pp. 16-19)

Read-back

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

Hypotheses, all explicit.

$\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$ , $\nu(E^{c})=0$ ;
the identity function $x\mapsto x$ is Bochner-integrable with respect to $\mu$ and with respect to $\nu$ (i.e. each has finite first absolute moment);
$\gamma$ is a Borel measure on $\mathbb{R}\times\mathbb{R}$ — not explicitly assumed finite or a probability measure — whose pushforward under $(x,y)\mapsto x$ equals $\mu$ and under $(x,y)\mapsto y$ equals $\nu$ ;
$S\subseteq\mathbb{R}^2$ $S \subseteq R^{2}$ is an arbitrary set (no measurability assumed) that is a monotone arch set, i.e. satisfies all three of:
- non-crossing: for all $p,q\in S$ , the closed intervals $I_p,I_q$ between the two coordinates of $p$ , resp. $q$ , taken in either order, are disjoint, or meet in exactly one point, or one contains the other;
- non-connecting: for all $p,q\in S$ with $\min(|p_2-p_1|,|q_2-q_1|)>0$ , one has $p_2\neq q_1$ ;
- same orientation: for all $p,q\in S$ , if $I_q$ is contained in the open interval strictly between $\min(p_1,p_2)$ and $\max(p_1,p_2)$ then $(p_2-p_1)(q_2-q_1)\ge 0$ ;
$\gamma(S^{c})=0$ (outer-measure evaluation).

Notation. Write $\Gamma$ for the set of paired routes of $F_\sigma$ , where

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

(masses converted to reals, $\infty\mapsto 0$ ). That is, $\Gamma$ is the set of pairs $(a,b)$ admitting a level $h\neq 0$ that is a regular level of $F_\sigma$ (its generalized level set, using left limits with junk values where none exist, is exactly $2n$ strictly increasing points, each an increasing or decreasing crossing point, increasing precisely when $h>0\iff$ the index is even), with $(a,h)$ an increasing point, $(b,h)$ a decreasing point, and either

$h>0$ , $a<b$ with no generalized solution in the open interval $(a,b)$ ; or
$h<0$ , $b<a$ with no generalized solution in $(b,a)$ .

Conclusion. The conjunction:

(i) the intersection $\Gamma\cap S$ is itself a monotone arch set (satisfies the same three conditions above); and
(ii) $\gamma$ gives full mass to it:

\gamma\big((\Gamma\cap S)^{c}\big)=0

(again outer-measure evaluation; no measurability of $\Gamma\cap S$ is asserted).

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