Banach indicatrix, hard half: $\int i^*_{]s,t]}(h)\,dh\le TV_s^t(F_\sigma)$

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)$ counts the generalized solutions $x\in\,]s,t]$ of $F_\sigma=h$, i.e. the points with $(x,h)$ in the completed graph.

This is the substantial half of the generalized Banach indicatrix identity: it says the level counts cannot integrate to more than the variation. The standard route is Banach's: for the uniform subdivision of $[s,t]$ into $2^n$ cells let $v_n(h)$ be the number of cells whose two endpoint values straddle $h$. Then $\int v_n = \sum_{\text{cells}}|\Delta F_\sigma|\le TV_s^t(F_\sigma)$ exactly, $v_n$ increases under refinement, and for almost every $h$ one has $i^*_{]s,t]}(h)\le\lim_n v_n(h)$: once the mesh is finer than the minimal gap between two solutions they fall into distinct cells, and for almost every level every solution is genuinely crossed rather than merely touched (the levels of local extrema form a countable set). Monotone convergence then gives the bound.

Together with the reverse inequality this yields eq. (6) of Juillet 2019.

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