Rothvoß's Lemma 9: low entropy of the quantized row-sum shell

This is Rothvoß's Lemma 9 from his exposition of Spencer's entropy method for discrepancy theory: quantizing the row sum of a random coloring into shells costs very little Shannon entropy once the shell width is a large multiple of $\sqrt m$.

Fix $m\ge1$, a row $a:\mathrm{Fin}\,m\to\{0,1\}$, and $\lambda\ge2$. Write $\Delta=\lambda\sqrt m$ and let $\mathrm{shellFin}(\Delta,a)$ send a Boolean coloring $\omega:\mathrm{Fin}\,m\to\{\mathrm{true},\mathrm{false}\}$ to the (shifted, finite-alphabet) index of the width-$2\Delta$ shell containing its row sum $\sum_j a_j\,\mathrm{RSign}(\omega,j)$. Then, treating $\omega$ as uniformly random, the Shannon entropy $H$ (base 2) of this shell-index random variable satisfies

Intuitively, for $\lambda\gg1$ the row sum concentrates in the central shell with overwhelming probability, so the shell index carries almost no information; this is the quantitative form of that statement, and it is the key per-row estimate combined across many rows (via subadditivity of entropy) to prove Spencer's discrepancy theorem.

Formalization Note. $\mathrm{shellFin}$, $\mathrm{shellIdx}$, $\mathrm{rowSumB}$ and $\mathrm{RSign}$ are the platform definitions of the same names; $H$ is the $\mathrm{shannonEntropy}$ of Definitions.Def_DiscreteEntropy, computed with respect to the uniform measure on colorings implicit in that definition.