Gilbert–Varshamov Bound

This file proves the Gilbert–Varshamov (GV) existence bound: for any block-length n, dimension k, and distance d over a q-ary alphabet α, if

k ≤ n − ⌈log_q Vol(n, d−1)⌉ − 1,

then there exists an n × k generator matrix G such that the linear code G·αᵏ has minimum distance at least d.

The proof proceeds via a probabilistic argument:

1. prob_leq_ball_size : for any nonzero message x, the probability that a random generator matrix G sends x to a low-weight codeword is at most Vol(n,d−1)/|α|ⁿ.

2. existence_bound : by a union bound over all nonzero messages, the number of "bad" generator matrices (those sending some nonzero x to a codeword of weight < d) is at most (|α|ᵏ − 1) · |α|^(nk−n) · Vol(n, d−1).

3. gv_bound : if k is small enough (satisfying the GV condition), the number of bad matrices is strictly less than the total |α|^(nk), so at least one good matrix exists.

Main Results

• prob_leq_ball_size : probabilistic bound on low-weight outputs.
• existence_bound : union-bound count of bad generator matrices.
• gv_bound : existence of a good generator matrix satisfying the GV condition.

theorem CodingTheory.Codeword.prob_leq_ball_size {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n k : ℕ} (x : Codeword k α) (d : ℕ) (h_k : k ≥ 1) (h_x : x ≠ 0) (h_d : d > 0) : ↑{G : Matrix (Fin n) (Fin k) α | weight (G.mulVec x) < d}.toFinset.card / ↑(Fintype.card α) ^ (n * k) ≤ ↑(hamming_ball (d - 1) zero).card / ↑(Fintype.card α) ^ n

Probabilistic bound: for any nonzero message x ∈ αᵏ, the fraction of n×k matrices G for which G·x has Hamming weight less than d is at most Vol(n,d−1)/|α|ⁿ.

theorem CodingTheory.Codeword.existence_bound {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n k : ℕ} (d : ℕ) (h_k : k ≥ 1) (h_d : d > 0) : {G : Matrix (Fin n) (Fin k) α | ∃ (x : Codeword k α), x ≠ 0 ∧ weight (G.mulVec x) < d}.toFinset.card ≤ (Fintype.card α ^ k - 1) * Fintype.card α ^ (n * k - n) * (hamming_ball (d - 1) zero).card

Union bound: the number of n×k generator matrices G for which some nonzero message x is sent to a codeword of weight less than d is at most (|α|ᵏ − 1) · |α|^(nk−n) · Vol(n, d−1).

theorem CodingTheory.Codeword.gv_bound {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n k q d : ℕ) (h_q : q = Fintype.card α) (h_k : k ≤ n - Nat.clog q (hamming_ball (d - 1) zero).card - 1) : {G : Matrix (Fin n) (Fin k) α | ∀ (x : Codeword k α), x ≠ 0 → weight (G.mulVec x) ≥ d}.toFinset.card ≥ 1

Gilbert–Varshamov bound: if k ≤ n − ⌈log_q Vol(n, d−1)⌉ − 1, then there exists an n×k generator matrix G such that every nonzero message is mapped to a codeword of Hamming weight at least d.