Banach indicatrix via crossings: $TV_s^t(F_\sigma)\le\int (i^{*,+}+i^{*,-})(h)\,dh$

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

where $i^{*,+}_{]s,t]}(h)$ and $i^{*,-}_{]s,t]}(h)$ count the increasing, resp. decreasing, points $(x,h)$ of the completed graph of $F_\sigma$ with $x\in\,]s,t]$.

This refines the elementary bound $TV_s^t(F_\sigma)\le\int i^*_{]s,t]}$, in which the generalized intermediate value theorem only produces some generalized solution in each straddled cell. Here the solution produced must be an actual crossing, which is exactly the extra content: for almost every level $h$ every generalized solution of $F_\sigma=h$ is either an increasing or a decreasing point, because the levels at which a solution is merely touched are the values of local extrema and hence form a countable set.

Combined with the reverse inequality (which follows from $i^{*,+}+i^{*,-}\le i^*$ pointwise and eq. (6)) this gives eq. (7) of Juillet 2019.

Formalization note. Both sides may be $+\infty$ a priori; the statement is in the extended nonnegative reals, with counts given by Set.encard coerced into $[0,\infty]$.