Lemma 5.12: Varshamov-Gilbert Bound

From Chapter 5.4 of Rigollet's "High Dimensional Statistics."

Lemma 5.12 (Varshamov-Gilbert). For any γ ∈ (0, 1/2), there exist M binary vectors ω₁, …, ω_M ∈ {0,1}^d with: (i) ρ(ωⱼ, ωₖ) ≥ (1/2 - γ)d for j ≠ k, (ii) M ≥ e^{γ²d/2}.

Proof strategy (probabilistic method)

The proof proceeds in four steps:

1. Random construction. Draw M independent random vectors ω₁, …, ω_M ∈ {0,1}^d where each coordinate ωⱼᵢ is i.i.d. Bernoulli(1/2).

2. Pairwise distance distribution. For any fixed pair j ≠ k, the Hamming distance ρ(ωⱼ, ωₖ) = Σᵢ 𝟙{ωⱼᵢ ≠ ωₖᵢ} is a sum of d independent Bernoulli(1/2) indicators, so ρ(ωⱼ, ωₖ) ~ Binomial(d, 1/2) with E[ρ] = d/2.

3. Concentration (Hoeffding). By Hoeffding's inequality applied to the sum of bounded independent random variables: P(ρ(ωⱼ, ωₖ) < (1/2 − γ)d) = P(ρ < E[ρ] − γd) ≤ exp(−2γ²d)

4. Union bound and counting. Set M = ⌊exp(γ²d/2)⌋. There are M(M−1)/2 < M²/2 pairs. By the union bound: P(∃ j≠k : ρ(ωⱼ,ωₖ) < (1/2−γ)d) ≤ (M²/2) · exp(−2γ²d) ≤ (1/2) · exp(γ²d) · exp(−2γ²d) = (1/2) · exp(−γ²d) < 1 Hence P(all pairs well-separated) > 0, so a valid configuration exists.

def VarshamovGilbert.hammingDist {d : ℕ} (ω₁ ω₂ : Fin d → Bool) : ℕ

Hamming distance between two binary vectors, defined locally to avoid heavy imports.

theorem VarshamovGilbert.varshamov_gilbert (d : ℕ) (hd : 0 < d) (γ : ℝ) (hγ_pos : 0 < γ) (hγ_lt : γ < 1 / 2) : ∃ (M : ℕ) (_ : 0 < M) (ω : Fin M → Fin d → Bool), ↑M ≥ Real.exp (γ ^ 2 * ↑d / 2) ∧ ∀ (j k : Fin M), j ≠ k → ↑(hammingDist (ω j) (ω k)) ≥ (1 / 2 - γ) * ↑d

Lemma 5.12 (Varshamov-Gilbert).

For any γ ∈ (0, 1/2) and positive dimension d, there exists a set of M binary vectors in {0,1}^d such that:

• M ≥ exp(γ² d / 2) (exponentially many vectors), and
• any two distinct vectors have Hamming distance at least (1/2 - γ) d.

The proof uses the probabilistic method: draw M i.i.d. uniform binary vectors and show via Hoeffding's inequality and a union bound that with positive probability all pairs are well-separated.