Documentation

CompPoly.Bivariate.Basic

Computable Bivariate Polynomials #

This file defines CBivariate R, the computable representation of bivariate polynomials with coefficients in R. The type is CPolynomial (CPolynomial R), i.e. polynomials in Y with coefficients that are polynomials in X, matching Mathlib's R[X][Y] (i.e. Polynomial (Polynomial R)).

The design is intended to be compatible with:

source
def CompPoly.CBivariate (R : Type u_1) [Zero R] :
Type u_1

Computable bivariate polynomials: F[X][Y] as CPolynomial (CPolynomial R).

Each p : CBivariate R is a polynomial in Y whose coefficients are univariate polynomials in X. The outer structure is indexed by powers of Y, the inner by powers of X.

Instances For
    source
    theorem CompPoly.CBivariate.ext {R : Type u_1} [Zero R] {p q : CBivariate R} (h : ↑p = ↑q) :
    p = q

    Extensionality: two bivariate polynomials are equal if their underlying values are.

    source
    theorem CompPoly.CBivariate.ext_iff {R : Type u_1} [Zero R] {p q : CBivariate R} :
    p = q ↔ ↑p = ↑q
    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instCoeCPolynomial {R : Type u_1} [Zero R] :
    Coe (CBivariate R) (CPolynomial (CPolynomial R))

    Coerce to the underlying univariate polynomial (in Y) with polynomial coefficients.

    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instInhabited {R : Type u_1} [Zero R] :
    Inhabited (CBivariate R)

    The zero bivariate polynomial is canonical.

    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instBEq {R : Type u_1} [Zero R] [BEq R] :
    BEq (CBivariate R)
    source
    instance CompPoly.CBivariate.instLawfulBEq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] :
    LawfulBEq (CBivariate R)
    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instDecidableEq {R : Type u_1} [Zero R] [DecidableEq R] :
    DecidableEq (CBivariate R)
    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instAddCommMonoid {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    AddCommMonoid (CBivariate R)

    Additive structure on CBivariate R

    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instSemiring {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    Semiring (CBivariate R)

    Ring structure on CBivariate R (for ring equiv with Mathlib in ToPoly).

    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instCommSemiring {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    CommSemiring (CBivariate R)
    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instRing {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    Ring (CBivariate R)
    source
    @[implicit_reducible]
    instance CompPoly.CBivariate.instCommRing {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    CommRing (CBivariate R)
    source
    def CompPoly.CBivariate.CC {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (r : R) :
    CBivariate R

    Constant as a bivariate polynomial. Mathlib: Polynomial.Bivariate.CC.

    Instances For
      source
      def CompPoly.CBivariate.X {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
      CBivariate R

      The variable X (inner variable). As bivariate: polynomial in Y with single coeff X at Y^0.

      Instances For
        source
        def CompPoly.CBivariate.Y {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] :
        CBivariate R

        The variable Y (outer variable). Monomial Y^1 with coefficient 1.

        Instances For
          source
          def CompPoly.CBivariate.monomialXY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (n m : ℕ) (c : R) :
          CBivariate R

          Monomial c * X^n * Y^m. ArkLib: Polynomial.Bivariate.monomialXY.

          Instances For
            source
            def CompPoly.CBivariate.coeff {R : Type u_1} [Zero R] (f : CBivariate R) (i j : ℕ) :
            R

            Coefficient of X^i Y^j in the bivariate polynomial. Here i is the X-exponent (inner) and j is the Y-exponent (outer). ArkLib: Polynomial.Bivariate.coeff f i j.

            Instances For
              source
              def CompPoly.CBivariate.supportY {R : Type u_1} [Zero R] [BEq R] (f : CBivariate R) :
              Finset ℕ

              The Y-support: indices j such that the coefficient of Y^j is nonzero.

              Instances For
                source
                def CompPoly.CBivariate.supportX {R : Type u_1} [Zero R] [BEq R] (f : CBivariate R) :
                Finset ℕ

                The X-support: indices i such that the coefficient of X^i is nonzero (i.e. some monomial X^i Y^j has nonzero coefficient).

                Instances For
                  source
                  def CompPoly.CBivariate.natDegreeY {R : Type u_1} [Zero R] (f : CBivariate R) :
                  ℕ

                  The Y-degree (degree when viewed as a polynomial in Y). ArkLib: Polynomial.Bivariate.natDegreeY.

                  Instances For
                    source
                    def CompPoly.CBivariate.natDegreeX {R : Type u_1} [Zero R] [BEq R] (f : CBivariate R) :
                    ℕ

                    The X-degree: maximum over all Y-coefficients of their degree in X. ArkLib: Polynomial.Bivariate.natDegreeX.

                    Instances For
                      source
                      def CompPoly.CBivariate.totalDegree {R : Type u_1} [Zero R] [BEq R] (f : CBivariate R) :
                      ℕ

                      Total degree: max over monomials of (deg_X + deg_Y). ArkLib: Polynomial.Bivariate.totalDegree.

                      Instances For
                        source
                        def CompPoly.CBivariate.natWeightedDegree {R : Type u_1} [Zero R] [BEq R] (f : CBivariate R) (u v : ℕ) :
                        ℕ

                        The (u, v)-weighted degree: max over monomials of u * deg_X + v * deg_Y.

                        Instances For
                          source
                          def CompPoly.CBivariate.evalX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (a : R) (f : CBivariate R) :
                          CPolynomial R

                          Evaluate in the first variable (X) at a, yielding a univariate polynomial in Y. ArkLib: Polynomial.Bivariate.evalX.

                          Instances For
                            source
                            def CompPoly.CBivariate.evalY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (a : R) (f : CBivariate R) :
                            CPolynomial R

                            Evaluate in the second variable (Y) at a, yielding a univariate polynomial in X. ArkLib: Polynomial.Bivariate.evalY.

                            Instances For
                              source
                              def CompPoly.CBivariate.evalEval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (x y : R) (f : CBivariate R) :
                              R

                              Full evaluation at (x, y): p(x, y). Inner variable X at x, outer variable Y at y. Equivalently (evalY y f).eval x. Mathlib: Polynomial.evalEval.

                              Instances For
                                source
                                def CompPoly.CBivariate.swap {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) :
                                CBivariate R

                                Swap the roles of X and Y. ArkLib/Mathlib: Polynomial.Bivariate.swap. TODO a more efficient implementation

                                Instances For
                                  source
                                  def CompPoly.CBivariate.leadingCoeffY {R : Type u_1} [Zero R] (f : CBivariate R) :
                                  CPolynomial R

                                  Leading coefficient when viewed as a polynomial in Y. ArkLib: Polynomial.Bivariate.leadingCoeffY.

                                  Instances For
                                    source
                                    def CompPoly.CBivariate.leadingCoeffX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CBivariate R) :
                                    CPolynomial R

                                    Leading coefficient when viewed as a polynomial in X. The coefficient of X^(degreeX f): a polynomial in Y.

                                    Instances For
                                      source
                                      theorem CompPoly.CBivariate.totalDegree_as_weightedDegree {R : Type u_1} [BEq R] [Semiring R] (f : CBivariate R) :
                                      f.totalDegree = f.natWeightedDegree 1 1

                                      The total degree is the (1, 1)-weighted degree.

                                      source
                                      theorem CompPoly.CBivariate.natDegreeX_as_weightedDegree {R : Type u_1} [BEq R] [Semiring R] (f : CBivariate R) :
                                      f.natDegreeX = f.natWeightedDegree 1 0

                                      The X-degree is the (1, 0)-weighted degree.