Basics of Coding Theory

We define a general code C to be a subset of n → R for some finite index set n and some target type R.

We can then specialize this notion to various settings. For [CommSemiring R], we define a linear code to be a linear subspace of n → R. We also define the notion of generator matrix and (parity) check matrix.

Main Definitions

• codeDist C: The Hamming distance of a code C, defined as the infimum (in ℕ∞) of the Hamming distances between any two distinct elements of C. This is noncomputable.

• codeDist' C: A computable version of codeDist C, assuming C is a Fintype.

We define the block length, rate, and distance of C. We prove simple properties of linear codes such as the singleton bound.

def «termΔ₀(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «term‖_‖₀» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℕ

The Hamming distance of a code C is the minimum Hamming distance between any two distinct elements of the code. cd We formalize this as the infimum sInf over all d : ℕ such that there exist u v : n → R in the code with u ≠ v and hammingDist u v ≤ d. If none exists, then we define the distance to be 0.

Equations

• ‖C‖₀ = sInf {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ Δ₀(u, v) ≤ d}

instance instEDistForall_arkLib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : EDist (n → R)

Equations

• instEDistForall_arkLib = { edist := fun (u v : n → R) => ↑Δ₀(u, v) }

instance instDistForall_arkLib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : Dist (n → R)

Equations

• instDistForall_arkLib = { dist := fun (u v : n → R) => ↑Δ₀(u, v) }

noncomputable def eCodeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ENNReal

Equations

• eCodeDistNew C = C.einfsep

noncomputable def codeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℝ

Equations

• codeDistNew C = C.infsep

def «term‖_‖₀_1» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def distFromCode {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : ℕ∞

The distance from a vector u to a code C is the minimum Hamming distance between u and any element of C.

Equations

• Δ₀(u, C) = sInf {d : ℕ∞ | ∃ v ∈ C, ↑Δ₀(u, v) ≤ d}

def «termΔ₀(_,_)_1» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem codeDist_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀ = 0

@[simp]

theorem codeDist_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Subsingleton ↑C] : ‖C‖₀ = 0

@[simp]

theorem codeDist_le_card {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ‖C‖₀ ≤ Fintype.card n

theorem eq_of_lt_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} {u v : n → R} (hu : u ∈ C) (hv : v ∈ C) (huv : Δ₀(u, v) < ‖C‖₀) : u = v

If u and v are two codewords of C with distance less than codeDist C, then they are the same.

@[simp]

theorem distFromCode_of_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) : Δ₀(u, ∅) = ⊤

theorem distFromCode_eq_top_iff_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : Δ₀(u, C) = ⊤ ↔ C = ∅

@[simp]

theorem distFromCode_of_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) {u : n → R} (h : u ∈ C) : Δ₀(u, C) = 0

theorem distFromCode_eq_zero_iff_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) : Δ₀(u, C) = 0 ↔ u ∈ C

theorem distFromCode_eq_of_lt_half_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) {v w : n → R} (hv : v ∈ C) (hw : w ∈ C) (huv : Δ₀(u, v) < ‖C‖₀ / 2) (hvw : Δ₀(u, w) < ‖C‖₀ / 2) : v = w

def codeDist' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] : ℕ∞

Computable version of the Hamming distance of a code C, assuming C is a Fintype.

The return type is ℕ∞ since we use Finset.min.

Equations

• ‖C‖₀' = (Finset.image (fun (x : ↑C × ↑C) => match x with | (u, v) => Δ₀(↑u, ↑v)) {p : ↑C × ↑C | p.1 ≠ p.2}).min

def «term‖_‖₀'» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem codeDist'_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀' = ⊤

@[simp]

theorem codeDist'_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] [Subsingleton ↑C] : ‖C‖₀' = ⊤

theorem codeDist'_eq_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] : ‖C‖₀'.toNat = ‖C‖₀

def distFromCode' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] (u : n → R) : ℕ∞

Computable version of the distance from a vector u to a code C, assuming C is a Fintype.

Equations

• Δ₀'(u, C) = (Finset.image (fun (v : ↑C) => Δ₀(u, ↑v)) Finset.univ).min

def «termΔ₀'(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def codeByGenMatrix {n : Type u_1} {R : Type u_2} {k : Type u_3} [Fintype k] [CommSemiring R] (G : Matrix k n R) : Submodule R (n → R)

Define a linear code from its generator matrix

Equations

• codeByGenMatrix G = LinearMap.range G.vecMulLinear

def codeByCheckMatrix {n : Type u_1} [Fintype n] {R : Type u_2} {k : Type u_3} [CommSemiring R] (H : Matrix k n R) : Submodule R (n → R)

Define a linear code from its (parity) check matrix

Equations

• codeByCheckMatrix H = LinearMap.ker H.mulVecLin

noncomputable def linearCodeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] (C : Submodule R (n → R)) : ℕ

The Hamming distance of a linear code can also be defined as the minimum Hamming norm of a non-zero vector in the code

Equations

• linearCodeDist C = sInf {d : ℕ | ∃ u ∈ C, u ≠ 0 ∧ ‖u‖₀ ≤ d}

theorem codeDist_eq_linearCodeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] (C : Submodule R (n → R)) : ‖C.carrier‖₀ = linearCodeDist C

def linearCodeDist' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] [DecidableEq n] [Fintype R] (C : Submodule R (n → R)) [DecidablePred fun (x : n → R) => x ∈ C] : ℕ∞

A computable version of the Hamming distance of a linear code C.

Equations

• linearCodeDist' C = (Finset.image (fun (v : ↥C) => ‖↑v‖₀) {v : ↥C | v ≠ 0}).min

def interleaveCode {n : Type u_1} {R : Type u_2} [CommSemiring R] (C : Submodule R (n → R)) (ι : Type u_4) : Submodule R (ι × n → R)

The interleaving of a linear code C over index set ι is the submodule spanned by ι × n-matrices whose rows are elements of C.

Equations

• (C^⋈ι) = Submodule.span R {v : ι × n → R | ∀ (i : ι), ∃ c ∈ C, c = fun (j : n) => v (i, j)}

def «term_^⋈_» : Lean.TrailingParserDescr

Equations

• «term_^⋈_» = Lean.ParserDescr.trailingNode `«term_^⋈_» 20 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^⋈") (Lean.ParserDescr.cat `term 0))

def Function.interleave₂ {α : Type u_4} {β : Type u_5} (u v : α → β) : Fin 2 × α → β

Interleave two functions u v : α → β.

Equations

• (u⋈v) = Function.uncurry fun (a : Fin 2) => if a = 0 then u else v

def «term_⋈_» : Lean.TrailingParserDescr

Equations

• «term_⋈_» = Lean.ParserDescr.trailingNode `«term_⋈_» 20 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋈") (Lean.ParserDescr.cat `term 0))

theorem singleton_bound {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [Finite R] (C : Set (n → R)) : Fintype.card ↑C ≤ Fintype.card R ^ (Fintype.card n - ‖C‖₀ + 1)

Singleton bound for arbitrary codes

theorem singleton_bound_linear {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [Finite R] [DivisionRing R] (C : Submodule R (n → R)) : Module.finrank R ↥C ≤ Fintype.card n - ‖C.carrier‖₀ + 1

Singleton bound for linear codes