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.

Naming conventions

1. suffix ': computable/instantiation of the corresponding mathematical generic definitions without such suffix (e.g. Δ₀'(u, C) vs Δ₀(u, C), δᵣ'(u, C) vs δᵣ(u, C), ...) - NOTE: The generic (non-suffixed) definitions (Δ₀, δᵣ, ...) are recommended to be used in generic security statements, and the suffixed definitions (Δ₀', δᵣ', ...) are used for proofs or in statements of lemmas that need smaller value range. - We usually prove the equality as a bridge from the suffixed definitions into the non-suffixed definitions (e.g. distFromCode'_eq_distFromCode, ...)

Main Definitions

1. Distance between two words: - hammingDist u v (Δ₀(u, v)): The Hamming distance between two words u and v - relHammingDist u v (δᵣ(u, v)): The relative Hamming distance between two words u and v
2. Distance of code: - dist C (‖"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.
   • minDist C: another statement of dist C using equality, we have dist_eq_minDist - dist' C (‖C‖₀'): A computable version of dist C, assuming C is a Fintype.
3. Distance from a word to a code: - distFromCode u C (Δ₀(u, C)): The hamming distance from a word u to a code C
   • distFromCode_of_empty: Δ₀(u, ∅) = ⊤
   • distFromCode_eq_top_iff_empty: Δ₀(u, C) = ⊤ ↔ C = ∅ - distFromCode' u C (Δ₀'(u, C)): A computable version of distFromCode u C, assuming C is a Fintype.
   • distFromCode'_eq_distFromCode: Δ₀'(u, C) = Δ₀(u, C) - relDistFromCode u C (δᵣ(u, C)): The relative Hamming distance from a word u to a code C
   • relDistFromCode' u C (δᵣ'(u, C)): A computable version of relDistFromCode u C, assuming C is a Fintype and C is non-empty.
   • relDistFromCode'_eq_relDistFromCode: δᵣ'(u, C) = δᵣ(u, C)
4. Switching between different distance realms: - relDistFromCode_eq_distFromCode_div: δᵣ(u, C) = Δ₀(u, C) / |ι| - pairDist_eq_distFromCode_iff_eq_relDistFromCode_div: Δ₀(u, v) = Δ₀(u, C) ↔ δᵣ(u, v) = δᵣ(u, C) - relDistFromCode_le_relDist_to_mem: δᵣ(u, C) ≤ δᵣ(u, v) - relCloseToCode_iff_relCloseToCodeword_of_minDist: δᵣ(u, C) ≤ δ ↔ ∃ v ∈ C, δᵣ(u, v) ≤ δ - pairRelDist_le_iff_pairDist_le: (δᵣ(u, v) ≤ δ) ↔ (Δ₀(u, v) ≤ Nat.floor (δ * Fintype.card ι)) - distFromCode_le_iff_relDistFromCode_le: Δ₀(u, C) ≤ e ↔ δᵣ(u, C) ≤ (e : ℝ≥0) / (Fintype.card ι : ℝ≥0) - relDistFromCode_le_iff_distFromCode_le: δᵣ(u, C) ≤ δ ↔ Δ₀(u, C) ≤ Nat.floor (δ * Fintype.card ι) - relCloseToWord_iff_exists_possibleDisagreeCols - relCloseToWord_iff_exists_agreementCols - relDist_floor_bound_iff_complement_bound - distFromCode_le_dist_to_mem: Δ₀(u, C) ≤ Δ₀(u, v), given v ∈ C - distFromCode_le_card_index_of_Nonempty: Δ₀(u, C) ≤ |ι|, given C is non-empty
5. Unique decoding radius: - uniqueDecodingRadius C (UDR(C)): The unique decoding radius of a code C - relativeUniqueDecodingRadius C (relUDR(C)): The relative unique decoding radius of a code C - UDR_close_iff_exists_unique_close_codeword: Δ₀(u, C) ≤ UDR(C) ↔ ∃! v ∈ C, Δ₀(u, v) ≤ UDR(C) - UDRClose_iff_two_mul_proximity_lt_d_UDR: e ≤ UDR(C) ↔ 2 * e < ‖C‖₀ - eq_of_le_uniqueDecodingRadius - UDR_close_iff_relURD_close: Δ₀(u, C) ≤ UDR(C) ↔ δᵣ(u, C) ≤ relUDR(C) - dist_le_UDR_iff_relDist_le_relUDR: e ≤ UDR(C) ↔ (e : ℝ≥0) / (Fintype.card ι : ℝ≥0) ≤ relUDR(C)

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

