Hamming Bound

This file establishes the Hamming bound (also called the sphere-packing bound): for a code C of block-length n and minimum distance d over a q-ary alphabet α,

|C| · Vol(n, ⌊(d-1)/2⌋) ≤ |α|^n,

where Vol(n, t) = Σ_{i=0}^{t} C(n,i) · (|α|-1)^i is the volume of a Hamming ball of radius t.

Main Results

• hamming_ball_size : the exact volume formula for Hamming balls.
• hamming_ball_non_intersect : balls of radius ⌊(d-1)/2⌋ around distinct codewords of a code with minimum distance d are disjoint.
• hamming_bound : the Hamming (sphere-packing) bound.

theorem CodingTheory.Codeword.hamming_ball_size {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n l : ℕ) (c : Codeword n α) : (hamming_ball l c).card = ∑ i ∈ Finset.range (l + 1), n.choose i * (Fintype.card α - 1) ^ i

Volume formula: the Hamming ball of radius l centred at any codeword has exactly Σ_{i=0}^{l} C(n,i) · (|α|-1)^i elements.

theorem CodingTheory.Codeword.hamming_ball_non_intersect {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n d : ℕ} (C : Code n α) (h : distance C d) (h' : 0 < d) (c₁ c₂ : Codeword n α) : c₁ ∈ C ∧ c₂ ∈ C ∧ c₁ ≠ c₂ → ∀ c' ∈ hamming_ball ⌊(↑d - 1) / 2⌋₊ c₁, c' ∉ hamming_ball ⌊(↑d - 1) / 2⌋₊ c₂

Hamming balls of radius ⌊(d-1)/2⌋ around distinct codewords of a code with minimum distance d are disjoint: no point can lie within that radius of two distinct codewords.

theorem CodingTheory.Codeword.hamming_ball'_disjoint {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n d : ℕ} (C : Code n α) (h : distance C d) (h' : 0 < d) (c₁ c₂ : Codeword n α) : c₁ ∈ C ∧ c₂ ∈ C ∧ c₁ ≠ c₂ → Disjoint (hamming_ball ⌊(↑d - 1) / 2⌋₊ c₁) (hamming_ball ⌊(↑d - 1) / 2⌋₊ c₂)

Helper: Hamming balls of radius ⌊(d-1)/2⌋ around distinct codewords are pairwise disjoint as Finsets.

theorem CodingTheory.Codeword.hamming_bound {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n d : ℕ) (C : Code n α) (h : distance C d) (h'' : Fintype.card α > 1) (hd : 0 < d) : Finset.card C ≤ Fintype.card α ^ n / ∑ i ∈ Finset.range (⌊(↑d - 1) / 2⌋₊ + 1), n.choose i * (Fintype.card α - 1) ^ i

Hamming bound (sphere-packing bound): a code C of block-length n and minimum distance d over an alphabet α with |α| > 1 satisfies |C| ≤ |α|^n / Vol(n, ⌊(d-1)/2⌋).