Documentation

CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution

Shifted Substitution for Guruswami-Sudan Root Search #

Executable substitution of Y = f(X) + X^t Y in bivariate polynomials.

source
def CompPoly.GuruswamiSudan.shiftPolynomialByXPower {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (p : CPolynomial F) (t : ℕ) :
CPolynomial F

Multiply a univariate polynomial by X^t.

Instances For
    source
    def CompPoly.GuruswamiSudan.shiftedSubstitutionCoeffTerm {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (coeffY f : CPolynomial F) (t y r : ℕ) :
    CPolynomial F

    The contribution of one Y^y coefficient to Y^r after substituting Y = f(X) + X^t Y.

    Instances For
      source
      def CompPoly.GuruswamiSudan.substituteYPolynomialPlusXPowerY {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (Q : CBivariate F) (f : CPolynomial F) (t : ℕ) :
      CBivariate F

      Substitute Y = f(X) + X^t Y into a bivariate polynomial.

      Instances For
        source
        def CompPoly.GuruswamiSudan.substituteYPolynomialPlusXPowerYTruncated {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (Q : CBivariate F) (f : CPolynomial F) (t N : ℕ) :
        CBivariate F

        Truncated substitution Y = f(X) + X^t Y, keeping only X-degree < N after each accumulated Y-coefficient contribution.

        Instances For