Error-Correcting Codes — 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 ErrorCorrectingCodes.Codeword (n : ℕ) (α : Type u_2) [Fintype α] [DecidableEq α] : Type u_2

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

Equations

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

def ErrorCorrectingCodes.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 ErrorCorrectingCodes.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 ErrorCorrectingCodes.Codeword.zero {α : Type u_1} [Fintype α] [DecidableEq α] [Field α] {n : ℕ} : Codeword n α

The all-zeros codeword.

Equations

• ErrorCorrectingCodes.Codeword.zero x✝ = 0

@[reducible, inline]

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

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

Equations

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

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

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

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

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

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

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

theorem ErrorCorrectingCodes.Codeword.natCast_pos_of_two_le {q : ℕ} (hq : 2 ≤ q) : 0 < ↑q

If q ≥ 2, then q is positive as a real number.

theorem ErrorCorrectingCodes.Codeword.natCast_one_lt_of_two_le {q : ℕ} (hq : 2 ≤ q) : 1 < ↑q

If q ≥ 2, then q > 1 as a real number.

theorem ErrorCorrectingCodes.Codeword.natCast_sub_one_nonneg_of_two_le {q : ℕ} (hq : 2 ≤ q) : 0 ≤ ↑q - 1

If q ≥ 2, then q - 1 is nonnegative as a real number.

theorem ErrorCorrectingCodes.Codeword.natCast_sub_one_pos_of_two_le {q : ℕ} (hq : 2 ≤ q) : 0 < ↑q - 1

If q ≥ 2, then q - 1 is positive as a real number.

theorem ErrorCorrectingCodes.Codeword.natCast_ne_one_of_two_le {q : ℕ} (hq : 2 ≤ q) : ↑q ≠ 1

If q ≥ 2, then q ≠ 1 as a real number.

theorem ErrorCorrectingCodes.Codeword.one_sub_pos_of_lt_one {p : ℝ} (hp : p < 1) : 0 < 1 - p

If p < 1, then 1 - p is positive.

theorem ErrorCorrectingCodes.Codeword.one_sub_nonneg_of_le_one {p : ℝ} (hp : p ≤ 1) : 0 ≤ 1 - p

If p ≤ 1, then 1 - p is nonnegative.

theorem ErrorCorrectingCodes.Codeword.mul_one_sub_pos {p : ℝ} (hp : 0 < p) (hp' : p < 1) : 0 < p * (1 - p)

If 0 < p < 1, then p (1 - p) is positive.

theorem ErrorCorrectingCodes.Codeword.lt_one_of_le_one_sub_inv {q p : ℝ} (hq : 0 < q) (hp : p ≤ 1 - 1 / q) : p < 1

If q > 0 and p ≤ 1 - 1/q, then p < 1.

theorem ErrorCorrectingCodes.Codeword.one_sub_pos_of_le_one_sub_inv {q p : ℝ} (hq : 0 < q) (hp : p ≤ 1 - 1 / q) : 0 < 1 - p

If q > 0 and p ≤ 1 - 1/q, then 1 - p is positive.

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

• ErrorCorrectingCodes.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 ErrorCorrectingCodes.Codeword.rate {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (C : Code n α) : ℝ

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

Equations

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

def ErrorCorrectingCodes.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 ErrorCorrectingCodes.Codeword.zero

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

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