TODOs

• Implement ENNRat (ℚ≥0∞), for usage in relDistFromCode and relDistFromCode', as counterpart of ENat (ℕ∞) in distFromCode and distFromCode'.

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

theorem Code.distFromCode_le_dist_to_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) {C : Set (n → R)} (v : n → R) (hv : v ∈ C) : Δ₀(u, C) ≤ ↑Δ₀(u, v)

The distance to a code is at most the distance to any specific codeword.

theorem Code.pairDist_ge_code_mindist_of_ne {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) (h_ne : u ≠ v) : Δ₀(u, v) ≥ ‖C‖₀

If u and v are distinct members of a code C, their distance is at least ‖C‖₀.

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.dist_eq_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : ‖C‖₀ = minDist C

theorem Code.dist_pos_of_Nontrivial {ι : Type u_3} [Fintype ι] {F : Type u_4} (C : Set (ι → F)) [DecidableEq F] (hC : C.Nontrivial) : ‖C‖₀ > 0

A non-trivial code (a code with at least two distinct codewords) must have a minimum distance greater than 0.

theorem Code.exists_closest_codeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ∃ M ∈ C, ↑Δ₀(u, M) = Δ₀(u, C)

noncomputable def Code.pickClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ↑C

theorem Code.distFromPickClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : Δ₀(u, C) = ↑Δ₀(u, ↑(pickClosestCodeword_of_Nonempty_Code C u))

theorem Code.closeToWord_iff_exists_possibleDisagreeCols {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) (e : ℕ) : Δ₀(u, v) ≤ e ↔ ∃ (D : Finset ι), D.card ≤ e ∧ ∀ colIdx ∉ D, u colIdx = v colIdx

theorem Code.closeToWord_iff_exists_agreementCols {ι : Type u_3} [Fintype ι] [DecidableEq ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) (e : ℕ) : Δ₀(u, v) ≤ e ↔ ∃ (S : Finset ι), Fintype.card ι - e ≤ S.card ∧ ∀ (colIdx : ι), (colIdx ∈ S → u colIdx = v colIdx) ∧ (u colIdx ≠ v colIdx → colIdx ∉ S)

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 = ∅

theorem Code.distFromCode_le_card_index_of_Nonempty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) {C : Set (n → R)} [Nonempty ↑C] : Δ₀(u, C) ≤ ↑(Fintype.card n)

@[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

theorem Code.closeToCode_iff_closeToCodeword_of_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (e : ℕ) : Δ₀(u, C) ≤ ↑e ↔ ∃ v ∈ C, Δ₀(u, v) ≤ e

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.

theorem Code.possibleDistsToCode_nonempty_iff {α : Type u_6} {F : Type u_7} {ι : Type u_8} {w : ι → F} {C : Set (ι → F)} {δf : (ι → F) → (ι → F) → α} : (possibleDistsToCode w C δf).Nonempty ↔ (C \ {w}).Nonempty

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 finite code C.

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

theorem Code.distFromCode'_eq_distFromCode {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] (u : n → R) : Δ₀'(u, C) = Δ₀(u, C)

For finite nonempty codes, the computable distance equals the noncomputable distance.

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.

noncomputable def Code.relDistFromCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u : ι → F) (C : Set (ι → F)) : ENNReal

