Documentation

CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Algorithm

Executable Lee-O'Sullivan Interpolation #

Executable Lee-O'Sullivan interpolation via an explicit F[X] module basis and shifted polynomial-row reduction.

References #

source
structure CompPoly.GuruswamiSudan.LeeOSullivan.RowChoice (F : Type u_2) [Zero F] :
Type u_2

Candidate row selected by least-shifted-degree scanning.

Instances For
    source
    def CompPoly.GuruswamiSudan.LeeOSullivan.betterRowChoice {F : Type u_1} [Field F] (candidate current : RowChoice F) :
    Bool

    Tie-breaking order for least-shifted-degree row selection.

    Instances For
      source
      def CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeRowStep? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (best : Option (RowChoice F)) (i : ℕ) :
      Option (RowChoice F)

      One left-to-right scan step for least-shifted-degree row selection.

      Instances For
        source
        def CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeChoice? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
        Option (RowChoice F)

        Scan row indices for the best least-shifted-degree candidate.

        Instances For
          source
          def CompPoly.GuruswamiSudan.LeeOSullivan.leastShiftedDegreeRow? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
          Option (PolynomialRow F)

          Select a nonzero row of least shifted degree from a reduced matrix.

          Instances For
            source
            def CompPoly.GuruswamiSudan.LeeOSullivan.normalizeLeeCandidate? {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (params : GSInterpParams) (Q : CBivariate F) :
            Option (CBivariate F)

            Normalize a row-derived candidate using the shared interpolation vector policy.

            Instances For
              source
              def CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanPositiveInterpolate {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (reducer : PolynomialMatrix.ShiftedRowReducerContext F) (points : Array (F × F)) (params : GSInterpParams) :
              Option (CBivariate F)

              Positive-Y-weight Lee-O'Sullivan interpolation branch.

              Instances For
                source
                def CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanInterpolate {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (reducer : PolynomialMatrix.ShiftedRowReducerContext F) (points : Array (F × F)) (params : GSInterpParams) :
                Option (CBivariate F)

                Lee-O'Sullivan interpolation with the shared low-message branch.

                Instances For