Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.Shifted

Shifted Degrees for Polynomial Rows #

source
structure CompPoly.PolynomialMatrix.ShiftedLeadingTerm (F : Type u_2) :
Type u_2

Shifted leading term metadata for a nonzero row.

  • position : ℕ
  • degree : ℕ
  • shiftedDegree : ℕ
  • coeff : F
Instances For
    source
    def CompPoly.PolynomialMatrix.instReprShiftedLeadingTerm.repr {F✝ : Type u_2} [Repr F✝] :
    ShiftedLeadingTerm F✝ → ℕ → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance CompPoly.PolynomialMatrix.instReprShiftedLeadingTerm {F✝ : Type u_2} [Repr F✝] :
      Repr (ShiftedLeadingTerm F✝)
      source
      def CompPoly.PolynomialMatrix.maxOption :
      Option ℕ → ℕ → Option ℕ

      Insert a natural number into an optional running maximum.

      Instances For
        source
        def CompPoly.PolynomialMatrix.shiftedEntryDegree? {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) (shift : Array ℕ) (j : ℕ) :
        Option ℕ

        Shifted degree of one row entry. Zero entries have no degree.

        Instances For
          source
          def CompPoly.PolynomialMatrix.rowShiftedDegree? {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) (shift : Array ℕ) :
          Option ℕ

          Shifted degree of a row, with none exactly for zero rows.

          Instances For
            source
            def CompPoly.PolynomialMatrix.rowShiftedLeadingPosition? {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) (shift : Array ℕ) :
            Option ℕ

            Shifted leading position of a nonzero row. Ties use the largest column index.

            Instances For
              source
              def CompPoly.PolynomialMatrix.rowShiftedLeadingTerm? {F : Type u_1} [Zero F] [BEq F] (row : PolynomialRow F) (shift : Array ℕ) :
              Option (ShiftedLeadingTerm F)

              Shifted leading term metadata for a nonzero row.

              Instances For
                source
                theorem CompPoly.PolynomialMatrix.shiftedEntryDegree?_eq_some_iff {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (shift : Array ℕ) (j d : ℕ) :
                shiftedEntryDegree? row shift j = some d ↔ rowGet row j ≠ 0 ∧ (rowGet row j).natDegree + shift.getD j 0 = d

                A row entry has shifted degree d exactly when it is nonzero and d is its shifted degree.

                source
                theorem CompPoly.PolynomialMatrix.rowShiftedDegree?_eq_none_iff {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {row : PolynomialRow F} {shift : Array ℕ} :
                rowShiftedDegree? row shift = none ↔ RowIsZero row

                Nonzero rows are exactly the rows with a shifted degree.

                source
                theorem CompPoly.PolynomialMatrix.shiftedEntryDegree?_le_of_rowShiftedDegree?_eq_some {F : Type u_1} [Zero F] [BEq F] {row : PolynomialRow F} {shift : Array ℕ} {d j e : ℕ} (hdeg : rowShiftedDegree? row shift = some d) (hj : j < Array.size row) (hentry : shiftedEntryDegree? row shift j = some e) :
                e ≤ d

                A returned shifted row degree bounds every nonzero shifted entry degree.

                source
                theorem CompPoly.PolynomialMatrix.exists_shiftedEntryDegree?_eq_of_rowShiftedDegree?_eq_some {F : Type u_1} [Zero F] [BEq F] {row : PolynomialRow F} {shift : Array ℕ} {d : ℕ} (hdeg : rowShiftedDegree? row shift = some d) :
                ∃ j < Array.size row, shiftedEntryDegree? row shift j = some d

                A returned shifted row degree is attained by some row entry.

                source
                def CompPoly.PolynomialMatrix.ShiftedWeakPopov {F : Type u_1} [Zero F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) :
                Prop

                A shifted weak-Popov matrix has distinct leading positions among nonzero rows.

                Instances For