The Hamming and Gilbert–Varshamov bounds for the minimum distance

The Hamming bound and the Gilbert–Varshamov bound of Complexity.Foundations.Data.HammingBound, stated there for codes whose distinct words are pairwise far apart, restated in terms of the minimum distance Cslib.Code.minDist. Over an alphabet of q letters at each of n positions, a code of minimum distance more than 2 r has at most q ^ n / V words, where V is the size of a ball of radius r (Cslib.Code.card_mul_sum_choose_le_of_two_mul_lt_minDist) [Ham50]; and for d ≥ 1 some code of minimum distance at least d has at least q ^ n / V words, where V is the size of a ball of radius d - 1 (Cslib.Code.exists_le_minDist_and_pow_le_card_mul_sum_choose) [Gil52].

Main results

• Cslib.Code.card_mul_sum_choose_le_of_two_mul_lt_minDist: the Hamming bound.
• Cslib.Code.exists_le_minDist_and_pow_le_card_mul_sum_choose: the Gilbert–Varshamov bound.

References

• R. W. Hamming, Error detecting and error correcting codes
• E. N. Gilbert, A comparison of signalling alphabets

theorem Cslib.Code.card_mul_sum_choose_le_of_two_mul_lt_minDist {ι : 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 : 2 * ↑r < minDist ↑C) : C.card * ∑ j ∈ Finset.range (r + 1), (Fintype.card ι).choose j * (q - 1) ^ j ≤ q ^ Fintype.card ι

The Hamming bound [Ham50] over a q-letter alphabet at each of n positions: a code of minimum 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 Cslib.Code.exists_le_minDist_and_pow_le_card_mul_sum_choose {ι : 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)), ↑d ≤ minDist ↑C ∧ 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 some code of minimum distance at least d 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.