The Exercise

A random variable $X$ takes its values among the $2^{2n}$ strings of $2n$ bits, with $n \ge 1$. It equals one particular string $x_0$ with probability $1 - 2^{-s}$, for a real $s > 0$, and each of the other $2^{2n} - 1$ strings with one and the same probability, so that together they carry the remaining $2^{-s}$. This is the spike distribution: a spike at $x_0$, sharper the larger $s$ is. The exercise asks for an upper bound on the Shannon entropy of $X$ in terms of $n$ and $s$.

The Entropy of the Spike

The entropy $H_{n,s}$ of the spike distribution on strings of $2n$ bits is its Shannon entropy in bits, the real number $$H_{n,s} = -\left(1 - 2^{-s}\right) \log_2\!\left(1 - 2^{-s}\right) - 2^{-s} \log_2 \frac{2^{-s}}{2^{2n} - 1}.$$(1)^✦

The Claim

What Is Checked

The claim is stated over one quantity, the entropy $H_{n,s}$ of the spike distribution given by (1). What the library proves about $H_{n,s}$ is the bound (2).