The generalized Banach indicatrices $i^{*,\pm}_A$ are measurable in the level

Proved

ExcursionCoupling.crossing_count_measurable

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

measure-theoryoptimal-transport

Let $\mu,\nu$ be finite Borel measures on $\mathbb R$ , let $F_\sigma=F_\mu-F_\nu$ , and let $A\subseteq\mathbb R$ be Borel. The generalized Banach indicatrices of $F_\sigma$ relative to $A$ are the level-counting functions

h\longmapsto i^{*,+}_A(h)=\#\{x\in A:(x,h)\in\mathrm{Graph}^{*,+}F_\sigma\}, \qquad h\longmapsto i^{*,-}_A(h)=\#\{x\in A:(x,h)\in\mathrm{Graph}^{*,-}F_\sigma\},

counting respectively the increasing and the decreasing points of the completed graph of $F_\sigma$ that lie above $A$ at height $h$ . The assertion is that both are Borel measurable functions of the level $h$ , as maps into $[0,\infty]$ .

Measurability of the indicatrix is the standing hypothesis that makes every statement of the form "integrate the crossing count over all levels" meaningful, and it is what allows the integral of a sum of crossing counts to be split as a sum of integrals. It is the measurability half of the classical Banach indicatrix theorem, here in the generalized (completed-graph, possibly discontinuous) setting of Bertoin-Yor.

Formalization note. Cardinalities are taken as Set.encard in ℕ∞ and coerced to ℝ≥0∞, so no finiteness of the level sets is presupposed; levels with infinitely many crossings simply give the value $+\infty$ .

Preamble

import Definitions.Def_excursion_coupling

open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem crossing_count_measurable
    (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (A : Set ℝ) (hA : MeasurableSet A) :
    Measurable (fun h : ℝ => ({x ∈ A | (x, h) ∈ posPoints (Fsigma μ ν)}.encard.toENNReal)) ∧
      Measurable (fun 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, equations (6)-(8) and Proposition 3.3 (p. 12); measurability of the generalized Banach indicatrix, after J. Bertoin and M. Yor (2014), Theorem 1.

View graph

The generalized Banach indicatrices iA∗,±i^{*,\pm}_AiA∗,±​ are measurable in the level

The generalized Banach indicatrices $i^{*,\pm}_A$ are measurable in the level