Prove2Me

Proposition 3.3 - crossing counting measures have marginals μ\mu and ν\nu

Proved
ExcursionCoupling.crossing_measures_marginals

by ykanoria · Aug 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

measure-theoryoptimal-transport

Let μ⊥ν\mu\perp\nu be mutually singular Borel probability measures on R\mathbf{R} and Fσ=Fμ−FνF_\sigma = F_\mu-F_\nu. For every Borel set A⊆RA\subseteq\mathbf{R},

∫R#{x∈A:(x,h)∈Graph∗,+(Fσ)} dh=μ(A),∫R#{x∈A:(x,h)∈Graph∗,−(Fσ)} dh=ν(A).\int_{\mathbf{R}} \#\{x\in A : (x,h)\in\mathrm{Graph}^{*,+}(F_\sigma)\}\,dh = \mu(A), \qquad \int_{\mathbf{R}} \#\{x\in A : (x,h)\in\mathrm{Graph}^{*,-}(F_\sigma)\}\,dh = \nu(A).

In words: the first marginal of the counting measure ζ+\zeta_+ over increasing points of the completed graph is exactly μ\mu, and the first marginal of ζ−\zeta_- over decreasing points is exactly ν\nu. This is why the excursion coupling, which transports each increasing point to a paired decreasing point at the same level, has the correct marginals.

Formalization Note The identity is stated for every Borel AA with the level integral as a Lebesgue lower integral of the (possibly infinite) cardinality Set.encard, which is exactly the statement that the pushforward of ζ±\zeta_\pm under the first projection is μ\mu resp. ν\nu.

Preamble
import Definitions.Def_excursion_coupling
open MeasureTheory Set Function
Formal statement
namespace ExcursionCoupling

theorem crossing_measures_marginals (μ ν : Measure ℝ)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hsing : μ ⟂ₘ ν) :
    ∀ A : Set ℝ, MeasurableSet A →
      (∫⁻ h : ℝ, ({x ∈ A | (x, h) ∈ posPoints (Fsigma μ ν)}.encard.toENNReal)) = μ A ∧
      (∫⁻ h : ℝ, ({x ∈ A | (x, h) ∈ negPoints (Fsigma μ ν)}.encard.toENNReal)) = ν A := 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.3, p. 14 (proof pp. 14-15, eqs. (9)-(13))

View graph