Coding Theory — Core Definitions

This file provides the foundational definitions for coding theory over a finite alphabet α.

Main Definitions

• Codeword n α : a vector of length n over alphabet α, i.e. Fin n → α.
• Code n α : a code of block-length n over α, i.e. a Finset (Codeword n α).
• Linear_Code C G : predicate asserting that C is the image of the linear map given by generator matrix G.
• Linear_Code' C m : existential variant — C is the image of some n×m generator matrix.
• qaryEntropy q p : the q-ary entropy function H_q(p).
• hamming_distance c₁ c₂ : Hamming distance between two codewords.
• distance C d : predicate asserting that d is the minimum distance of code C.
• rate C : the rate of code C (base-|α| logarithm of |C| over block length).
• weight c : Hamming weight of a codeword c.
• hamming_ball l c : the Hamming ball of radius l centred at c.

Main Results

• dist_le_length : the minimum distance of a code is at most its block length.

@[reducible, inline]

abbrev CodingTheory.Codeword (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Type u_2

A codeword of block-length n over alphabet α. Concretely, a function Fin n → α.

Equations

• CodingTheory.Codeword n α = (Fin n → α)

def CodingTheory.Codeword.add {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c₁ c₂ : Codeword n α) : Codeword n α

Pointwise addition of two codewords.

Equations

• c₁.add c₂ i = c₁ i + c₂ i

def CodingTheory.Codeword.sub {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c₁ c₂ : Codeword n α) : Codeword n α

Pointwise subtraction of two codewords.

Equations

• c₁.sub c₂ i = c₁ i - c₂ i

def CodingTheory.Codeword.zero {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} : Codeword n α

The all-zeros codeword.

Equations

• CodingTheory.Codeword.zero x✝ = 0

@[reducible, inline]

abbrev CodingTheory.Codeword.Code (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Type u_2

A code of block-length n over α: a finite set of codewords.

Equations

• CodingTheory.Codeword.Code n α = Finset (CodingTheory.Codeword n α)

def CodingTheory.Codeword.Linear_Code {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n m : ℕ} (C : Code n α) (G : Matrix (Fin n) (Fin m) α) : Prop

A code C is linear with generator matrix G : Fin n × Fin m → α if C is exactly the image of the linear map G · -.

Equations

• CodingTheory.Codeword.Linear_Code C G = ((∀ (c' : CodingTheory.Codeword m α), G.mulVec c' ∈ C) ∧ ∀ c ∈ C, ∃ (c' : CodingTheory.Codeword m α), c = G.mulVec c')

def CodingTheory.Codeword.Linear_Code' {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (C : Code n α) (m : ℕ) : Prop

Existential variant of Linear_Code: C is the image of some n×m generator matrix.

Equations

• CodingTheory.Codeword.Linear_Code' C m = ∃ (G : Matrix (Fin n) (Fin m) α), (∀ (c' : CodingTheory.Codeword m α), G.mulVec c' ∈ C) ∧ ∀ c ∈ C, ∃ (c' : CodingTheory.Codeword m α), c = G.mulVec c'

noncomputable def CodingTheory.Codeword.qaryEntropy (q : ℕ) (p : ℝ) : ℝ

The q-ary entropy function H_q(p) = p·log_q(q-1) - p·log_q(p) - (1-p)·log_q(1-p).

Equations

• CodingTheory.Codeword.qaryEntropy q p = p * Real.logb (↑q) (↑q - 1) - p * Real.logb (↑q) p - (1 - p) * Real.logb (↑q) (1 - p)

def CodingTheory.Codeword.hamming_distance {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (c1 c2 : Codeword n α) : ℕ

The Hamming distance between two codewords.

Equations

• c1.hamming_distance c2 = hammingDist c1 c2

def CodingTheory.Codeword.distance {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (C : Code n α) (d : ℕ) : Prop

distance C d holds when d is the minimum Hamming distance of code C: there exist two distinct codewords at distance exactly d, and no two distinct codewords are closer.

Equations

• CodingTheory.Codeword.distance C d = ((∃ x ∈ C, ∃ y ∈ C, x ≠ y ∧ x.hamming_distance y = d) ∧ ∀ z ∈ C, ∀ w ∈ C, z ≠ w → z.hamming_distance w ≥ d)

noncomputable def CodingTheory.Codeword.rate {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (C : Code n α) : ℝ

The rate of a code: log_{|α|}(|C|) / n.

Equations

• CodingTheory.Codeword.rate C = Real.log ↑(Finset.card C) / (↑n * Real.log ↑(Fintype.card α))

def CodingTheory.Codeword.weight {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} (c : Codeword n α) : ℕ

The Hamming weight of a codeword: its distance from the all-zeros word.

Equations

• c.weight = c.hamming_distance CodingTheory.Codeword.zero

def CodingTheory.Codeword.max_size {α : Type u_1} [Fintype α] [DecidableEq α] (n d A : ℕ) : Prop

max_size n d A asserts that A is the maximum size of any code of block-length n and minimum distance d.

Equations

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

theorem CodingTheory.Codeword.dist_le_length {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n : ℕ} (C : Code n α) (d : ℕ) (h : distance C d) : d ≤ n

The minimum distance of a code is at most the block length.

def CodingTheory.Codeword.hamming_ball {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (l : ℕ) (c : Codeword n α) : Finset (Codeword n α)

The Hamming ball of radius l centred at codeword c: the set of codewords within Hamming distance l of c.

Equations

• CodingTheory.Codeword.hamming_ball l c = {c' : CodingTheory.Codeword n α | c'.hamming_distance c ≤ l}.toFinset