Entropy bound for a Hamming ball (source code)

= Entropy bound for a Hamming ball
{title2=$\sum_{j\leq\rho n}\binom nj\leq e^{nh(\rho)}$}

For $0<\rho\leq1/2$, the number of binary words within <Hamming distance> $\rho n$ of a fixed word is at most $e^{nh(\rho)}$, with the <binary entropy function> in natural logarithms. In $1=\sum_j\binom nj\rho^j(1-\rho)^{n-j}$, each summand weight for $j\leq\rho n$ is at least $\rho^{\rho n}(1-\rho)^{n(1-\rho)}=e^{-nh(\rho)}$. Also $h''(\rho)=-1/(\rho(1-\rho))\leq-4$, so $\log2-h(1/2-a)\geq2a^2$. These two bounds give the approximate-recovery denominator in the <list-decoding Fano inequality>.