Documentation

Complexity.Foundations.Data.Code.SudanInterpolant

Sudan interpolants, weighted degree, and elimination #

Let w : ι → F be a received word and let α be distinct evaluation points. Sudan's list decoder [Sud97], [GRS19] for polynomials P of degree at most d needs a nonzero bivariate polynomial Q(X, Y) of (1, d)-weighted degree at most D (Cslib.Code.Sudan.WeightedDegreeLE), that is with a + d * b ≤ D for each of its monomials X ^ a * Y ^ b, vanishing at the n points (α i, w i) (Cslib.Code.Sudan.IsInterpolant). Such a Q is a nonzero solution of n linear equations in its coefficients, so it exists as soon as there are more than n monomials of (1, d)-weighted degree at most D (Cslib.Code.Sudan.exists_isInterpolant); for d ≥ 1 there are at least (D + 1) * (D + 2) / (2 * d) of them (Cslib.Code.Sudan.add_one_mul_add_two_le_two_mul_mul_card_monomials). If P has degree at most d, then Q(X, P(X)) has degree at most D (Cslib.Code.Sudan.WeightedDegreeLE.natDegree_eval_le) and vanishes at every point where P agrees with w; when there are more than D of them it is zero, so Y - P(X) divides Q(X, Y) (Cslib.Code.Sudan.IsInterpolant.X_sub_C_dvd): P is a root of Q viewed as a polynomial in Y over F[X].

This module also computes an explicit interpolant by linear algebra, choosing one 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 d ≥ 1 and 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 #

Main results #

References #

Monomials and weighted degree #

source
def Cslib.Code.Sudan.monomials (d D : ℕ) :
Finset (ℕ × ℕ)

The exponents (a, b) with a, b ≤ D of the monomials X ^ a * Y ^ b of (1, d)-weighted degree a + d * b at most D. For d ≥ 1 the bound b ≤ D holds for all of them.

