Reed–Solomon codes

The Reed–Solomon code with degree bound k and evaluation points α : ι → F in a field F consists of the words i ↦ p (α i) of values of the polynomials p of degree less than k (Cslib.Code.reedSolomon) [RS60], [GRS19], MacWilliams and Sloane, Chapter 10. It is a linear code of length n = |ι|. When the points are distinct, a nonzero polynomial of degree less than k vanishes at fewer than k of them, so a nonzero codeword has weight at least n - k + 1 (Cslib.Code.le_hammingNorm_of_mem_reedSolomon); the product of X - α i over k - 1 of the points shows that this is attained, so for 1 ≤ k ≤ n the minimum distance is exactly n - k + 1 (Cslib.Code.minDist_reedSolomon). For k ≤ n the polynomials of degree less than k are determined by their values, so the code has dimension k (Cslib.Code.finrank_reedSolomon). Dimension plus minimum distance is n + 1: Reed–Solomon codes meet the Singleton bound Cslib.Code.finrank_add_le_card_add_one with equality.

Main definitions

• Cslib.Code.reedSolomon: the Reed–Solomon code.

Main results

• Cslib.Code.mem_reedSolomon: the codewords are the evaluations of polynomials of degree less than k.
• Cslib.Code.le_hammingNorm_of_mem_reedSolomon, Cslib.Code.le_minDist_reedSolomon: nonzero codewords have weight at least n - k + 1.
• Cslib.Code.minDist_reedSolomon: the minimum distance is n - k + 1.
• Cslib.Code.finrank_reedSolomon: with distinct points and k ≤ n, the dimension is k.

References

• I. S. Reed, G. Solomon, Polynomial codes over certain finite fields
• [V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory] [GRS19]
• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

noncomputable def Cslib.Code.reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] (α : ι → F) (k : ℕ) : Submodule F (ι → F)

The Reed–Solomon code with degree bound k and evaluation points α: the words i ↦ p (α i) for the polynomials p of degree less than k. The points are usually distinct.

theorem Cslib.Code.mem_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {α : ι → F} {k : ℕ} {w : ι → F} : w ∈ reedSolomon α k ↔ ∃ (p : Polynomial F), p.degree < ↑k ∧ (fun (i : ι) => Polynomial.eval (α i) p) = w

A word is a codeword of reedSolomon α k exactly when it is i ↦ p (α i) for a polynomial p of degree less than k.

theorem Cslib.Code.eval_mem_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {k : ℕ} (α : ι → F) {p : Polynomial F} (hp : p.degree < ↑k) : (fun (i : ι) => Polynomial.eval (α i) p) ∈ reedSolomon α k

The values i ↦ p (α i) of a polynomial p of degree less than k form a codeword of reedSolomon α k.

theorem Cslib.Code.le_hammingNorm_of_mem_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {α : ι → F} {k : ℕ} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) {w : ι → F} (hw : w ∈ reedSolomon α k) (hw0 : w ≠ 0) : Fintype.card ι - k + 1 ≤ hammingNorm w

With distinct points, a nonzero codeword of the Reed–Solomon code with degree bound k has weight at least n - k + 1.

theorem Cslib.Code.le_minDist_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {α : ι → F} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (k : ℕ) : ↑(Fintype.card ι - k + 1) ≤ minDist ↑(reedSolomon α k)

With distinct points, the Reed–Solomon code with degree bound k has minimum distance at least n - k + 1.

theorem Cslib.Code.minDist_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {α : ι → F} {k : ℕ} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hk : 1 ≤ k) (hkn : k ≤ Fintype.card ι) : minDist ↑(reedSolomon α k) = ↑(Fintype.card ι - k + 1)

The distance of Reed–Solomon codes. With distinct points, the Reed–Solomon code with degree bound 1 ≤ k ≤ n has minimum distance exactly n - k + 1.

theorem Cslib.Code.finrank_reedSolomon {F : Type u_1} {ι : Type u_2} [Field F] {α : ι → F} {k : ℕ} [Fintype ι] (hα : Function.Injective α) (hkn : k ≤ Fintype.card ι) : Module.finrank F ↥(reedSolomon α k) = k

With distinct points, the Reed–Solomon code with degree bound k ≤ n has dimension k.