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

• dist 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.

• dist' C: A computable version of dist 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 Code.«termΔ₀(_,_)» : Lean.ParserDescr

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

noncomputable def Code.dist {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. 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.

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

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

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

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

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

noncomputable def Code.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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Code.eq_of_lt_dist {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 dist C, then they are the same.

@[simp]

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

theorem Code.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 Code.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 Code.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 Code.distFromCode_eq_of_lt_half_dist {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 Code.dist' {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.

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

@[simp]

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

@[simp]

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

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

def Code.possibleDistsToCode {α : Type u_3} {F : Type u_4} {ι : Type u_5} (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf from a vector w to a code C.

def Code.possibleDists {α : Type u_3} {F : Type u_4} {ι : Type u_5} (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf between distinct codewords in a code C.

• TODO: This allows us to express distance in non-ℝ, which is quite convenient. Extending to (E)Dist forces this into ℝ; give some thought.

noncomputable def Code.distToCode {α : Type u_3} {F : Type u_4} {ι : Type u_5} [LinearOrder α] [Zero α] (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) (h : (possibleDistsToCode w C δf).Finite) : WithTop α

A generalisation of distFromCode for an arbitrary distance function δf.

theorem Code.distToCode_of_nonempty {α : Type u_3} [LinearOrder α] [Zero α] {ι : Type u_4} {F : Type u_5} {w : ι → F} {C : Set (ι → F)} {δf : (ι → F) → (ι → F) → α} (h₁ : (possibleDistsToCode w C δf).Finite) (h₂ : (possibleDistsToCode w C δf).Nonempty) : distToCode w C δf h₁ = ↑((possibleDistsToCode w C δf).toFinset.min' ⋯)

def Code.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.

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

def Code.relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) : ℚ≥0

def Code.«termδᵣ(_,_)» : Lean.ParserDescr

δᵣ(u,v) denotes the relative Hamming distance between vectors u and v.

@[simp]

theorem Code.relHammingDist_le_one {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : δᵣ(u, v) ≤ 1

The relative Hamming distance between two vectors is at most 1.

@[simp]

theorem Code.zero_le_relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : 0 ≤ δᵣ(u, v)

The relative Hamming distance between two vectors is non-negative.

def Code.relHammingDistRange (ι : Type u_5) [Fintype ι] : Set ℚ≥0

The range of the relative Hamming distance function.

@[simp]

theorem Code.relHammingDist_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [DecidableEq F] : δᵣ(u, v) ∈ relHammingDistRange ι

The range of the relative Hamming distance is well-defined.

@[simp]

theorem Code.finite_relHammingDistRange {ι : Type u_3} [Fintype ι] [Nonempty ι] : (relHammingDistRange ι).Finite

The range of the relative Hamming distance function is finite.

@[simp]

theorem Code.finite_offDiag {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [Finite F] : C.offDiag.Finite

The set of pairs of distinct elements from a finite set is finite.

def Code.possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : Set ℚ≥0

The set of possible distances between distinct codewords in a code.

@[simp]

theorem Code.possibleRelHammingDists_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] : possibleRelHammingDists C ⊆ relHammingDistRange ι

The set of possible distances between distinct codewords in a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem Code.finite_possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] [Nonempty ι] : (possibleRelHammingDists C).Finite

The set of possible distances between distinct codewords in a code is a finite set.

def Code.minRelHammingDistCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) : ℚ≥0

The minimum relative Hamming distance of a code.

def Code.termδᵣ_ : Lean.ParserDescr

δᵣ C denotes the minimum relative Hamming distance of a code C.

@[simp]

theorem Code.possibleRelHammingDistsToC_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [DecidableEq F] : possibleDistsToCode w C relHammingDist ⊆ relHammingDistRange ι

The range set of possible relative Hamming distances from a vector to a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem Code.finite_possibleRelHammingDistsToCode {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : (possibleDistsToCode w C relHammingDist).Finite

The set of possible relative Hamming distances from a vector to a code is a finite set.

instance Code.instFintypeElemNNRatPossibleDistsToCodeRelHammingDistOfNonempty {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : Fintype ↑(possibleDistsToCode w C relHammingDist)

def Code.relHammingDistToCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (w : ι → F) (C : Set (ι → F)) : ℚ≥0

The relative Hamming distance from a vector to a code.

theorem Code.relHammingDistToCode.p {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (w : ι → F) (C : Set (ι → F)) (h : (possibleDistsToCode w C relHammingDist).Nonempty) : Option.isSome (distToCode w C relHammingDist ⋯) = true

def Code.«termδᵣ(_,_)_1» : Lean.ParserDescr

δᵣ(w,C) denotes the relative Hamming distance between a vector w and a code C.

@[simp]

theorem Code.zero_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] : 0 ∈ relHammingDistRange ι

@[simp]

theorem Code.relHammingDistToCode_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {c : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : δᵣ(c, C) ∈ relHammingDistRange ι

The relative Hamming distances between a vector and a codeword is in the range of the relative Hamming distance function.

def Code.wt {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] (v : ι → F) : ℕ

theorem Code.wt_eq_hammingNorm {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = ‖v‖₀

theorem Code.wt_eq_zero_iff {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = 0 ↔ Fintype.card ι = 0 ∨ ∀ (i : ι), v i = 0

def projection {n : Type u_1} {R : Type u_2} (S : Finset n) (w : n → R) : { x : n // x ∈ S } → R

theorem projection_injective {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (nontriv : ‖C‖₀ ≥ 1) (S : Finset n) (hS : Fintype.card { x : n // x ∈ S } = Fintype.card n - (‖C‖₀ - 1)) (u v : n → R) (hu : u ∈ C) (hv : v ∈ C) : projection S u = projection S v → u = v

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

@[reducible, inline]

abbrev LinearCode (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v)

noncomputable def LinearCode.fromRowGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [Fintype κ] [Semiring F] (G : Matrix κ ι F) : LinearCode ι F

Linear code defined by left multiplication by its generator matrix.

noncomputable def LinearCode.fromColGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [Fintype κ] [CommRing F] (G : Matrix ι κ F) : LinearCode ι F

Linear code defined by right multiplication by a generator matrix.

noncomputable def LinearCode.byCheckMatrix {F : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype κ] [CommRing F] (H : Matrix ι κ F) : LinearCode κ F

Define a linear code from its (parity) check matrix

noncomputable def LinearCode.disFromHammingNorm {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] [DecidableEq F] (LC : LinearCode ι F) : ℕ

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

theorem LinearCode.dist_eq_dist_from_HammingNorm {F : Type u_3} {ι : Type u_4} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : ‖LC.carrier‖₀ = LC.disFromHammingNorm

noncomputable def LinearCode.dim {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : ℕ

The dimension of a linear code.

theorem LinearCode.rank_eq_dim_fromColGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [Fintype κ] [CommRing F] {G : Matrix κ ι F} : G.rank = (fromColGenMat G).dim

The dimension of a linear code equals the rank of its associated generator matrix.

def LinearCode.length {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] : LinearCode ι F → ℕ

The length of a linear code.

noncomputable def LinearCode.rate {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : ℚ≥0

The rate of a linear code.

def LinearCode.termρ_ : Lean.ParserDescr

ρ LC is the rate of the linear code LC.

Uses & to make the notation non-reserved, allowing ρ to also be used as a variable name.

noncomputable def LinearCode.minWtCodewords {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : ℕ

The minimum taken over the weight of codewords in a linear code.

theorem LinearCode.hammingDist_eq_wt_sub {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] {u v : ι → F} : Δ₀(u, v) = Code.wt (u - v)

The Hamming distance between codewords equals to the weight of their difference.

theorem LinearCode.dist_eq_minWtCodewords {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] {LC : LinearCode ι F} : Code.minDist ↑LC = LC.minWtCodewords

The min distance of a linear code equals the minimum of the weights of non-zero codewords.

theorem LinearCode.dist_UB {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] {LC : LinearCode ι F} : Code.minDist ↑LC ≤ LC.length

noncomputable def LinearCode.restrictLinear {F : Type u_3} {ι : Type u_4} [Semiring F] (S : Finset ι) : (ι → F) →ₗ[F] { x : ι // x ∈ S } → F

theorem LinearCode.singletonBound {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] [StrongRankCondition F] (LC : LinearCode ι F) : LC.dim ≤ LC.length - Code.minDist ↑LC + 1

def LinearCode.interleaveCode {n : Type u_1} {F : Type u_3} [Semiring F] [DecidableEq F] (C : Submodule F (n → F)) (ι : Type u_5) : Submodule F (ι × n → F)

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

def LinearCode.«term_^⋈_» : Lean.TrailingParserDescr

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

Interleave two functions u v : α → β.

def LinearCode.«term_⋈_» : Lean.TrailingParserDescr

theorem LinearCode.singleton_bound_linear {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] [StrongRankCondition F] (LC : LinearCode ι F) : Module.finrank F ↥LC ≤ Fintype.card ι - ‖LC.carrier‖₀ + 1

Singleton bound for linear codes

def LinearCode.linearCodeDist' {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] [DecidableEq F] [Fintype F] [DecidableEq ι] (LC : LinearCode ι F) [DecidablePred fun (x : ι → F) => x ∈ LC] : ℕ∞

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

theorem poly_eq_zero_of_dist_lt {n k : ℕ} {F : Type u_3} [DecidableEq F] [CommRing F] [IsDomain F] {p : Polynomial F} {ωs : Fin n → F} (h_deg : p.natDegree < k) (hn : k ≤ n) (h_inj : Function.Injective ωs) (h_dist : Δ₀((fun (a : F) => Polynomial.eval a p) ∘ ωs, 0) < n - k + 1) : p = 0