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

Proved

ExcursionCoupling.cdf_difference_eq_signed_indicatrix_integral

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$ ,

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

View graph

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

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