Sudan interpolants of least Y-degree by elimination

Sudan's list decoder [Sud97] for the Reed–Solomon code of dimension d + 1 needs a nonzero bivariate polynomial Q(X, Y) of (1, d)-weighted degree at most D vanishing at the points (α i, w i) of a received word (Cslib.Code.Sudan.IsInterpolant). This module computes one by linear algebra, choosing an interpolant of least Y-degree: for j = 0, 1, …, D / d it finds a kernel vector of the interpolation matrix restricted to the monomials of Y-degree at most j (Cslib.LinearAlgebra.kernelVec), and takes the first nonzero one (Cslib.Code.Sudan.interpolant). When there are more monomials than points this is an interpolant (Cslib.Code.Sudan.isInterpolant_interpolant), and no interpolant has smaller Y-degree (Cslib.Code.Sudan.natDegree_interpolant_le).

Least Y-degree makes every polynomial P of degree at most d with more than D agreements a simple root of Q, viewed as a polynomial in Y: if (Y - P)² divided Q, then Q / (Y - P) would be an interpolant of smaller Y-degree. On division by Y - P the bound D on the weighted degree drops to D - d (Cslib.Code.Sudan.add_mul_add_one_le_of_mul, an upper bound), so Q = (Y - P) * S where S(X, P(X)) is a nonzero polynomial of degree at most D - d (Cslib.Code.Sudan.exists_eq_mul_eval_ne_zero). Simplicity is what lets the root P be lifted from a single known value by Newton iteration (Cslib.Code.henselValue_eq).

Main definitions

• Cslib.Code.Sudan.monomialsUpTo: the monomials of bounded weighted degree and bounded Y-degree.
• Cslib.Code.Sudan.interpMatrix: the interpolation matrix on a set of monomials.
• Cslib.Code.Sudan.coeffsOf: the coefficients on a set of monomials given by a vector indexed by its enumeration.
• Cslib.Code.Sudan.kernelVecUpTo: the kernel vector of the interpolation matrix on the monomials of Y-degree at most j.
• Cslib.Code.Sudan.interpolantCoeffs: the coefficients of the first nonzero kernel vector.
• Cslib.Code.Sudan.interpolant: an interpolant of least Y-degree, by elimination.

Main results

• Cslib.Code.Sudan.isInterpolant_interpolant: it is an interpolant.
• Cslib.Code.Sudan.natDegree_interpolant_le: it has least Y-degree.
• Cslib.Code.Sudan.add_mul_add_one_le_of_mul: division by Y - P lowers the weighted degree by d.
• Cslib.Code.Sudan.exists_eq_mul_eval_ne_zero: polynomials with large agreement are simple roots of an interpolant of least Y-degree.

References

• M. Sudan, Decoding of Reed Solomon codes beyond the error-correction bound
• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]

Bivariate polynomials from coefficients

theorem Cslib.Code.Sudan.bivariateOf_congr {F : Type u_1} [Field F] {M : Finset (ℕ × ℕ)} {c c' : ℕ × ℕ → F} (h : ∀ m ∈ M, c m = c' m) : bivariateOf M c = bivariateOf M c'

bivariateOf M c depends only on the values of c on M.

theorem Cslib.Code.Sudan.eq_bivariateOf {F : Type u_1} [Field F] {Q : Polynomial (Polynomial F)} {M : Finset (ℕ × ℕ)} (h : ∀ (a b : ℕ), (Q.coeff b).coeff a ≠ 0 → (a, b) ∈ M) : Q = bivariateOf M fun (m : ℕ × ℕ) => (Q.coeff m.2).coeff m.1

A bivariate polynomial whose monomials lie in M is bivariateOf M of its coefficients.

The interpolation matrix

def Cslib.Code.Sudan.monomialsUpTo (d D j : ℕ) : Finset (ℕ × ℕ)

The monomials of (1, d)-weighted degree at most D and Y-degree at most j.

noncomputable def Cslib.Code.Sudan.interpMatrix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (α w : ι → F) (M : Finset (ℕ × ℕ)) : Fin (Fintype.card ι) → Fin M.card → F

