Documentation

TauCeti.InformationTheory.Coding.Elementary.Basic

Repetition and single-parity-check codes #

The repetition code consists of constant words, and the single-parity-check code consists of words whose coordinate sum is zero. They are Euclidean duals. A positive-length repetition code has as many words as its alphabet; at length zero it has only one word. Over a finite field with q elements, the parity-check code has q^(n - 1) words at length n, including length zero, where the natural-number subtraction gives exponent zero.

Their weight enumerators are computed in TauCeti.InformationTheory.Coding.Elementary.WeightEnumerator.

References #

W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §§1.2–1.4.

source
def TauCeti.repetitionCode (R : Type u_1) (ι : Type u_2) [Semiring R] :
Submodule R (ι → R)

The repetition code is the submodule of constant words.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_repetitionCode (R : Type u_1) (ι : Type u_2) [Semiring R] {x : ι → R} :
    x ∈ repetitionCode R ι ↔ ∃ (a : R), Function.const ι a = x

    Membership in the repetition code means being constant.

    source
    def TauCeti.singleParityCheckCode (R : Type u_1) (ι : Type u_2) [Semiring R] [Fintype ι] :
    Submodule R (ι → R)

    The single-parity-check code is the kernel of the coordinate-sum map.

    Instances For
      source
      @[simp]
      theorem TauCeti.mem_singleParityCheckCode (R : Type u_1) (ι : Type u_2) [Semiring R] [Fintype ι] {x : ι → R} :
      x ∈ singleParityCheckCode R ι ↔ ∑ i : ι, x i = 0

      Membership in the single-parity-check code means having coordinate sum zero.

      source
      @[simp]
      theorem TauCeti.euclideanDual_repetitionCode (R : Type u_1) (ι : Type u_2) [CommSemiring R] [Fintype ι] :
      (repetitionCode R ι).euclideanDual = singleParityCheckCode R ι

      The dual of the repetition code is the single-parity-check code.

      source
      @[simp]
      theorem TauCeti.euclideanDual_singleParityCheckCode (R : Type u_1) (ι : Type u_2) [Field R] [Fintype ι] :
      (singleParityCheckCode R ι).euclideanDual = repetitionCode R ι

      The dual of the single-parity-check code over a field is the repetition code.

      source
      @[simp]
      theorem TauCeti.repetitionCode_eq_bot_of_isEmpty (R : Type u_1) (ι : Type u_2) [Semiring R] [IsEmpty ι] :
      repetitionCode R ι = ⊥

      With no coordinates, the repetition code is zero.

      source
      @[simp]
      theorem TauCeti.singleParityCheckCode_eq_top_of_isEmpty (R : Type u_1) (ι : Type u_2) [Semiring R] [Fintype ι] [IsEmpty ι] :
      singleParityCheckCode R ι = ⊤

      With no coordinates, the parity-check code is the whole word space.

      source
      @[simp]
      theorem TauCeti.natCard_repetitionCode (R : Type u_1) (ι : Type u_2) [Semiring R] [Nonempty ι] :
      Nat.card ↥(repetitionCode R ι) = Nat.card R

      A positive-length repetition code has as many words as its alphabet.

      source
      @[simp]
      theorem TauCeti.natCard_singleParityCheckCode (R : Type u_1) (ι : Type u_2) [Field R] [Finite R] [Fintype ι] :
      Nat.card ↥(singleParityCheckCode R ι) = Nat.card R ^ (Fintype.card ι - 1)

      Over a finite field, the parity-check code has q^(n - 1) words, including at length zero.