Reed–Muller codes

The Reed–Muller code of degree d in m variables over a finite field F with q elements consists of the evaluation tables on Fin m → F of the polynomials of total degree at most d (Cslib.Code.reedMuller) [Ree54], [Mul54], [GRS19]. By the Schwartz–Zippel lemma MvPolynomial.schwartz_zippel_totalDegree, a nonzero polynomial of total degree at most d vanishes on at most a d / q fraction of the points, so two distinct codewords differ on at least a 1 - d / q fraction of the q ^ m points (Cslib.Code.card_sub_mul_pow_le_mul_hammingDist_of_mem_reedMuller). For d < q this is exact: the product of X 0 - t over d field elements t vanishes exactly where the first coordinate is one of them, so in m + 1 variables the minimum distance is (q - d) * q ^ m (Cslib.Code.minDist_reedMuller). For d ≥ q the bound says nothing; in particular the binary Reed–Muller codes of degree at least two, whose distance comes from multilinear polynomials, are not covered by it.

Main definitions

• Cslib.Code.reedMuller: the Reed–Muller code.

Main results

• Cslib.Code.mem_reedMuller: the codewords are the evaluation tables of polynomials of total degree at most d.
• Cslib.Code.card_sub_mul_pow_le_mul_hammingNorm_of_mem_reedMuller, Cslib.Code.card_sub_mul_pow_le_mul_hammingDist_of_mem_reedMuller: the Schwartz–Zippel distance bound.
• Cslib.Code.le_minDist_reedMuller: the minimum distance in m + 1 variables is at least (q - d) * q ^ m.
• Cslib.Code.minDist_reedMuller: for d < q the minimum distance in m + 1 variables is (q - d) * q ^ m.

References

• I. S. Reed, A class of multiple-error-correcting codes and the decoding scheme
• D. E. Muller, Application of Boolean algebra to switching circuit design and to error detection
• [V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory] [GRS19]

noncomputable def Cslib.Code.reedMuller (F : Type u_1) [Field F] (m d : ℕ) : Submodule F ((Fin m → F) → F)

The Reed–Muller code of degree d in m variables: the evaluation tables on Fin m → F of the polynomials of total degree at most d.

theorem Cslib.Code.mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} {f : (Fin m → F) → F} : f ∈ reedMuller F m d ↔ ∃ (P : MvPolynomial (Fin m) F), P.totalDegree ≤ d ∧ (fun (x : Fin m → F) => (MvPolynomial.eval x) P) = f

A word is a codeword of the Reed–Muller code of degree d exactly when it is the evaluation table of a polynomial of total degree at most d.

theorem Cslib.Code.eval_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} {P : MvPolynomial (Fin m) F} (hP : P.totalDegree ≤ d) : (fun (x : Fin m → F) => (MvPolynomial.eval x) P) ∈ reedMuller F m d

The evaluation table of a polynomial of total degree at most d is a codeword of the Reed–Muller code of degree d.

theorem Cslib.Code.card_sub_mul_pow_le_mul_hammingNorm_of_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} [Fintype F] [DecidableEq F] {f : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (hf0 : f ≠ 0) : (Fintype.card F - d) * Fintype.card F ^ m ≤ Fintype.card F * hammingNorm f

Schwartz–Zippel distance. A nonzero codeword of the Reed–Muller code of degree d in m variables over a field with q elements is nonzero on at least a 1 - d / q fraction of the q ^ m points: (q - d) * q ^ m ≤ q * hammingNorm f.

theorem Cslib.Code.card_sub_mul_pow_le_mul_hammingDist_of_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} [Fintype F] [DecidableEq F] {f g : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (hg : g ∈ reedMuller F m d) (hfg : f ≠ g) : (Fintype.card F - d) * Fintype.card F ^ m ≤ Fintype.card F * hammingDist f g

Schwartz–Zippel distance. Two distinct codewords of the Reed–Muller code of degree d in m variables over a field with q elements differ on at least a 1 - d / q fraction of the q ^ m points: (q - d) * q ^ m ≤ q * hammingDist f g.

theorem Cslib.Code.le_minDist_reedMuller {F : Type u_1} [Field F] {m d : ℕ} [Fintype F] [DecidableEq F] : ↑((Fintype.card F - d) * Fintype.card F ^ m) ≤ minDist ↑(reedMuller F (m + 1) d)

The Reed–Muller code of degree d in m + 1 variables over a field with q elements has minimum distance at least (q - d) * q ^ m.

theorem Cslib.Code.minDist_reedMuller {F : Type u_1} [Field F] {m d : ℕ} [Fintype F] [DecidableEq F] (hd : d < Fintype.card F) : minDist ↑(reedMuller F (m + 1) d) = ↑((Fintype.card F - d) * Fintype.card F ^ m)

The distance of Reed–Muller codes. For d < q, the Reed–Muller code of degree d in m + 1 variables over a field with q elements has minimum distance exactly (q - d) * q ^ m.