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 0df444a (Lean v4.33.1)

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)

View graph