Binomial partial sums bounded via the binary entropy function

Let $n,k$ be natural numbers with $0 < n$ and $2k \le n$, and let $\lambda = k/n \in [0,1/2]$. Then the volume of the Hamming ball of radius $k$ in $\{0,1\}^n$ is bounded via the binary entropy function $H(\lambda) = -\lambda\ln\lambda - (1-\lambda)\ln(1-\lambda)$ (Real.binEntropy, measured in nats) by

This is the classical volume bound on Hamming balls (equivalently, on partial sums of binomial coefficients) used throughout coding theory and combinatorics: it converts a bound on the size of a subset of the hypercube contained in (or compared against) a Hamming ball into an entropy bound, and conversely. The proof is elementary: for $j \le k$ and $\lambda \le 1/2$, the term $\lambda^j (1-\lambda)^{n-j}$ of the binomial expansion of $1 = (\lambda + (1-\lambda))^n$ is at least $\lambda^k (1-\lambda)^{n-k}$, so $\left(\sum_{i=0}^k \binom{n}{i}\right) \lambda^k(1-\lambda)^{n-k} \le \sum_{j=0}^k \binom{n}{j}\lambda^j(1-\lambda)^{n-j} \le 1$, and rearranging with $\lambda = k/n$ gives the stated bound after converting $\lambda^{-k}(1-\lambda)^{-(n-k)}$ into exponential-of-entropy form.

Formalization Note. Entropy is measured in nats (Real.binEntropy uses natural log, as in Mathlib's Analysis.SpecialFunctions.BinaryEntropy), so the bound reads $e^{nH(\lambda)}$ rather than $2^{nH_2(\lambda)}$; the two forms are equivalent up to the base of the logarithm. This connects Mathlib's Real.binEntropy to Nat.choose for the first time, and is the tool needed to bound the size of a 'bad' bin-pattern set by a volume-of-Hamming-ball argument in entropy-compression proofs such as Spencer's partial-colouring method and Kleitman's diameter theorem.