Lemma 5.14: Sparse Varshamov-Gilbert Bound

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

Lemma 5.14 (Sparse Varshamov-Gilbert). For 1 ≤ k ≤ d/8, there exist M binary vectors ω₁, …, ω_M ∈ {0,1}^d with: (i) ρ(ωⱼ, ωₖ) ≥ k/2 for j ≠ k, (ii) log M ≥ (k/8) log(1 + d/(2k)), (iii) |ωⱼ|₀ = k for all j.

This variant of the Varshamov-Gilbert bound additionally ensures that all vectors have exactly k nonzero entries (sparsity constraint).

Proof structure

The textbook proof uses the probabilistic method:

1. Sample ω uniformly from C₀(k) = {ω ∈ {0,1}^d : |ω|₀ = k}
2. Chernoff bound: P(ρ(ω,x₀) < k/2) ≤ 2^k · (1+d/(2k))^{-k/2}
3. Union bound + probabilistic method: a good packing exists

The proof is decomposed as follows:

• chernoff_counting_bound_ceil (proved): The counting consequence of the Chernoff bound on Hamming ball sizes, for the ceiling-radius ball (textbook-faithful). Uses a combinatorial argument via binomial coefficient ratio bounds and Vandermonde's identity.

• chernoff_counting_bound (proved): The floor-radius version, derived from the ceiling version via sparseBall ⊆ sparseBallCeil.

• chernoff_ball_bound / chernoff_ball_bound_ceil (proved): Derive the existence of a packing number N from the counting bounds.

• sparse_vec_k1_count (proved): For k=1, the count of 1-sparse vectors.

• greedy_packing_bound (proved): Greedy packing from ball size bounds.

• probabilistic_method_sparse_vg (proved): Main theorem from the above.

• sparse_vg_card_bound (proved): Strengthened version with 8 ≤ M and ℝ distance ≥ k/2.

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

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

def SparseVarshamovGilbert.l0norm {d : ℕ} (ω : Fin d → Bool) : ℕ

The ℓ₀ "norm" (number of nonzero / true entries) of a binary vector.

@[reducible, inline]

abbrev SparseVarshamovGilbert.SparseVec (d k : ℕ) : Type

The k-sparse binary vectors as a subtype.

theorem SparseVarshamovGilbert.sparsevec_card (d k : ℕ) : Fintype.card (SparseVec d k) = d.choose k

The cardinality of SparseVec d k equals Nat.choose d k.

