Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohann

Mulders-Storjohann Shifted Row Reduction #

Direct executable shifted row reduction over polynomial rows.

References #

source
def CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowStep? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (found : Option (ℕ × ℕ)) (j : ℕ) :
Option (ℕ × ℕ)

One inner-loop update for shifted-leading-position conflict search.

Instances For
    source
    def CompPoly.PolynomialMatrix.shiftedLeadingConflictInRow? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (found : Option (ℕ × ℕ)) :
    Option (ℕ × ℕ)

    Scan one row index i for a shifted-leading-position conflict.

    Instances For
      source
      def CompPoly.PolynomialMatrix.shiftedLeadingConflictFromStep? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (found : Option (ℕ × ℕ)) (i : ℕ) :
      Option (ℕ × ℕ)

      One outer-loop update for shifted-leading-position conflict search.

      Instances For
        source
        def CompPoly.PolynomialMatrix.shiftedLeadingConflictFrom? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (found : Option (ℕ × ℕ)) :
        Option (ℕ × ℕ)

        Scan all row pairs for the first shifted-leading-position conflict.

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

          First pair of nonzero rows with the same shifted leading position.

          Instances For
            source
            def CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (target reducer : PolynomialRow F) (shift : Array ℕ) :
            PolynomialRow F

            Cancel the shifted leading term of target using reducer, when possible.

            Instances For
              source
              def CompPoly.PolynomialMatrix.muldersStorjohannStep {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i j : ℕ) :
              PolynomialMatrix F

              One Mulders-Storjohann cancellation step for a chosen conflicting pair.

              Instances For
                source
                def CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuel {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] :
                ℕ → PolynomialMatrix F → Array ℕ → PolynomialMatrix F

                Fuel-bounded Mulders-Storjohann reduction loop.

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

                  Maximum shifted row degree among the rows of a matrix.

                  Instances For
                    source
                    def CompPoly.PolynomialMatrix.muldersStorjohannFuel {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
                    ℕ

                    Executable fuel used by the direct reducer.

                    Instances For
                      source
                      def CompPoly.PolynomialMatrix.muldersStorjohannReduce {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
                      PolynomialMatrix F

                      Direct executable Mulders-Storjohann shifted row reducer.

                      Instances For

                        Fast variants #

                        The loop above recomputes every row's shifted leading position for every scanned row pair, and cancels leading terms through a generic monomial-times-row multiplication. The variants below compute each row's leading position once per scan and use the fused rowSubScaledShift update. They are proved extensionally equal to the direct definitions in MuldersStorjohannCorrectness/Fast.lean, so all correctness results transfer.

                        source
                        def CompPoly.PolynomialMatrix.rowLeadingPositions {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
                        Array (Option ℕ)

                        Shifted leading positions of all rows, computed once per conflict scan.

                        Instances For
                          source
                          def CompPoly.PolynomialMatrix.cachedLeadingConflictInRowStep? (positions : Array (Option ℕ)) (i : ℕ) (found : Option (ℕ × ℕ)) (j : ℕ) :
                          Option (ℕ × ℕ)

                          One inner-loop update for cached shifted-leading-position conflict search.

                          Instances For
                            source
                            def CompPoly.PolynomialMatrix.cachedLeadingConflictInRow? (positions : Array (Option ℕ)) (i : ℕ) (found : Option (ℕ × ℕ)) :
                            Option (ℕ × ℕ)

                            Scan one row index i for a cached shifted-leading-position conflict.

                            Instances For
                              source
                              def CompPoly.PolynomialMatrix.cachedLeadingConflict? (positions : Array (Option ℕ)) :
                              Option (ℕ × ℕ)

                              First pair of rows with the same cached shifted leading position.

                              Instances For
                                source
                                def CompPoly.PolynomialMatrix.cancelShiftedLeadingTermFast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (target reducer : PolynomialRow F) (shift : Array ℕ) :
                                PolynomialRow F

                                cancelShiftedLeadingTerm with the fused row update.

                                Instances For
                                  source
                                  def CompPoly.PolynomialMatrix.muldersStorjohannStepFast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i j : ℕ) :
                                  PolynomialMatrix F

                                  One fast Mulders-Storjohann cancellation step.

                                  Instances For
                                    source
                                    def CompPoly.PolynomialMatrix.muldersStorjohannReduceWithFuelFast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] :
                                    ℕ → PolynomialMatrix F → Array ℕ → PolynomialMatrix F

                                    Fuel-bounded fast Mulders-Storjohann reduction loop.

                                    Instances For
                                      source
                                      def CompPoly.PolynomialMatrix.muldersStorjohannReduceFast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
                                      PolynomialMatrix F

                                      Fast executable Mulders-Storjohann shifted row reducer. Agrees with muldersStorjohannReduce; see muldersStorjohannReduceFast_eq.

                                      Instances For