The interpolation matrix: its rows are the points (α i, w i) (enumerated by Fintype.equivFin ι), its columns the monomials of M (enumerated by M.equivFin), and its entries the values of the monomials at the points.

noncomputable def Cslib.Code.Sudan.coeffsOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (u : Fin M.card → F) (m : ℕ × ℕ) : F

The coefficients on M given by a vector indexed by the enumeration of M, and zero elsewhere.

theorem Cslib.Code.Sudan.interpMatrix_dotProduct {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] (α w : ι → F) (M : Finset (ℕ × ℕ)) (u : Fin M.card → F) (i : ι) : interpMatrix α w M ((Fintype.equivFin ι) i) ⬝ᵥ u = Polynomial.evalEval (α i) (w i) (bivariateOf M (coeffsOf M u))

The product of a row of the interpolation matrix with a vector u is the value at the row's point of the polynomial with coefficients u.

The interpolant of least Y-degree

noncomputable def Cslib.Code.Sudan.kernelVecUpTo {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) (d D j : ℕ) : Fin (monomialsUpTo d D j).card → F

The kernel vector of the interpolation matrix on the monomials of Y-degree at most j.

noncomputable def Cslib.Code.Sudan.interpolantCoeffs {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) (d D : ℕ) : ℕ × ℕ → F

The coefficients of the interpolant: those of the first nonzero kernel vector among j = 0, 1, …, D / d.

noncomputable def Cslib.Code.Sudan.interpolant {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) (d D : ℕ) : Polynomial (Polynomial F)

An interpolant of least Y-degree, computed by elimination.

theorem Cslib.Code.Sudan.isInterpolant_interpolant {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) {d D : ℕ} (hd : 1 ≤ d) (hn : Fintype.card ι < (monomials d D).card) : IsInterpolant α w (d + 1) D (interpolant α w d D)

The elimination interpolant is an interpolant. With d ≥ 1 and more monomials of (1, d)-weighted degree at most D than points, interpolant α w d D is a Sudan interpolant for the dimension d + 1.

theorem Cslib.Code.Sudan.natDegree_interpolant_le {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) {d D : ℕ} (hd : 1 ≤ d) (hn : Fintype.card ι < (monomials d D).card) {Q : Polynomial (Polynomial F)} (hQ : IsInterpolant α w (d + 1) D Q) : (interpolant α w d D).natDegree ≤ Q.natDegree

The elimination interpolant has least Y-degree among all Sudan interpolants.

Simplicity of the roots

theorem Cslib.Code.Sudan.add_mul_add_one_le_of_mul {F : Type u_1} [Field F] {d D : ℕ} {P : Polynomial F} (hP : P.natDegree ≤ d) {S : Polynomial (Polynomial F)} (h : ∀ (a b : ℕ), (((Polynomial.X - Polynomial.C P) * S).coeff b).coeff a ≠ 0 → a + d * b ≤ D) (a b : ℕ) : (S.coeff b).coeff a ≠ 0 → a + d * (b + 1) ≤ D

Division by Y - P lowers the weighted degree bound by d. If P has degree at most d and every monomial of (Y - P) * S has (1, d)-weighted degree at most D, then every monomial X ^ a * Y ^ b of S has a + d * (b + 1) ≤ D.

theorem Cslib.Code.Sudan.exists_eq_mul_eval_ne_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] {α w : ι → F} {d D : ℕ} (hα : Function.Injective α) {Q : Polynomial (Polynomial F)} (hQ : IsInterpolant α w (d + 1) D Q) (hmin : ∀ (Q' : Polynomial (Polynomial F)), IsInterpolant α w (d + 1) D Q' → Q.natDegree ≤ Q'.natDegree) {P : Polynomial F} (hP : P.natDegree ≤ d) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) : ∃ (S : Polynomial (Polynomial F)), Q = (Polynomial.X - Polynomial.C P) * S ∧ Polynomial.eval P S ≠ 0 ∧ (Polynomial.eval P S).natDegree ≤ D - d

Large agreement gives simple roots. Let Q be a Sudan interpolant of least Y-degree for the dimension d + 1, with distinct points. If P has degree at most d and agrees with the received word at more than D points, then Q = (Y - P) * S where S(X, P(X)) is a nonzero polynomial of degree at most D - d.