Lemma 2.7: Binomial coefficient upper bound

From Rigollet, Chapter 2, Lemma 2.7: For any integers 1 ≤ k ≤ n, C(n, k) ≤ (e · n / k)^k.

Proof strategy

Rather than the book's induction proof, we use two clean Mathlib bounds:

1. Nat.choose_le_pow_div: C(n,k) ≤ n^k / k!
2. Real.pow_div_factorial_le_exp: k^k / k! ≤ exp(k)

Combining: C(n,k) ≤ n^k / k! = (n/k)^k · (k^k/k!) ≤ (n/k)^k · e^k = (en/k)^k.

theorem lemma_2_7_binom_bound (n k : ℕ) (hk : 1 ≤ k) (_hkn : k ≤ n) : ↑(n.choose k) ≤ (Real.exp 1 * ↑n / ↑k) ^ k

Lemma 2.7 (Rigollet): For any integers 1 ≤ k ≤ n, C(n, k) ≤ (e · n / k)^k.

theorem lemma_2_7 (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) : ↑(n.choose k) ≤ (Real.exp 1 * ↑n / ↑k) ^ k

Lemma 2.7 (Rigollet): For any integers 1 ≤ k ≤ n, C(n, k) ≤ (e · n / k)^k.

This is the standard binomial coefficient upper bound.