The proof constructs an equivalence between SparseVec d k (Boolean functions with exactly k true entries) and {S : Finset (Fin d) // S.card = k} (k-element subsets of Fin d), then applies the Mathlib result Fintype.card_finset_len.

def SparseVarshamovGilbert.sparseBall (d k : ℕ) (x : SparseVec d k) : Finset (SparseVec d k)

Hamming ball in sparse vector space: vectors within Hamming distance < k/2.

theorem SparseVarshamovGilbert.hammingDist_comm {d : ℕ} (f g : Fin d → Bool) : hammingDist f g = hammingDist g f

Symmetry of Hamming distance.

theorem SparseVarshamovGilbert.greedy_packing_bound {α : Type} [Fintype α] [DecidableEq α] (ball : α → Finset α) (B : ℕ) (ball_self : ∀ (x : α), x ∈ ball x) (ball_symm : ∀ (x y : α), y ∈ ball x → x ∈ ball y) (ball_bound : ∀ (x : α), (ball x).card ≤ B) : ∃ (T : Finset α), Fintype.card α ≤ T.card * B ∧ ∀ x ∈ T, ∀ y ∈ T, x ≠ y → y ∉ ball x

Greedy packing bound: given a finite type with a symmetric ball relation and a uniform bound B on ball sizes, there exists a maximal packing T with |universe| ≤ |T| * B. The proof constructs T as a maximum-cardinality independent set in the ball overlap relation, using the finite maximum principle.

theorem SparseVarshamovGilbert.self_mem_sparseBall (d k : ℕ) (hk : 2 ≤ k) (x : SparseVec d k) : x ∈ sparseBall d k x

A vector is always in its own Hamming ball (distance 0 < k/2 for k ≥ 2).

theorem SparseVarshamovGilbert.card_filter_val_lt (d k : ℕ) (hkd : k ≤ d) : {i : Fin d | ↑i < k}.card = k

Counting lemma: the number of Fin d elements with value < k equals k, when k ≤ d.

def SparseVarshamovGilbert.mkSparseVec (d k : ℕ) (hkd : k ≤ d) : SparseVec d k

Construct a k-sparse vector (ones in first k positions) when k ≤ d.

def SparseVarshamovGilbert.sparseBallCeil (d k : ℕ) (x : SparseVec d k) : Finset (SparseVec d k)

Hamming ball in sparse vector space with ceiling radius: vectors within Hamming distance < ⌈k/2⌉ = (k+1)/2. This is the ball corresponding to the textbook's real-valued radius k/2, since for integer distances, dist < k/2 (real) iff dist < ⌈k/2⌉ (nat).

theorem SparseVarshamovGilbert.sparseBall_subset_sparseBallCeil (d k : ℕ) (x : SparseVec d k) : sparseBall d k x ⊆ sparseBallCeil d k x

The floor-radius ball is a subset of the ceiling-radius ball.

def SparseVarshamovGilbert.supp {d : ℕ} (f : Fin d → Bool) : Finset (Fin d)

Support of a Boolean vector: the set of indices where the vector is true.

theorem SparseVarshamovGilbert.eq_of_supp_eq {d : ℕ} (f g : Fin d → Bool) (h : supp f = supp g) : f = g

Boolean vectors are determined by their support.

theorem SparseVarshamovGilbert.hammingDist_eq_sdiff_sum {d : ℕ} (f g : Fin d → Bool) : hammingDist f g = (supp f \ supp g).card + (supp g \ supp f).card

Hamming distance equals the sum of the two set-difference cardinalities.

theorem SparseVarshamovGilbert.card_sdiff_eq_of_card_eq' {α : Type u_1} [DecidableEq α] {A B : Finset α} (h : A.card = B.card) : (A \ B).card = (B \ A).card

For two finsets of equal cardinality, the two set-differences have the same cardinality.

theorem SparseVarshamovGilbert.sdiff_supp_subset_compl {d : ℕ} (f g : Fin d → Bool) : supp f \ supp g ⊆ (supp g)ᶜ

The set-difference of supports lies in the complement of the other support.

theorem SparseVarshamovGilbert.sparseBallCeil_card_le (d k : ℕ) (_hk : 2 ≤ k) (_hkd : k ≤ d / 8) (x : SparseVec d k) : (sparseBallCeil d k x).card ≤ ∑ j ∈ Finset.range ((k + 1) / 2), k.choose j * (d - k).choose j

The sparse ball (ceiling radius) has cardinality bounded by a sum of products of binomial coefficients. For each y in the ball, the support shift from x has some size j < (k+1)/2, contributing C(k,j) · C(d−k,j) possible vectors.

theorem SparseVarshamovGilbert.sparseBallCeil_card_le_tight (d k : ℕ) (_hk : 2 ≤ k) (_hkd : k ≤ d / 8) (x : SparseVec d k) : (sparseBallCeil d k x).card ≤ ∑ j ∈ Finset.range ((k + 3) / 4), k.choose j * (d - k).choose j

Tighter ball cardinality bound: the range is (k+3)/4 instead of (k+1)/2. Since the Hamming distance between k-sparse vectors is always even (= 2j where j is the support shift), dist < (k+1)/2 implies j < (k+3)/4.

theorem SparseVarshamovGilbert.nat_div_cast_gt (a b : ℕ) (hb : 0 < b) : ↑a / ↑b - 1 < ↑(a / b)

Chernoff-type counting bound for sparse Hamming balls (Lemma 5.14 helper).

For k-sparse binary vectors in {0,1}^d with d ≥ 8k, the Hamming ball of radius ⌈(k+1)/2⌉ around any sparse vector x contains at most C(d,k) / ⌈exp(k/8 · log(1+d/(2k)))⌉ elements.

Equivalently: ball.card * ⌈exp(k/8 · log(1+d/(2k)))⌉₊ ≤ C(d,k).

Proved using a combinatorial argument:

1. Ball cardinality ≤ Σ_{j < (k+3)/4} C(k,j)·C(d-k,j) (injection counting)
2. For each j in range: C(k,j)·C(d-k,j)·⌈E⌉₊ ≤ C(k,j)·C(d-k,k-j) (ratio bound)
3. Σ_{j} C(k,j)·C(d-k,k-j) ≤ C(d,k) (Vandermonde identity)

theorem SparseVarshamovGilbert.ceil_exp_choose_le (d k j : ℕ) (hk : 2 ≤ k) (hkd : k ≤ d / 8) (hj : j < (k + 3) / 4) : (d - k).choose j * ⌈Real.exp (↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)))⌉₊ ≤ (d - k).choose (k - j)

theorem SparseVarshamovGilbert.chernoff_counting_bound_ceil (d k : ℕ) (hk : 2 ≤ k) (hkd : k ≤ d / 8) (x : SparseVec d k) : (sparseBallCeil d k x).card * ⌈Real.exp (↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)))⌉₊ ≤ Fintype.card (SparseVec d k)

