Hamming balls and volume

Definitions and cardinality results for Hamming balls and spheres over finite alphabets. Used in distributional lower bounds (e.g., the randomized indexing lower bound via Roughgarden's counting argument).

Ported from CS 294 lecture exercises (lec-294/lec6.lean).

Main definitions

• hammingBall u r: the Finset of codewords within Hamming distance r of u
• hammingSphere u r: the Finset of codewords at exactly Hamming distance r from u
• ballVol n t q: the volume formula Σ_{i=0}^{t} C(n,i) · (q-1)^i

Main results

• hammingSphere_card: |S(u, k)| = C(n, k) · (q-1)^k
• hammingBall_card: |B(u, r)| = ballVol n r q

@[reducible, inline]

abbrev CommunicationComplexity.Word (n : ℕ) (α : Type u_2) : Type u_2

A codeword of length n over alphabet α.

Equations

• CommunicationComplexity.Word n α = (Fin n → α)

def CommunicationComplexity.hammingBall {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r : ℕ) : Finset (Word n α)

The Hamming ball of radius r centered at u: all words within distance r.

Equations

• CommunicationComplexity.hammingBall u r = {v : CommunicationComplexity.Word n α | hammingDist u v ≤ r}

def CommunicationComplexity.hammingSphere {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r : ℕ) : Finset (Word n α)

The Hamming sphere of radius r centered at u: all words at exactly distance r.

Equations

• CommunicationComplexity.hammingSphere u r = {v : CommunicationComplexity.Word n α | hammingDist u v = r}

def CommunicationComplexity.ballVol (n t q : ℕ) : ℕ

The volume of a Hamming ball: Σ_{i=0}^{t} C(n, i) · (q-1)^i.

Equations

• CommunicationComplexity.ballVol n t q = ∑ i ∈ Finset.range (t + 1), n.choose i * (q - 1) ^ i

Sphere and ball decomposition

theorem CommunicationComplexity.hammingSpheres_disjoint {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r t : ℕ) (hrt : r ≠ t) : Disjoint (hammingSphere u r) (hammingSphere u t)

theorem CommunicationComplexity.hammingSpheres_pairwise_disjoint {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r : ℕ) : (↑(Finset.range r)).PairwiseDisjoint fun (t : ℕ) => hammingSphere u t

theorem CommunicationComplexity.hammingBall_eq_hammingSpheres {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r : ℕ) : hammingBall u r = (Finset.range (r + 1)).disjiUnion (fun (k : ℕ) => hammingSphere u k) ⋯

Support fibers and sphere cardinality

theorem CommunicationComplexity.hammingSphere_card {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (k : ℕ) : (hammingSphere u k).card = n.choose k * (Fintype.card α - 1) ^ k

theorem CommunicationComplexity.hammingBall_card {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (u : Word n α) (r : ℕ) : (hammingBall u r).card = ballVol n r (Fintype.card α)

theorem CommunicationComplexity.ballVol_binary (n t : ℕ) : ballVol n t 2 = ∑ i ∈ Finset.range (t + 1), n.choose i

Binary Hamming ball volume: Σ_{i=0}^{t} C(n, i).