Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.Basic

Polynomial Rows and Matrices #

Minimal row-oriented polynomial-matrix infrastructure for shifted row reduction.

source
@[reducible, inline]
abbrev CompPoly.PolynomialRow (F : Type u_1) [Zero F] :
Type u_1

A polynomial row over F[X].

Instances For
    source
    @[reducible, inline]
    abbrev CompPoly.PolynomialMatrix (F : Type u_1) [Zero F] :
    Type u_1

    A polynomial matrix over F[X], stored as an array of rows.

    Instances For
      source
      structure CompPoly.PolynomialMatrixShape :
      Type

      Runtime rectangular shape of a polynomial matrix.

      Instances For
        source
        def CompPoly.instReprPolynomialMatrixShape.repr :
        PolynomialMatrixShape → ℕ → Std.Format
        Instances For
          source
          @[instance_reducible]
          instance CompPoly.instReprPolynomialMatrixShape :
          Repr PolynomialMatrixShape
          source
          def CompPoly.instBEqPolynomialMatrixShape.beq :
          PolynomialMatrixShape → PolynomialMatrixShape → Bool
          Instances For
            source
            @[instance_reducible]
            instance CompPoly.instBEqPolynomialMatrixShape :
            BEq PolynomialMatrixShape
            source
            def CompPoly.instDecidableEqPolynomialMatrixShape.decEq (x✝ x✝¹ : PolynomialMatrixShape) :
            Decidable (x✝ = x✝¹)
            Instances For
              source
              @[instance_reducible]
              instance CompPoly.instDecidableEqPolynomialMatrixShape :
              DecidableEq PolynomialMatrixShape
              source
              def CompPoly.PolynomialMatrix.RowWidth {F : Type u_1} [Zero F] (row : PolynomialRow F) :
              ℕ

              Width of a row.

              Instances For
                source
                def CompPoly.PolynomialMatrix.MatrixWidth {F : Type u_1} [Zero F] (M : PolynomialMatrix F) :
                ℕ

                Matrix width, using the first row and width 0 for an empty matrix.

                Instances For
                  source
                  def CompPoly.PolynomialMatrix.MatrixShape {F : Type u_1} [Zero F] (M : PolynomialMatrix F) :
                  PolynomialMatrixShape

                  Runtime matrix shape.

                  Instances For
                    source
                    def CompPoly.PolynomialMatrix.MatrixRows {F : Type u_1} [Zero F] (M : PolynomialMatrix F) :
                    List (PolynomialRow F)

                    Matrix rows as a list, for membership statements.

                    Instances For
                      source
                      def CompPoly.PolynomialMatrix.WellFormed {F : Type u_1} [Zero F] (M : PolynomialMatrix F) :
                      Prop

                      A matrix is rectangular when every row has the matrix width.

                      Instances For
                        source
                        def CompPoly.PolynomialMatrix.rowGet {F : Type u_1} [Zero F] (row : PolynomialRow F) (j : ℕ) :
                        CPolynomial F

                        Read a row coefficient with zero default.

                        Instances For
                          source
                          def CompPoly.PolynomialMatrix.zeroRow {F : Type u_1} [Zero F] (width : ℕ) :
                          PolynomialRow F

                          The zero row of a fixed width.

                          Instances For
                            source
                            def CompPoly.PolynomialMatrix.rowAdd {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) :
                            PolynomialRow F

                            Pointwise row addition over the maximum input width.

                            Instances For
                              source
                              def CompPoly.PolynomialMatrix.rowNeg {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) :
                              PolynomialRow F

                              Pointwise row negation.

                              Instances For
                                source
                                def CompPoly.PolynomialMatrix.rowSub {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (a b : PolynomialRow F) :
                                PolynomialRow F

                                Pointwise row subtraction over the maximum input width.

                                Instances For
                                  source
                                  def CompPoly.PolynomialMatrix.rowScalePolynomial {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (c : CPolynomial F) (row : PolynomialRow F) :
                                  PolynomialRow F

                                  Multiply a row by a univariate polynomial.

                                  Instances For
                                    source
                                    def CompPoly.PolynomialMatrix.rowScaleMonomial {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (d : ℕ) (row : PolynomialRow F) :
                                    PolynomialRow F

                                    Multiply a row by c * X^d.

                                    Instances For
                                      source
                                      def CompPoly.PolynomialMatrix.rowSubScaledShift {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (a : PolynomialRow F) (c : F) (d : ℕ) (b : PolynomialRow F) :
                                      PolynomialRow F

                                      Fused a - c * X^d * b over the maximum input width, entrywise via CPolynomial.subMulMonomial. One call costs O(deg + d) per entry instead of the O(d * deg) convolution behind rowSub a (rowScaleMonomial c d b).

                                      Instances For
                                        source
                                        def CompPoly.PolynomialMatrix.replaceRow {F : Type u_1} [Zero F] (M : PolynomialMatrix F) (idx : ℕ) (row : PolynomialRow F) :
                                        PolynomialMatrix F

                                        Replace a row if the index is in bounds.

                                        Instances For