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

Proved

ExcursionCoupling.crossing_measures_marginals

by ykanoria · Aug 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

measure-theoryoptimal-transport

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbf{R}$ and $F_\sigma = F_\mu-F_\nu$ . For every Borel set $A\subseteq\mathbf{R}$ ,

\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 $A$ 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))

Read-back

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

Hypotheses.

$\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$ and $\nu(E^{c})=0$ .

Notation. Write

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

(masses converted to reals, $\infty\mapsto 0$ ), $F_\sigma^-$ for its left-limit function (junk value at points with no left limit), and

\text{completed graph}=\big\{(x,y)\;:\;y\text{ between }F_\sigma^-(x)\text{ and }F_\sigma(x)\text{ inclusive}\big\}.

Conclusion. For every Borel set $A\subseteq\mathbb{R}$ , the conjunction of two equalities in $[0,\infty]$ :

1. the lower Lebesgue integral, over $h\in\mathbb{R}$ with respect to Lebesgue measure, of the cardinality of $\{x\in A : (x,h)$ is an increasing point of the completed graph $\}$ equals $\mu(A)$ :

\int_{\mathbb{R}}\#\big\{x\in A:(x,h)\text{ increasing}\big\}\,dh\;=\;\mu(A);

2. the same integral with decreasing points in place of increasing points equals $\nu(A)$ :

\int_{\mathbb{R}}\#\big\{x\in A:(x,h)\text{ decreasing}\big\}\,dh\;=\;\nu(A).

Here $(x,h)$ is an increasing (resp. decreasing) point when it lies on the completed graph and for some $\varepsilon>0$ every completed-graph point $(x',h')$ with $x'\neq x$ and $|x'-x|<\varepsilon$ satisfies $(h'-h)(x'-x)>0$ (resp. $<0$ ).

Conventions.

Cardinalities are counted in $\mathbb{N}\cup\{\infty\}$ , viewed in $[0,\infty]$ , with value $\infty$ for infinite sets.
No measurability of the $h$ -integrands is hypothesized (the lower integral is defined for arbitrary $[0,\infty]$ -valued functions).

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

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

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