The total crossing mass is $2$ : $\int_{\mathbb R}i^*(h)\,dh=2$

Proved

ExcursionCoupling.lintegral_crossingMultiplicity_eq_two

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

measure-theoryoptimal-transport

Let $\mu\perp\nu$ be mutually singular Borel probability measures on $\mathbb R$ and $F_\sigma=F_\mu-F_\nu$ . Then

\int_{\mathbb R}\Big(i^{*,+}(h)+i^{*,-}(h)\Big)\,dh=2,

where $i^{*,+}(h)$ and $i^{*,-}(h)$ count the increasing and the decreasing points of the completed graph $\mathrm{Graph}^*F_\sigma$ at height $h$ .

This is the normalisation that makes Juillet's sampling law $\theta/2$ a probability law: the integrand is the total crossing multiplicity of the level $h$ , its integral is the total variation of $F_\sigma$ over the whole line, and mutual singularity identifies that total variation with

\mathrm{TV}(F_\mu)+\mathrm{TV}(F_\nu)=\mu(\mathbb R)+\nu(\mathbb R)=1+1=2.

Preamble

import Definitions.Def_JuilletExcursionCoupling

open MeasureTheory Set Function Filter Topology

Formal statement

namespace ExcursionCoupling

theorem lintegral_crossingMultiplicity_eq_two
    (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hsing : μ ⟂ₘ ν) :
    ∫⁻ h : ℝ, crossingMultiplicity (Fsigma μ ν) h = 2 := 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), Section 3.1, proof of Theorem 1.1 (p. 15): "We proved that i_R is almost surely an even integer and int i_R(h) dh = TV(F_sigma) = TV(F_mu) + TV(F_nu) = 2".

View graph

The total crossing mass is 222: ∫Ri∗(h) dh=2\int_{\mathbb R}i^*(h)\,dh=2∫R​i∗(h)dh=2

The total crossing mass is $2$ : $\int_{\mathbb R}i^*(h)\,dh=2$