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

Proved

ExcursionCoupling.total_variation_eq_integral_indicatrix

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

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

Read-back

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

Setting. Let $\mu,\nu$ be Borel measures on $\mathbb{R}$ , each assumed to be a finite measure (finite total mass), and let $s,t\in\mathbb{R}$ with the hypothesis $s\le t$ .

Throughout, write

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

each mass converted to a real number by the total map sending $\infty\mapsto 0$ (under the finiteness assumptions the masses are finite). Write $F_\sigma^-(x)$ for the left limit of $F_\sigma$ at $x$ (an arbitrary junk value at any point where the left limit does not exist), and call completed graph the set of $(x,y)$ with $y$ between $F_\sigma^-(x)$ and $F_\sigma(x)$ inclusive.

Conclusion. The theorem asserts the conjunction of two equalities in $[0,\infty]$ , both with the same left-hand side: the extended total variation of $F_\sigma$ on the closed interval $[s,t]$ , i.e. the supremum in $[0,\infty]$ , over all finite nondecreasing sequences $u_0\le u_1\le\dots\le u_n$ of points of $[s,t]$ , of

\mathrm{TV}\;=\;\sup\;\sum_{i<n}\big|F_\sigma(u_{i+1})-F_\sigma(u_i)\big|.

1. It equals the lower Lebesgue integral, over levels $h\in\mathbb{R}$ with respect to Lebesgue measure, of the cardinality of the set of $x$ in the half-open interval $(s,t]$ such that $h$ lies between $F_\sigma^-(x)$ and $F_\sigma(x)$ inclusive:

\mathrm{TV}\;=\;\int_{\mathbb{R}}\#\Big\{x\in(s,t]\;:\;h\text{ lies between }F_\sigma^-(x)\text{ and }F_\sigma(x)\text{ inclusive}\Big\}\;dh.

2. The same extended total variation equals the lower Lebesgue integral over $h\in\mathbb{R}$ of the sum of two such cardinalities:

\mathrm{TV}\;=\;\int_{\mathbb{R}}\Big(\#\big\{x\in(s,t]:(x,h)\text{ increasing}\big\}\;+\;\#\big\{x\in(s,t]:(x,h)\text{ decreasing}\big\}\Big)\;dh,

where

$(x,h)$ is an increasing point of the completed graph when $(x,h)$ is on the completed graph and there is $\varepsilon>0$ such that every completed-graph point $(x',h')$ with $x'\neq x$ , $|x'-x|<\varepsilon$ satisfies $(h'-h)(x'-x)>0$ ;
$(x,h)$ is a decreasing point in the same sense with $(h'-h)(x'-x)<0$ .

Conventions and edge cases.

Each cardinality is counted in $\mathbb{N}\cup\{\infty\}$ and viewed in $[0,\infty]$ , taking the value $\infty$ for an infinite set.
No measurability of the level-counting integrands is hypothesized (the lower integral is defined for arbitrary $[0,\infty]$ -valued functions).
The degenerate case $s=t$ is included ( $[s,t]=\{s\}$ , $(s,t]=\varnothing$ ).

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

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

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