Documentation

CompPoly.Bivariate.CoeffRows

Coefficient Rows for Bivariate Polynomials #

Conversions between finite Y-coefficient rows and CBivariate.

source
def CompPoly.CBivariate.ofCoeffRow {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) :
CBivariate F

Interpret a polynomial row [q_0, ..., q_l] as ∑ q_j(X) Y^j.

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

    Truncate a bivariate polynomial to its first width Y-coefficient rows.

    Instances For
      source
      theorem CompPoly.CBivariate.toCoeffRow_size {F : Type u_1} [Zero F] (width : ℕ) (Q : CBivariate F) :
      Array.size (toCoeffRow width Q) = width

      Truncated coefficient rows have the requested width.

      source
      def CompPoly.CBivariate.weightedDegreeShift (w width : ℕ) :
      Array ℕ

      Lee-style shift array for (1, w) weighted degree.

      Instances For
        source
        theorem CompPoly.CBivariate.coeff_ofCoeffRow_of_lt {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) {i j : ℕ} (hj : j < Array.size row) :
        (ofCoeffRow row).coeff i j = (Array.getD row j 0).coeff i

        Coefficient-row conversion preserves finite Y coefficients below row width.

        source
        theorem CompPoly.CBivariate.coeff_ofCoeffRow_of_size_le {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) {i j : ℕ} (hj : Array.size row ≤ j) :
        (ofCoeffRow row).coeff i j = 0

        Coefficients past the row width vanish after row-to-bivariate conversion.

        source
        theorem CompPoly.CBivariate.rowShiftedDegree?_eq_natWeightedDegree_ofCoeffRow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (w d : ℕ) (hdeg : PolynomialMatrix.rowShiftedDegree? row (weightedDegreeShift w (Array.size row)) = some d) :
        (ofCoeffRow row).natWeightedDegree 1 w = d

        Row shifted degree for the Lee shift matches weighted degree of the bivariate view.

        source
        theorem CompPoly.CBivariate.natWeightedDegree_ofCoeffRow_le_of_rowShiftedDegree?_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (w bound d : ℕ) (hdeg : PolynomialMatrix.rowShiftedDegree? row (weightedDegreeShift w (Array.size row)) = some d) (hle : d ≤ bound) :
        (ofCoeffRow row).natWeightedDegree 1 w ≤ bound

        Weighted-degree bounded rows convert to weighted-degree bounded bivariate polynomials.