Prove2Me

The crossing counting set functions ζ±\zeta_\pm are Borel measures

Proved
ExcursionCoupling.crossing_counting_functions_are_measures

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

measure-theoryoptimal-transport

Let μ,ν\mu,\nu be finite Borel measures on R\mathbb R and let Fσ=Fμ−FνF_\sigma=F_\mu-F_\nu be the difference of their cumulative distribution functions. For a level h∈Rh\in\mathbb R let

Graph∗,+FσandGraph∗,−Fσ\mathrm{Graph}^{*,+}F_\sigma\quad\text{and}\quad\mathrm{Graph}^{*,-}F_\sigma

be the sets of increasing, respectively decreasing, points of the completed graph of FσF_\sigma. Juillet's crossing measures are obtained by integrating, over all levels, the counting measure of the crossings at that level:

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

The assertion is that these two set functions really are Borel measures on R\mathbb R: there exist measures ζ+,ζ−\zeta_+,\zeta_- whose value on every Borel set AA is given by the displayed integrals.

For each fixed level hh the set function A↦#(A∩{x:(x,h)∈Graph∗,±Fσ})A\mapsto\#(A\cap\{x:(x,h)\in\mathrm{Graph}^{*,\pm}F_\sigma\}) is a counting measure, hence countably additive; the content of the statement is therefore the measurability in hh of the crossing counts, which lets one exchange the integral with a countable sum by monotone convergence.

Formalization note. The existential packaging is deliberate: it says exactly that the lower Lebesgue integrals below define genuine measures, without committing to a particular construction of them.

Preamble
import Definitions.Def_excursion_coupling

open MeasureTheory Set Function
Formal statement
namespace ExcursionCoupling

theorem crossing_counting_functions_are_measures
    (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    ∃ ζpos ζneg : Measure ℝ,
      (∀ A : Set ℝ, MeasurableSet A →
          ζpos A = ∫⁻ h : ℝ, ({x ∈ A | (x, h) ∈ posPoints (Fsigma μ ν)}.encard.toENNReal)) ∧
      (∀ A : Set ℝ, MeasurableSet A →
          ζneg A = ∫⁻ h : ℝ, ({x ∈ A | (x, h) ∈ negPoints (Fsigma μ ν)}.encard.toENNReal)) := 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, the measures zeta_+ and zeta_- introduced before Proposition 3.3 (p. 12); counting measures of the increasing/decreasing points of Graph^* F_sigma integrated over levels.

View graph