The relative Hamming distance from a vector to a code, defined as the infimum of all relative distances from u to codewords in C. The type is ENNReal (ℝ≥0∞) to correctly handle the case C = ∅. For case of Nonempty C, we can use relDistFromCode (δᵣ') for smaller value range in ℚ≥0, which is equal to this definition.

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

δᵣ(u,C) denotes the relative distance from u to C. This is the main standard definition used in statements. The NNRat version of it is δᵣ'(u, C).

theorem Code.relDistFromCode_le_relDist_to_mem {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u : ι → F) {C : Set (ι → F)} (v : ι → F) (hv : v ∈ C) : δᵣ(u, C) ≤ ↑δᵣ(u, v)

The relative distance to a code is at most the relative distance to any specific codeword.

@[simp]

theorem Code.relDistFromCode_of_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) : δᵣ(u, ∅) = ⊤

theorem Code.exists_relClosest_codeword_of_Nonempty_Code {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ∃ M ∈ C, ↑δᵣ(u, M) = δᵣ(u, C)

This follows proof strategy from exists_closest_codeword_of_Nonempty_Code. However, it's NOT used to construct pickRelClosestCodeword_of_Nonempty_Code.

theorem Code.relDistFromCode_eq_distFromCode_div {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (u : ι → F) (C : Set (ι → F)) : δᵣ(u, C) = ↑Δ₀(u, C) / ↑(Fintype.card ι)

theorem Code.pairDist_eq_distFromCode_iff_eq_relDistFromCode_div {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (u v : ι → F) (C : Set (ι → F)) [Nonempty ↑C] : ↑Δ₀(u, v) = Δ₀(u, C) ↔ ↑δᵣ(u, v) = δᵣ(u, C)

noncomputable def Code.pickRelClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ↑C

Note that this gives the same codeword as pickClosestCodeword_of_Nonempty_Code.

theorem Code.relDistFromPickRelClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : δᵣ(u, C) = ↑δᵣ(u, ↑(pickRelClosestCodeword_of_Nonempty_Code C u))

theorem Code.relCloseToCode_iff_relCloseToCodeword_of_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (δ : NNReal) : δᵣ(u, C) ≤ ↑δ ↔ ∃ v ∈ C, ↑δᵣ(u, v) ≤ δ

Relative distance version of closeToCode_iff_closeToCodeword_of_minDist. If the distance to a code is at most δ, then there exists a codeword within distance δ. NOTE: can we make this shorter using relDistFromCode_eq_distFromCode_div?

theorem Code.pairRelDist_le_iff_pairDist_le {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ Δ₀(u, v) ≤ ⌊δ * ↑(Fintype.card ι)⌋₊

Equivalence between relative and natural distance bounds.

theorem Code.distFromCode_le_iff_relDistFromCode_le {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] {C : Set (ι → F)} [Nonempty ι] (u : ι → F) (e : ℕ) : Δ₀(u, C) ≤ ↑e ↔ δᵣ(u, C) ≤ ↑↑e / ↑↑(Fintype.card ι)

A word u is close to a code C within an absolute error bound e if and only if it is close within the equivalent relative error bound e / n.

theorem Code.relDistFromCode_le_iff_distFromCode_le {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (δ : NNReal) : δᵣ(u, C) ≤ ↑δ ↔ Δ₀(u, C) ≤ ↑⌊δ * ↑(Fintype.card ι)⌋₊

A word u is relatively close to a code C within an relative error bound δ if and only if it is relatively close within the equivalent absolute error bound ⌊δ * n⌋.

theorem Code.relCloseToWord_iff_exists_possibleDisagreeCols {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (u v : ι → F) (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ ∃ (D : Finset ι), D.card ≤ ⌊δ * ↑(Fintype.card ι)⌋₊ ∧ ∀ colIdx ∉ D, u colIdx = v colIdx

theorem Code.relCloseToWord_iff_exists_agreementCols {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (u v : ι → F) (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ ∃ (S : Finset ι), Fintype.card ι - ⌊δ * ↑(Fintype.card ι)⌋₊ ≤ S.card ∧ ∀ (colIdx : ι), (colIdx ∈ S → u colIdx = v colIdx) ∧ (u colIdx ≠ v colIdx → colIdx ∉ S)

theorem Code.NNReal.floor_ge_Nat_of_gt {r : NNReal} {n : ℕ} (h : r > ↑n) : ⌊r⌋₊ ≥ n

theorem Code.NNReal.sub_eq_zero_of_le (x y : NNReal) (h : x ≤ y) : x - y = 0

theorem Code.relDist_floor_bound_iff_complement_bound (n upperBound : ℕ) (δ : NNReal) : n - ⌊δ * ↑n⌋₊ ≤ upperBound ↔ (1 - δ) * ↑n ≤ ↑upperBound

The equivalence between the two lowerbound of upperBound in Nat and NNReal context. In which, upperBound is viewed as the size of an agreement set S (e.g. between two words, or between a word to a code, ...). Specifically, n - ⌊δ * n⌋ ≤ (upperBound : ℕ) ↔ (1 - δ) * n ≤ (upperBound : ℝ≥0). This lemma is useful for jumping back-and-forth between absolute distance and relative distance realms, especially when we work with an agreement set. For example, it can be used after simping with closeToWord_iff_exists_agreementCols and relCloseToWord_iff_exists_agreementCols.

@[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.relDistFromCode' {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (w : ι → F) (C : Set (ι → F)) [Fintype ↑C] [Nonempty ↑C] : ℚ≥0

Computable version of the relative Hamming distance from a vector w to a finite non-empty code C. This one is intended to mimic the definition of distFromCode'. However, we don't have ENNRat (ℚ≥0∞) (as counterpart of ENat (ℕ∞) in distFromCode') so we require [Nonempty C]. TODO: define ENNRat (ℚ≥0∞) so we can migrate both relDistFromCode and relDistFromCode' to ℚ≥0∞

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

δᵣ'(w,C) denotes the relative Hamming distance between a vector w and a code C. This is a different statement of the generic definition δᵣ(w,C).

theorem Code.relDistFromCode'_eq_relDistFromCode {ι : Type u_5} [Fintype ι] [Nonempty ι] [DecidableEq ι] {F : Type u_6} [DecidableEq F] (w : ι → F) (C : Set (ι → F)) [Fintype ↑C] [Nonempty ↑C] : δᵣ(w, C) = ↑δᵣ'(w, C)

@[simp]

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

noncomputable def Code.uniqueDecodingRadius {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) : ℕ

The unique decoding radius: ≤ ⌊(d-1)/2⌋ for any code C.

def Code.UDR {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) : ℕ

Alias of Code.uniqueDecodingRadius.

---

The unique decoding radius: ≤ ⌊(d-1)/2⌋ for any code C.

noncomputable def Code.relativeUniqueDecodingRadius {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) : NNReal

The relative unique decoding radius, obtained from the absolute radius by normalizing with the block length. This also works with ≤.

def Code.relUDR {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) : NNReal

Alias of Code.relativeUniqueDecodingRadius.

---

The relative unique decoding radius, obtained from the absolute radius by normalizing with the block length. This also works with ≤.

@[simp]

theorem Code.uniqueDecodingRadius_eq_floor_div_2 {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) : uniqueDecodingRadius C = ⌊(↑‖C‖₀ - 1) / 2⌋₊

theorem Code.UDRClose_iff_two_mul_proximity_lt_d_UDR {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) [NeZero ‖C‖₀] {e : ℕ} : e ≤ uniqueDecodingRadius C ↔ 2 * e < ‖C‖₀

Given an error/proximity parameter e within the unique decoding radius of a code C where ‖C‖₀ > 0, this lemma proves the standard bound 2 * e < d (i.e. condition of Code.eq_of_lt_dist).

theorem Code.eq_of_le_uniqueDecodingRadius {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) (u : ι → F) {v w : ι → F} (hv : v ∈ C) (hw : w ∈ C) (huv : Δ₀(u, v) ≤ uniqueDecodingRadius C) (huw : Δ₀(u, w) ≤ uniqueDecodingRadius C) : v = w

A stronger version of distFromCode_eq_of_lt_half_dist: If two codewords v and w are both within the uniqueDecodingRadius of u (i.e. 2 * Δ₀(u, v) < ‖C‖₀ and 2 * Δ₀(u, w) < ‖C‖₀), then they must be equal.

theorem Code.UDR_close_iff_exists_unique_close_codeword {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : Δ₀(u, C) ≤ ↑(uniqueDecodingRadius C) ↔ ∃! v : ι → F, v ∈ C ∧ Δ₀(u, v) ≤ uniqueDecodingRadius C

A word u is within the uniqueDecodingRadius of a code C if and only if there exists exactly one codeword v in C that is that close.

theorem Code.UDR_close_iff_relURD_close {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) (u : ι → F) : Δ₀(u, C) ≤ ↑(uniqueDecodingRadius C) ↔ δᵣ(u, C) ≤ ↑(relativeUniqueDecodingRadius C)

A word u is close to a code C within the absolute unique decoding radius if and only if it is close within the relative unique decoding radius.

@[simp]

theorem Code.dist_le_UDR_iff_relDist_le_relUDR {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) (e : ℕ) : e ≤ uniqueDecodingRadius C ↔ ↑e / ↑(Fintype.card ι) ≤ relativeUniqueDecodingRadius C

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

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

theorem Code.wt_eq_zero_iff {F : Type u_5} [DecidableEq F] {ι : Type u_6} [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 ModuleCode (ι : Type u) (F : Type v) [Semiring F] (A : Type w) [AddCommMonoid A] [Module F A] : Type (max u w)

A ModuleCode ι F A is an F-linear code of length indexed by ι over the alphabet A, defined as an F-submodule of ι → A.

@[reducible, inline]

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

theorem LinearCode_is_ModuleCode {ι : Type u} [Fintype ι] {F : Type v} [Semiring F] : LinearCode ι F = ModuleCode ι F F

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

Module code defined by left multiplication by its generator matrix. For a matrix G : Matrix κ ι F (over field F) and module A over F, this generates the F-submodule of (ι → A) spanned by the rows of G acting on (κ → A). The matrix acts on vectors v : κ → A by: (G • v)(i) = ∑ k, G k i • v k where G k i : F is the scalar and v k : A is the module element.

noncomputable def LinearCode.fromColGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [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_5} {κ : Type u_6} [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_5} [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_5} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : ‖LC.carrier‖₀ = LC.disFromHammingNorm

noncomputable def LinearCode.dim {F : Type u_3} {ι : Type u_5} [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) : ℕ

The dimension of a linear code.

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

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

def LinearCode.length {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] : ModuleCode ι F A → ℕ

The length of a linear code.

noncomputable def LinearCode.rate {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] {A : Type u_7} [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) : ℚ≥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} {ι : Type u_4} [Fintype ι] {A : Type u_5} [AddCommMonoid A] [DecidableEq A] [Semiring F] [Module F A] (MC : ModuleCode ι F A) : ℕ

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 ι] [AddCommGroup 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} {ι : Type u_4} [Fintype ι] [Ring F] {A : Type u_6} [DecidableEq A] [AddCommGroup A] [Module F A] {MC : ModuleCode ι F A} : Code.minDist ↑MC = minWtCodewords MC

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} {ι : Type u_4} [Fintype ι] [Ring F] {A : Type u_6} [DecidableEq A] [AddCommGroup A] [Module F A] {MC : ModuleCode ι F A} : Code.minDist ↑MC ≤ length MC

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

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

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.moduleCodeDist' {F : Type u_3} {A : Type u_4} {ι : Type u_5} [Fintype ι] [Semiring F] [Fintype A] [DecidableEq ι] [DecidableEq A] [AddCommMonoid A] [Module F A] (MC : ModuleCode ι F A) [DecidablePred fun (x : ι → A) => x ∈ MC] : ℕ∞

A computable version of the Hamming distance of a module code MC.

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