Total occupation-time bound for a gradient flow (source code)

= Total occupation-time bound for a gradient flow
{title2=$T_\varepsilon\leq(\sup f-\inf f)/\varepsilon^2$}

If $f$ is bounded along a downward <gradient flow>, the total time spent where $\|\nabla_g f\|\geq\varepsilon$ is at most $(\sup f-\inf f)/\varepsilon^2$. The <gradient-flow dissipation identity> proves this by integrating the indicator of that region. It bounds all visits together, without requiring the visited region to be connected.