Prove2Me

Supremum argument: the open column ]a,b[×{b}]a,b[\times\{b\} has marginal-determined mass

Open
ExcursionCoupling.coupling_eq_on_open_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 open column 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 the supremum step in the proof of Proposition 3.6 of Juillet (2019). The generalized intermediate value theorem shows Fσ(a′)>hF_\sigma(a')>h for every a′∈ ]a,b[a'\in\,]a,b[, so equation (17) holds with any such a′a' in place of aa for which (a′,b)∈Γ(a',b)\in\Gamma. Taking the supremum,

π(]a,b[ ×{b})=sup⁡{π([a′,b[ ×{b}):(a′,b)∈Γ, a<a′<b},\pi\bigl(]a,b[\,\times\{b\}\bigr)=\sup\bigl\{\pi\bigl([a',b[\,\times\{b\}\bigr) : (a',b)\in\Gamma,\ a<a'<b\bigr\},

and every term on the right is determined by the marginals, hence so is the left side.

Formalization Note The open interval with endpoints a,ba,b in either order is written Ioo (min a b) (max a b), covering both the h>0h>0 case (a<ba<b) and the h<0h<0 case (b<ab<a).

Preamble
import Definitions.Def_excursion_coupling

open MeasureTheory Set Function Filter Topology
Formal statement
theorem ExcursionCoupling.coupling_eq_on_open_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 μ ν)) :
    π ((Ioo (min a b) (max a b)) ×ˢ ({b} : Set ℝ))
      = π' ((Ioo (min a b) (max a 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), the supremum argument pi(]a,b[ x {b}) = sup {pi([a',b[ x {b}) : (a',b) in Gamma, a < a' < b}.

View graph