Simple non-asymptotic upper-bound for packing number of a hamming cube

Question

Looking for a simple upper-bound for the packing number of hamming cube, I'm led to consider the following. Fix $p \in (0,1/2]$. For a positive integer $n$, define $S_n(p) := \sum_{i=1}^{\lfloor np\rfloor}{n\choose i}$, and $M_n(p) := 1-\dfrac{1}{n}\log_2S_n(p)$. Note that $B_n(p):=2^n/S_n(p)$ is a well-known $np$-packing number of $\{0,1\}^n$. For example, see https://mathoverflow.net/a/283202/78539.

I've empirically observed that

Empirical observation. $M_n(p) \le 1-H_2(p)$ for every $n$, where $H_2:[0,1] \to [0,1]$ is the binary entropy function. See figure below.

Question. Is there a simple proof for the above observation ?

Answer 1

Based on comments and references from user Ofir Gorodetsky, we can prove the following

Proposition. $M_n(p) \le 1-H_2(p)$ for every positive integer $n$ and every $p \in (0,1/2)$.

Proof. As $p \in (0,1/2)$, we from Theorem 3.1 of this tutorial that

$$ S_n(p):= \sum_{1 \le i \le np}{n \choose i} \le 2^{nH_2(p)}. $$

Thus, $M_n(p) := 1-(1/n)\log_2 S_n(p) \le 1-H_2(p)$, which concludes the proof.