Hamming balls, the Hamming bound and the Gilbert–Varshamov bound

The words ∀ i, β i at Hamming distance exactly r from a word x are obtained by choosing the r positions where they differ and a different letter at each, so there are ∑_{|S| = r} ∏_{i ∈ S} (|β i| - 1) of them, whatever x is (card_filter_hammingDist_eq); over an alphabet of q letters at each of n positions this is C(n, r) (q - 1) ^ r (card_filter_hammingDist_eq_choose_mul_pow). Balls of radius r around the words of a code whose distinct words are at distance more than 2 r are disjoint, so the code has at most q ^ n / V words, where V is the size of a ball: the Hamming bound (card_mul_card_filter_hammingDist_le_le_prod, card_mul_sum_choose_le_of_two_mul_lt_hammingDist) [Ham50], MacWilliams and Sloane, Chapter 1, Theorem 6. Conversely, the balls of radius d - 1 around a largest code of minimum distance d cover every word, so some code of minimum distance d has at least q ^ n / V words, where V is the size of a ball of radius d - 1: the Gilbert–Varshamov bound (exists_prod_le_card_mul_card_filter_hammingDist_lt, exists_pow_le_card_mul_sum_choose_of_le_hammingDist) [Gil52], by Gilbert's greedy argument; Varshamov proved the same bound for linear codes [Var57].

Main results

• card_filter_hammingDist_eq: the size of a Hamming sphere.
• card_filter_hammingDist_le_eq_sum: the size of a Hamming ball, as a sum of sphere sizes.
• card_mul_card_filter_hammingDist_le_le_prod: the Hamming bound.
• card_mul_sum_choose_le_of_two_mul_lt_hammingDist: the Hamming bound over a q-letter alphabet.
• exists_prod_le_card_mul_card_filter_hammingDist_lt: the Gilbert–Varshamov bound.
• exists_pow_le_card_mul_sum_choose_of_le_hammingDist: the Gilbert–Varshamov bound over a q-letter alphabet.

References

• R. W. Hamming, Error detecting and error correcting codes
• E. N. Gilbert, A comparison of signalling alphabets
• R. R. Varshamov, Estimate of the number of signals in error correcting codes
• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

theorem card_filter_hammingDist_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (r : ℕ) : {y : (i : ι) → β i | hammingDist x y = r}.card = ∑ S ∈ Finset.powersetCard r Finset.univ, ∏ i ∈ S, (Fintype.card (β i) - 1)

The size of a Hamming sphere: the words at distance r from x. It does not depend on x.

theorem card_filter_hammingDist_eq_choose_mul_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] {q : ℕ} (hq : ∀ (i : ι), Fintype.card (β i) = q) (x : (i : ι) → β i) (r : ℕ) : {y : (i : ι) → β i | hammingDist x y = r}.card = (Fintype.card ι).choose r * (q - 1) ^ r

Over an alphabet of q letters at each of n positions, a Hamming sphere of radius r has C(n, r) (q - 1) ^ r words.

theorem card_filter_hammingDist_le_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (r : ℕ) : {y : (i : ι) → β i | hammingDist x y ≤ r}.card = ∑ j ∈ Finset.range (r + 1), {y : (i : ι) → β i | hammingDist x y = j}.card

The size of a Hamming ball is the sum of the sizes of the spheres.

theorem card_mul_card_filter_hammingDist_le_le_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] {C : Finset ((i : ι) → β i)} {r : ℕ} (hC : (↑C).Pairwise fun (x y : (i : ι) → β i) => 2 * r < hammingDist x y) (x₀ : (i : ι) → β i) : C.card * {y : (i : ι) → β i | hammingDist x₀ y ≤ r}.card ≤ ∏ i : ι, Fintype.card (β i)

The Hamming bound: a code whose distinct words are at distance more than 2 r has at most ∏ i, |β i| words in all of its balls of radius r together.

theorem card_mul_sum_choose_le_of_two_mul_lt_hammingDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] {q : ℕ} (hq : ∀ (i : ι), Fintype.card (β i) = q) {C : Finset ((i : ι) → β i)} {r : ℕ} (hC : (↑C).Pairwise fun (x y : (i : ι) → β i) => 2 * r < hammingDist x y) : C.card * ∑ j ∈ Finset.range (r + 1), (Fintype.card ι).choose j * (q - 1) ^ j ≤ q ^ Fintype.card ι

The Hamming bound over a q-letter alphabet at each of n positions: a code whose distinct words are at distance more than 2 r has at most q ^ n / V words, where V = ∑_{j ≤ r} C(n, j) (q - 1) ^ j is the size of a ball of radius r.

theorem exists_prod_le_card_mul_card_filter_hammingDist_lt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] {d : ℕ} (hd : 0 < d) (x₀ : (i : ι) → β i) : ∃ (C : Finset ((i : ι) → β i)), ((↑C).Pairwise fun (x y : (i : ι) → β i) => d ≤ hammingDist x y) ∧ ∏ i : ι, Fintype.card (β i) ≤ C.card * {y : (i : ι) → β i | hammingDist x₀ y < d}.card

The Gilbert–Varshamov bound [Gil52]: for d ≥ 1 there is a code whose distinct words are at distance at least d and which has at least ∏ i, |β i| / V words, where V is the size of a ball of radius d - 1. A largest such code works: its balls of radius d - 1 cover every word, since a word at distance at least d from every codeword could be added to it.

theorem exists_pow_le_card_mul_sum_choose_of_le_hammingDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → Fintype (β i)] [(i : ι) → DecidableEq (β i)] {q : ℕ} (hq : ∀ (i : ι), Fintype.card (β i) = q) {d : ℕ} (hd : 0 < d) : ∃ (C : Finset ((i : ι) → β i)), ((↑C).Pairwise fun (x y : (i : ι) → β i) => d ≤ hammingDist x y) ∧ q ^ Fintype.card ι ≤ C.card * ∑ j ∈ Finset.range d, (Fintype.card ι).choose j * (q - 1) ^ j

The Gilbert–Varshamov bound [Gil52] over a q-letter alphabet at each of n positions: for d ≥ 1 there is a code whose distinct words are at distance at least d and which has at least q ^ n / V words, where V = ∑_{j < d} C(n, j) (q - 1) ^ j is the size of a ball of radius d - 1.