theorem SparseVarshamovGilbert.chernoff_counting_bound (d k : ℕ) (hk : 2 ≤ k) (hkd : k ≤ d / 8) (x : SparseVec d k) : (sparseBall d k x).card * ⌈Real.exp (↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)))⌉₊ ≤ Fintype.card (SparseVec d k)

The Chernoff counting bound for the floor-radius ball, derived from the ceiling-radius version. Since sparseBall ⊆ sparseBallCeil, the bound transfers.

theorem SparseVarshamovGilbert.chernoff_ball_bound (d k : ℕ) (hk : 2 ≤ k) (hkd : k ≤ d / 8) : ∃ (N : ℕ), 0 < N ∧ ↑N ≥ Real.exp (↑k / 8 * Real.log (1 + ↑d / (2 * ↑k))) ∧ N ≤ Fintype.card (SparseVec d k) ∧ ∀ (x : SparseVec d k), (sparseBall d k x).card * N ≤ Fintype.card (SparseVec d k)

The Chernoff bound on Hamming ball sizes within k-sparse vectors (k ≥ 2).

The textbook proof of Lemma 5.14 shows via the Chernoff method: for any x₀ ∈ C₀(k) with |x₀|₀ = k and d ≥ 8k, the proportion of k-sparse vectors within Hamming distance < k/2 from x₀ is bounded. Specifically:

1. Write ρ(ω, x₀) ≥ k - Σᵢ Zᵢ where Zᵢ = 𝟙(Uᵢ ∈ supp(x₀)) are conditionally Bernoulli with parameter Qᵢ ≤ 2k/d.
2. Chernoff bound with s = log(1 + d/(2k)): E[exp(s·Σ Zᵢ)] ≤ (2k/d·(eˢ-1)+1)^k = 2^k
3. Therefore P(ρ < k/2) ≤ 2^k · (1+d/(2k))^{-k/2}
4. This gives: |ball(x)| · N ≤ |C₀(k)| where N ≥ exp((k/8)·log(1+d/(2k)))

Proved from chernoff_counting_bound which axiomatizes the counting consequence of the Chernoff bound (Steps 3-5 of the textbook proof, where the MGF induction is partially elided).

def SparseVarshamovGilbert.unitVec (d : ℕ) (i : Fin d) : Fin d → Bool

Unit vector: true only at position i.

theorem SparseVarshamovGilbert.l0norm_unitVec (d : ℕ) (i : Fin d) : l0norm (unitVec d i) = 1

def SparseVarshamovGilbert.sparseVecOfFin (d : ℕ) (i : Fin d) : SparseVec d 1

Injection from Fin d to SparseVec d 1: each coordinate gives a 1-sparse vector.

theorem SparseVarshamovGilbert.sparseVecOfFin_injective (d : ℕ) : Function.Injective (sparseVecOfFin d)

theorem SparseVarshamovGilbert.sparse_vec_k1_count (d : ℕ) (hd : 1 ≤ d / 8) : ↑d ≥ Real.exp (1 / 8 * Real.log (1 + ↑d / 2)) ∧ d ≤ Fintype.card (SparseVec d 1)

For k = 1: C₀(1) has exactly d elements (one per coordinate), and the inequality d ≥ exp((1/8)·log(1 + d/2)) holds for d ≥ 8.

The count |C₀(1)| = d is a basic combinatorial fact: each 1-sparse binary vector is determined by its single nonzero coordinate. The inequality follows from d ≥ 1 + d/2 ≥ (1 + d/2)^{1/8} for d ≥ 2.

