Linear Codes and the Uniformity Lemma

This file develops the theory of linear codes and a key probabilistic tool used in the Gilbert–Varshamov existence argument.

Main Definitions

• uniform_vector_dist n α : the uniform distribution on length-n vectors over α.
• matrix_dist n k x : the distribution on length-n output vectors induced by a uniformly random generator matrix G applied to a fixed nonzero message x ∈ αᵏ.
• get_matrix_row : utility to extract row i of a matrix as a 1×k matrix.

Main Results

• Linear_Code_dist_eq_min_weight : for a linear code, minimum distance equals minimum nonzero weight.
• finite_matrix_dist : the set {G | G·x = v} is finite.
• uniformity_lemma : for any nonzero x ∈ αᵏ, the output G·x is uniformly distributed over αⁿ when G is a uniformly random n×k matrix over α.

theorem CodingTheory.Codeword.Linear_Code_dist_eq_min_weight {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n m d : ℕ} (C : Code n α) (h_linear : Linear_Code' C m) (h : distance C d) : (∀ c ∈ C, c ≠ 0 → c.weight ≥ d) ∧ ∃ c ∈ C, c.weight = d

For a linear code, minimum distance equals minimum nonzero Hamming weight.

noncomputable def CodingTheory.Codeword.uniform_vector_dist (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Codeword n α → ℝ

The uniform distribution on length-n vectors: each vector has probability 1/|α|^n.

Equations

• CodingTheory.Codeword.uniform_vector_dist n α x✝ = 1 / ↑(Fintype.card α) ^ n

theorem CodingTheory.Codeword.finite_matrix_dist {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n k : ℕ) (v : Codeword n α) (x : Codeword k α) : {G : Matrix (Fin n) (Fin k) α | G.mulVec x = v}.Finite

The set of matrices G such that G·x = v is finite.

noncomputable def CodingTheory.Codeword.matrix_dist {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n k : ℕ) (x : Codeword k α) : Codeword n α → ℝ

The distribution on αⁿ induced by applying a uniformly random n×k matrix to x: matrix_dist n k x v = |{G | G·x = v}| / |α|^(n·k).

Equations

• CodingTheory.Codeword.matrix_dist n k x v = ↑⋯.toFinset.card / ↑(Fintype.card α) ^ (n * k)

def CodingTheory.Codeword.get_matrix_row {α : Type u_1} (n k : ℕ) (M : Matrix (Fin n) (Fin k) α) (i : Fin n) : Matrix (Fin 1) (Fin k) α

Utility: extract row i of matrix M as a 1×k matrix.

Equations

• CodingTheory.Codeword.get_matrix_row n k M i = Matrix.of fun (x : Fin 1) (j : Fin k) => M i j

theorem CodingTheory.Codeword.uniformity_lemma {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n k : ℕ) (x : Codeword k α) (h_x : x ≠ zero) (h_k : k ≥ 1) : matrix_dist n k x = uniform_vector_dist n α

Uniformity Lemma: for any nonzero x ∈ αᵏ, applying a uniformly random n×k matrix over α to x yields the uniform distribution over αⁿ.