Chernoff Helpers: Hamming Distance Structure for Equal-Weight Boolean Vectors

Helper lemmas supporting the proof of Lemma 5.14 (Sparse Varshamov-Gilbert) from Chapter 5.4 of Rigollet's "High Dimensional Statistics".

Main results

1. hammingDist_eq_two_mul_sdiff (re-exported from SparseBallCard): For vectors ω, ω' ∈ {0,1}^d with Hamming weight k, hammingDist(ω, ω') = 2 * |supp(ω) \ supp(ω')|.

2. sparse_ball_radius_card: General ball counting formula: |{ω' : wt(ω') = k, hammingDist(ω, ω') ≤ 2t}| = ∑_{j=0}^{t} C(k,j) * C(d-k,j).

3. sparsevec_card (re-exported from Lemma_5_14): |{ω ∈ {0,1}^d : |ω|₀ = k}| = C(d,k).

These are helper lemmas used in the proof of Lemma 5.14. The key mathematical insight is that for equal-weight Boolean vectors, the Hamming distance decomposes into a symmetric difference on supports, which enables counting via combinatorial bijections.

Proof outline for hammingDist_eq_two_mul_sdiff

For binary vectors x, y with |x|₀ = |y|₀ = k:

• The positions where x and y disagree are (supp(x) \ supp(y)) ∪ (supp(y) \ supp(x)).
• These two sets are disjoint (both sides of a symmetric difference).
• By equal weight, |supp(x) \ supp(y)| = |supp(y) \ supp(x)|.
• Therefore, hammingDist(x, y) = |supp(x) \ supp(y)| + |supp(y) \ supp(x)| = 2 * |supp(x) \ supp(y)|.

Proof outline for sparse_ball_radius_card

The ball {y : wt(y) = k, dist(x,y) ≤ 2t} is in bijection with ∐_{j=0}^{t} {(J, K) : J ⊆ supp(x), K ⊆ supp(x)ᶜ, |J| = |K| = j}:

• Forward: (j, J, K) ↦ flipVec(x, J, K) (flip J-bits off and K-bits on)
• Inverse: y ↦ (|supp(x)\supp(y)|, supp(x)\supp(y), supp(y)\supp(x)) The fiber at j has cardinality C(k,j) · C(d-k,j), giving the formula.

Hamming ball with general radius

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

Hamming ball of radius ≤ 2t in the space of k-sparse binary vectors. For equal-weight vectors, the Hamming distance is always even, so this captures all vectors within "combinatorial radius" t (number of support swaps).

theorem SparseVarshamovGilbert.sparse_ball_radius_card (d k t : ℕ) (hkd : k ≤ d) (x : SparseVec d k) : (sparseBallRadius d k t x).card = ∑ j ∈ Finset.range (t + 1), k.choose j * (d - k).choose j

Ball counting formula for equal-weight Boolean vectors.

For a k-sparse binary vector x in {0,1}^d, the ball of radius ≤ 2t has cardinality: |{y : wt(y) = k, dist(x, y) ≤ 2t}| = ∑_{j=0}^{t} C(k, j) · C(d-k, j)

This is a key combinatorial identity used in the proof of the Sparse Varshamov-Gilbert lemma (Lemma 5.14). The proof constructs an explicit bijection between the ball and the sigma type ∐_{j ≤ t} (j-subsets of supp(x)) × (j-subsets of supp(x)ᶜ).