theorem SparseVarshamovGilbert.probabilistic_method_sparse_vg (d k : ℕ) (hk : 1 ≤ k) (hkd : k ≤ d / 8) : ∃ (M : ℕ) (_ : 0 < M) (ω : Fin M → Fin d → Bool), Real.log ↑M ≥ ↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)) ∧ (∀ (j : Fin M), l0norm (ω j) = k) ∧ ∀ (j k' : Fin M), j ≠ k' → hammingDist (ω j) (ω k') ≥ k / 2

The probabilistic method step for the Sparse Varshamov-Gilbert bound (Lemma 5.14).

Proved from chernoff_ball_bound (Chernoff bound on ball sizes, axiomatized due to missing discrete probability infrastructure in Mathlib), sparse_vec_k1_count (elementary counting axiom for k=1), and greedy_packing_bound (proved greedy packing construction).

theorem SparseVarshamovGilbert.sparse_varshamov_gilbert (d k : ℕ) (hk : 1 ≤ k) (hkd : k ≤ d / 8) : ∃ (M : ℕ) (_ : 0 < M) (ω : Fin M → Fin d → Bool), Real.log ↑M ≥ ↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)) ∧ (∀ (j : Fin M), l0norm (ω j) = k) ∧ ∀ (j k' : Fin M), j ≠ k' → hammingDist (ω j) (ω k') ≥ k / 2

Lemma 5.14 (Sparse Varshamov-Gilbert). For 1 ≤ k ≤ d/8, there exists a set of M binary vectors in {0,1}^d such that:

• log M ≥ (k/8) log(1 + d/(2k)) (sufficiently many vectors),
• every vector has exactly k nonzero entries (sparsity), and
• any two distinct vectors have Hamming distance at least k/2.

The proof uses the probabilistic method: sample vectors uniformly from the set of k-sparse binary vectors and show via Chernoff bound + union bound that a good packing exists with positive probability.

theorem SparseVarshamovGilbert.chernoff_ball_bound_ceil (d k : ℕ) (hk : 2 ≤ k) (hkd : k ≤ d / 8) : ∃ (N : ℕ), 0 < N ∧ ↑N ≥ Real.exp (↑k / 8 * Real.log (1 + ↑d / (2 * ↑k))) ∧ N ≤ Fintype.card (SparseVec d k) ∧ ∀ (x : SparseVec d k), (sparseBallCeil d k x).card * N ≤ Fintype.card (SparseVec d k)

Chernoff ball bound with ceiling radius, derived from chernoff_counting_bound_ceil.

theorem SparseVarshamovGilbert.card_filter_interval (d a k : ℕ) (h : a + k ≤ d) : {i : Fin d | a ≤ ↑i ∧ ↑i < a + k}.card = k

Helper: count elements in an interval [a, a+k) within Fin d.

def SparseVarshamovGilbert.blockSparseVec (d k : ℕ) (hkd : k ≤ d / 8) (j : Fin 8) : SparseVec d k

Block sparse vector: support in positions [j*k, (j+1)*k).

theorem SparseVarshamovGilbert.blockSparseVec_injective (d k : ℕ) (hk : 1 ≤ k) (hkd : k ≤ d / 8) : Function.Injective (blockSparseVec d k hkd)

theorem SparseVarshamovGilbert.card_sparseVec_ge_eight (d k : ℕ) (hk : 1 ≤ k) (hkd : k ≤ d / 8) : 8 ≤ Fintype.card (SparseVec d k)

There are at least 8 k-sparse vectors when k ≤ d/8.

theorem SparseVarshamovGilbert.blockSparseVec_dist (d k : ℕ) (_hk : 1 ≤ k) (hkd : k ≤ d / 8) (i j : Fin 8) (hij : i ≠ j) : hammingDist ↑(blockSparseVec d k hkd i) ↑(blockSparseVec d k hkd j) ≥ k

Block vectors have disjoint supports, so Hamming distance ≥ k.

theorem SparseVarshamovGilbert.nat_ceil_half_ge_real (k n : ℕ) (h : n ≥ (k + 1) / 2) : ↑n ≥ ↑k / 2

Helper: ↑((k+1)/2) ≥ (k : ℝ) / 2 (ℕ ceiling division bounds real half).

theorem SparseVarshamovGilbert.hammingDist_pos_of_ne {d : ℕ} {f g : Fin d → Bool} (h : f ≠ g) : 0 < hammingDist f g

Distinct binary vectors have positive Hamming distance.

theorem SparseVarshamovGilbert.sparseBallCeil_symm (d k : ℕ) (x y : SparseVec d k) : y ∈ sparseBallCeil d k x → x ∈ sparseBallCeil d k y

Symmetry of sparseBallCeil.

theorem SparseVarshamovGilbert.self_mem_sparseBallCeil (d k : ℕ) (hk : 2 ≤ k) (x : SparseVec d k) : x ∈ sparseBallCeil d k x

Self-membership in sparseBallCeil (for k ≥ 2).

theorem SparseVarshamovGilbert.sparse_vg_card_bound (d k : ℕ) (hk : 1 ≤ k) (hkd : k ≤ d / 8) : ∃ (M : ℕ) (_ : 0 < M) (ω : Fin M → Fin d → Bool), 8 ≤ M ∧ Real.log ↑M ≥ ↑k / 8 * Real.log (1 + ↑d / (2 * ↑k)) ∧ (∀ (j : Fin M), l0norm (ω j) = k) ∧ ∀ (j k' : Fin M), j ≠ k' → ↑(hammingDist (ω j) (ω k')) ≥ ↑k / 2

Strengthened Sparse Varshamov-Gilbert with cardinality lower bound 8 ≤ M.

The proof splits into three cases:

1. k = 1: use all d unit vectors (d ≥ 8, pairwise distance = 2 ≥ 1/2 = k/2)
2. k ≥ 2, N < 8: use block vectors (M = 8, distance ≥ k ≥ k/2, log 8 ≥ bound)
3. k ≥ 2, N ≥ 8: ceiling ball greedy packing (M ≥ N ≥ 8, distance ≥ ⌈k/2⌉ ≥ k/2)