Linear-Code Constructions and Bounds

This module contains weight/projection lemmas, the singleton bound for arbitrary and linear codes, and basic constructions and dimension/rate facts for linear codes.

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) : ↥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 ↥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] ↥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 (x : F) => Polynomial.eval x p) ∘ ωs, 0) < n - k + 1) : p = 0