Instances For
    source
    theorem Cslib.Code.Sudan.mem_monomials {d D : ℕ} {ab : ℕ × ℕ} :
    ab ∈ monomials d D ↔ ab.1 ≤ D ∧ ab.2 ≤ D ∧ ab.1 + d * ab.2 ≤ D

    (a, b) is in monomials d D exactly when a ≤ D, b ≤ D and a + d * b ≤ D.

    source
    theorem Cslib.Code.Sudan.add_one_mul_add_two_le_two_mul_mul_card_monomials {w : ℕ} (hw : 1 ≤ w) (D : ℕ) :
    (D + 1) * (D + 2) ≤ 2 * w * (monomials w D).card

    Counting monomials. For w ≥ 1 there are at least (D + 1) * (D + 2) / (2 * w) monomials of (1, w)-weighted degree at most D: for each j ≤ D there are j / w + 1 ≥ (j + 1) / w of weighted degree exactly j.

    source
    def Cslib.Code.Sudan.WeightedDegreeLE {F : Type u_1} [Field F] (d D : ℕ) (Q : Polynomial (Polynomial F)) :
    Prop

    Q has (1, d)-weighted degree at most D: every nonzero coefficient Q_{a,b} X ^ a Y ^ b has a + d * b ≤ D.

    Instances For
      source
      @[simp]
      theorem Cslib.Code.Sudan.weightedDegreeLE_zero {F : Type u_1} [Field F] (d D : ℕ) :
      WeightedDegreeLE d D 0

      The zero polynomial has (1, d)-weighted degree at most D.

      source
      theorem Cslib.Code.Sudan.WeightedDegreeLE.mono {F : Type u_1} [Field F] {d D D' : ℕ} {Q : Polynomial (Polynomial F)} (hQ : WeightedDegreeLE d D Q) (hD : D ≤ D') :
      WeightedDegreeLE d D' Q

      Monotonicity of (1, d)-weighted degree in the bound D.

      source
      theorem Cslib.Code.Sudan.WeightedDegreeLE.natDegree_mul_le {F : Type u_1} [Field F] {d D : ℕ} {Q : Polynomial (Polynomial F)} (hQ : WeightedDegreeLE d D Q) :
      Q.natDegree * d ≤ D

      If Q has (1, d)-weighted degree at most D, its Y-degree satisfies deg_Y Q * d ≤ D.

      source
      theorem Polynomial.eval_eval_eq_evalEval {R : Type u_3} [CommSemiring R] (Q : Polynomial (Polynomial R)) (P : Polynomial R) (x : R) :
      eval x (eval P Q) = evalEval x (eval x P) Q

      Evaluating Q(X, P(X)) at x evaluates Q at (x, P(x)).

      source
      theorem Cslib.Code.Sudan.WeightedDegreeLE.natDegree_eval_le {F : Type u_1} [Field F] {d E : ℕ} {S : Polynomial (Polynomial F)} {P : Polynomial F} (hS : WeightedDegreeLE d E S) (hP : P.natDegree ≤ d) :
      (Polynomial.eval P S).natDegree ≤ E

      Substituting Y = P(X), with P of degree at most d, into a bivariate polynomial of (1, d)-weighted degree at most E gives a polynomial of degree at most E.

      Bivariate polynomials from coefficients #

      source
      noncomputable def Cslib.Code.Sudan.bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) :
      Polynomial (Polynomial F)

      The bivariate polynomial with coefficient c m at X ^ m.1 * Y ^ m.2 for m ∈ M.

      Instances For
        source
        @[simp]
        theorem Cslib.Code.Sudan.coeff_coeff_bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) (a b : ℕ) :
        ((bivariateOf M c).coeff b).coeff a = if (a, b) ∈ M then c (a, b) else 0

        The coefficient of X ^ a * Y ^ b in bivariateOf M c is c (a, b) when (a, b) ∈ M, and zero otherwise.

        source
        theorem Cslib.Code.Sudan.evalEval_bivariateOf {F : Type u_1} [Field F] (M : Finset (ℕ × ℕ)) (c : ℕ × ℕ → F) (x y : F) :
        Polynomial.evalEval x y (bivariateOf M c) = ∑ m ∈ M, c m * x ^ m.1 * y ^ m.2

        The value of bivariateOf M c at (x, y) is ∑ m ∈ M, c m * x ^ m.1 * y ^ m.2.

        source
        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.

        source
        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.

        source
        theorem Cslib.Code.Sudan.weightedDegreeLE_bivariateOf {F : Type u_1} [Field F] {M : Finset (ℕ × ℕ)} {d D : ℕ} (hM : M ⊆ monomials d D) (c : ℕ × ℕ → F) :
        WeightedDegreeLE d D (bivariateOf M c)

        bivariateOf M c has (1, d)-weighted degree at most D when M ⊆ monomials d D.

        Sudan interpolants #

        source
        structure Cslib.Code.Sudan.IsInterpolant {F : Type u_1} {ι : Type u_2} [Field F] (α w : ι → F) (d D : ℕ) (Q : Polynomial (Polynomial F)) :
        Prop

        Q is a Sudan interpolant for the received word w with evaluation points α, weight d and weighted degree D: a nonzero bivariate polynomial of (1, d)-weighted degree at most D that vanishes at the points (α i, w i).

        • ne_zero : Q ≠ 0

          The interpolant is nonzero.

        • weightedDegree_le : WeightedDegreeLE d D Q

          Every monomial X ^ a * Y ^ b of Q has (1, d)-weighted degree a + d * b at most D.

        • evalEval_eq_zero (i : ι) : Polynomial.evalEval (α i) (w i) Q = 0

          The interpolant vanishes at the points (α i, w i).

        Instances For
          source
          theorem Cslib.Code.Sudan.IsInterpolant.natDegree_mul_le {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {d D : ℕ} {Q : Polynomial (Polynomial F)} (hQ : IsInterpolant α w d D Q) :
          Q.natDegree * d ≤ D

          The Y-degree of a Sudan interpolant: deg_Y Q * d ≤ D.

          source
          theorem Cslib.Code.Sudan.exists_isInterpolant {F : Type u_1} {ι : Type u_2} [Field F] {d D : ℕ} [Fintype ι] (α w : ι → F) (hn : Fintype.card ι < (monomials d D).card) :
          ∃ (Q : Polynomial (Polynomial F)), IsInterpolant α w d D Q

          Interpolation. If there are more than n monomials of (1, d)-weighted degree at most D, every received word has a Sudan interpolant: the n conditions Q (α i, w i) = 0 are linear in the coefficients of Q.

          source
          theorem Cslib.Code.Sudan.IsInterpolant.eval_eq_zero {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {d D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w d D Q) {P : Polynomial F} (hP : P.natDegree ≤ d) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) :
          Polynomial.eval P Q = 0

          Root containment. With distinct points, if P has degree at most d and agrees with the received word at more than D points, then Q(X, P(X)) = 0 for every Sudan interpolant Q.

          source
          theorem Cslib.Code.Sudan.IsInterpolant.X_sub_C_dvd {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {d D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w d D Q) {P : Polynomial F} (hP : P.natDegree ≤ d) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) :
          Polynomial.X - Polynomial.C P ∣ Q

          Root containment. With distinct points, if P has degree at most d and agrees with the received word at more than D points, then Y - P(X) divides every Sudan interpolant Q(X, Y).

          source
          theorem Cslib.Code.Sudan.IsInterpolant.mem_roots {F : Type u_1} {ι : Type u_2} [Field F] {α w : ι → F} {d D : ℕ} {Q : Polynomial (Polynomial F)} [Fintype ι] [DecidableEq F] (hα : Function.Injective α) (hQ : IsInterpolant α w d D Q) {P : Polynomial F} (hP : P.natDegree ≤ d) (hagree : D < {i : ι | Polynomial.eval (α i) P = w i}.card) :
          P ∈ Q.roots

          With distinct points, a polynomial of degree at most d that agrees with the received word at more than D points is a root of every Sudan interpolant, as a polynomial in Y.

          The interpolation matrix #

          source
          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.

          Instances For
            source
            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.

            Instances For
              source
              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.

              Instances For
                source
                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 #

                source
                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.

                Instances For
                  source
                  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.

                  Instances For
                    source
                    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.

                    Instances For
                      source
                      theorem Cslib.Code.Sudan.weightedDegreeLE_interpolant {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq F] (α w : ι → F) (d D : ℕ) :
                      WeightedDegreeLE d D (interpolant α w d D)

                      The elimination interpolant always has (1, d)-weighted degree at most D.

                      source
                      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 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 of weight d and weighted degree D.

                      source
                      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 D Q) :
                      (interpolant α w d D).natDegree ≤ Q.natDegree

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

                      Simplicity of the roots #

                      source
                      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 : WeightedDegreeLE d D ((Polynomial.X - Polynomial.C P) * S)) (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 (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.

                      source
                      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 D Q) (hmin : ∀ (Q' : Polynomial (Polynomial F)), IsInterpolant α w d 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 weight d and weighted degree D, 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.