Prove2Me

Eq. (17): the half-open column [a,b[×{b}[a,b[\times\{b\} has marginal-determined mass

Open
ExcursionCoupling.coupling_eq_on_halfopen_column

by ew2493 · Aug 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Let μ⊥ν\mu\perp\nu be mutually singular Borel probability measures on R\mathbf{R}, let Γ\Gamma be the paired-route set of equation (14), and let π,π′\pi,\pi' be transport plans with marginals μ,ν\mu,\nu both concentrated on Γ\Gamma. Fix a paired route (a,b)∈Γ(a,b)\in\Gamma.

Then the mass carried on the half-open column toward the arrival point bb agrees for the two plans:

π([a,b[ ×{b})=π′([a,b[ ×{b}).\pi\bigl([a,b[\,\times\{b\}\bigr)=\pi'\bigl([a,b[\,\times\{b\}\bigr).

This is equation (17) of Juillet (2019). Assuming a<ba<b with Fσ(a−)≥Fσ(b)F_\sigma(a^-)\ge F_\sigma(b), the definition of Γ\Gamma forces the mass of μ\mu on [a,b[[a,b[ to be transported into ]a,b]]a,b], whence for either coupling

π([a,b[ ×{b})=μ([a,b[)−ν(]a,b[),\pi\bigl([a,b[\,\times\{b\}\bigr)=\mu([a,b[)-\nu(]a,b[),

an expression depending only on the marginals. The two plans therefore assign it the same value.

Formalization Note The half-open interval with endpoints a,ba,b in either order, excluding bb, is written uIcc a b \ {b}; this is [a,b[[a,b[ when a<ba<b and ]b,a]]b,a] when b<ab<a, matching the orientation convention of Γ\Gamma at negative levels.

Preamble
import Definitions.Def_excursion_coupling

open MeasureTheory Set Function Filter Topology
Formal statement
theorem ExcursionCoupling.coupling_eq_on_halfopen_column
    (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hsing : μ ⟂ₘ ν)
    (π π' : Measure (ℝ × ℝ))
    (hπFst : π.map Prod.fst = μ) (hπSnd : π.map Prod.snd = ν)
    (hπConc : π (pairedRoutes (Fsigma μ ν))ᶜ = 0)
    (hπ'Fst : π'.map Prod.fst = μ) (hπ'Snd : π'.map Prod.snd = ν)
    (hπ'Conc : π' (pairedRoutes (Fsigma μ ν))ᶜ = 0)
    (a b : ℝ) (hab : (a, b) ∈ pairedRoutes (Fsigma μ ν)) :
    π ((uIcc a b \ {b}) ×ˢ ({b} : Set ℝ))
      = π' ((uIcc a b \ {b}) ×ˢ ({b} : Set ℝ)) := by sorry
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), Section 3.2, proof of Proposition 3.6 (pp. 18-19), equation (17).

View graph