Eq. (8) - signed indicatrix identity for increments of $F_\sigma$

Proved

ExcursionCoupling.cdf_difference_eq_signed_indicatrix_integral

by ykanoria · 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$ ,

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

where $i^{*,\pm}_{]s,t]}(h)$ count the increasing and decreasing points $(x,h)$ of the completed graph of $F_\sigma$ with $x\in\,]s,t]$ . Together with eqs. (6)-(7) this identifies the positive and negative variations of $F_\sigma$ as the level integrals of $i^{*,+}$ and $i^{*,-}$ , which is how the marginals $\mu$ and $\nu$ are recovered from crossing counts in Proposition 3.3.

Formalization Note The two lower integrals are extended-real valued and finite (each is bounded by the total variation); the statement takes their real values via ENNReal.toReal.

Preamble

import Definitions.Def_excursion_coupling
open MeasureTheory Set Function

Formal statement

namespace ExcursionCoupling

theorem cdf_difference_eq_signed_indicatrix_integral
    (μ ν : Measure ℝ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s t : ℝ) (_hst : s ≤ t) :
    Fsigma μ ν t - Fsigma μ ν s
      = (∫⁻ h : ℝ, ({x ∈ Ioc s t | (x, h) ∈ posPoints (Fsigma μ ν)}.encard.toENNReal)).toReal
        - (∫⁻ h : ℝ,
            ({x ∈ Ioc s t | (x, h) ∈ negPoints (Fsigma μ ν)}.encard.toENNReal)).toReal := 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; eq. (8), p. 14

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 finite (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)

(masses converted to reals by the total map sending $\infty\mapsto 0$ ), $F_\sigma^-$ for its left-limit function (junk value where no left limit exists), and completed graph for the set of $(x,y)$ with $y$ between $F_\sigma^-(x)$ and $F_\sigma(x)$ inclusive.

Conclusion. The theorem asserts the real-number identity

F_\sigma(t)-F_\sigma(s) \;=\; A - B,

where:

$A$ is the real number obtained from the lower Lebesgue integral (over $h\in\mathbb{R}$ , Lebesgue measure)

\int_{\mathbb{R}}\#\big\{x\in(s,t] \;:\; (x,h)\text{ is an \textit{increasing} point of the completed graph}\big\}\;dh,

the cardinality counted in $\mathbb{N}\cup\{\infty\}$ , viewed in $[0,\infty]$ , over the half-open interval $(s,t]$ ; here $(x,h)$ is increasing when it is on the graph and, for some $\varepsilon>0$ , every graph point $(x',h')$ with $x'\neq x$ , $|x'-x|<\varepsilon$ has $(h'-h)(x'-x)>0$ ;

$B$ is the analogous quantity for decreasing points, i.e. with $(h'-h)(x'-x)<0$ .

Conventions and edge cases.

Each of $A,B$ is produced by the total conversion $[0,\infty]\to\mathbb{R}$ that sends $\infty$ to the junk value $0$ : if either integral is infinite, the corresponding term of the right-hand side is $0$ .
No measurability of the integrands is hypothesized, and no claim is made that the integrals are finite.

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

Eq. (8) - signed indicatrix identity for increments of FσF_\sigmaFσ​

Eq. (8) - signed indicatrix identity for increments of $F_\sigma$