Eqs. (6)-(7) - generalized Banach indicatrix identities for $F_\sigma$

Proved

ExcursionCoupling.total_variation_eq_integral_indicatrix

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

bounded-variationoptimal-transportreal-analysis

Let $\mu,\nu$ be finite Borel measures on $\mathbf{R}$ and $F_\sigma = F_\mu - F_\nu$ . For all $s\le t$ ,

TV_s^t(F_\sigma) \;=\; \int_{\mathbf{R}} i^*_{]s,t]}(h)\,dh \;=\; \int_{\mathbf{R}} \bigl(i^{*,+}_{]s,t]}(h) + i^{*,-}_{]s,t]}(h)\bigr)\,dh,

where $i^*_{]s,t]}(h)$ is the number of generalized solutions $x\in\,]s,t]$ of $F_\sigma = h$ (points with $(x,h)$ in the completed graph), and $i^{*,\pm}_{]s,t]}(h)$ count the increasing, resp. decreasing, points among them. This is the generalized Banach indicatrix identity: the vertical segments of the completed graph absorb the saltus part of the variation, so no jump correction is needed.

It is the quantitative backbone of the excursion coupling: it shows the level-counting functions are finite for almost every $h$ and integrate to the variation of $F_\sigma$ .

Formalization Note The total variation is Mathlib's eVariationOn over Icc s t (values in $[0,\infty]$ ), the level counts are Set.encard coerced into $[0,\infty]$ , and both sides may be infinite a priori, so the identity is stated in the extended nonnegative reals.

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem total_variation_eq_integral_indicatrix
    (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s t : ℝ) (_hst : s ≤ t) :
    eVariationOn (Fsigma μ ν) (Icc s t)
        = ∫⁻ h : ℝ, ((Ioc s t ∩ levelSet (Fsigma μ ν) h).encard.toENNReal) ∧
    eVariationOn (Fsigma μ ν) (Icc s t)
        = ∫⁻ h : ℝ,
            (({x ∈ Ioc s t | (x, h) ∈ posPoints (Fsigma μ ν)}.encard.toENNReal)
              + ({x ∈ Ioc s t | (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), https://arxiv.org/abs/1907.00681; eqs. (5)-(7), pp. 13-14; after J. Bertoin and M. Yor, Local times for functions with finite variation: two versions of the Stieltjes change-of-variables formula, Bull. Lond. Math. Soc. 46 (2014), Theorem 1

View graph

Eqs. (6)-(7) - generalized Banach indicatrix identities for FσF_\sigmaFσ​

Eqs. (6)-(7) - generalized Banach indicatrix identities for $F_\sigma$