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:

• Mathlib's Polynomial.Bivariate (see CompPoly/Bivariate/ToPoly.lean)
• ArkLib's Polynomial.Bivariate interface (see ArkLib/Data/Polynomial/Bivariate.lean and ArkLib/Data/CodingTheory/PolishchukSpielman/Degrees.lean, BCIKS20.lean, etc.)

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.

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.

theorem CompPoly.CBivariate.ext_iff {R : Type u_1} [Zero R] {p q : CBivariate R} : p = q ↔ ↑p = ↑q

@[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.

@[implicit_reducible]

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

The zero bivariate polynomial is canonical.

@[implicit_reducible]

instance CompPoly.CBivariate.instBEq {R : Type u_1} [Zero R] [BEq R] : BEq (CBivariate R)

instance CompPoly.CBivariate.instLawfulBEq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : LawfulBEq (CBivariate R)

@[implicit_reducible]

instance CompPoly.CBivariate.instDecidableEq {R : Type u_1} [Zero R] [DecidableEq R] : DecidableEq (CBivariate R)

@[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

@[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).

@[implicit_reducible]

instance CompPoly.CBivariate.instCommSemiring {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CBivariate R)

@[implicit_reducible]

instance CompPoly.CBivariate.instRing {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Ring (CBivariate R)

@[implicit_reducible]

instance CompPoly.CBivariate.instCommRing {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommRing (CBivariate R)

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.

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.

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.

Folds the Y-coefficients of f with a raw Horner pattern (smulRight a then addRaw), trimming once at the end. This avoids paying one CPolynomial.mul and one CPolynomial.add trim per Y-coefficient.

def CompPoly.CBivariate.evalYHorner {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (a : R) (p : CBivariate R) : CPolynomial R

Evaluate in the second variable (Y) at a using Horner's method, yielding a univariate polynomial in X.

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.

See CBivariate.eval_y_horner_eq_eval_y in CompPoly/Bivariate/ToPoly.lean for agreement between evalY and evalYHorner.

def CompPoly.CBivariate.evalEvalHornerYThenX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (x y : R) (p : CBivariate R) : R

Full evaluation at (x, y) using Horner in Y, then Horner in X on the intermediate univariate polynomial.

def CompPoly.CBivariate.evalEvalHornerXThenY {R : Type u_1} [Semiring R] (x y : R) (p : CBivariate R) : R

Full evaluation at (x, y) by evaluating each X-coefficient polynomial at x, then Horner-evaluating the resulting scalar polynomial in Y.

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

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.

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.

@[simp]

theorem CompPoly.CBivariate.coeff_eq_coeff_coeff {R : Type u_1} [Zero R] (f : CBivariate R) (i j : ℕ) : f.coeff i j = (CPolynomial.coeff f j).coeff i

CBivariate.coeff as two composed CPolynomial.coeff.

theorem CompPoly.CBivariate.coeff_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CBivariate R) (i j : ℕ) : (p + q).coeff i j = p.coeff i j + q.coeff i j

Bivariate coefficients are additive.

theorem CompPoly.CBivariate.coeff_finset_sum {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (f : ι → CBivariate R) (i j : ℕ) : (s.sum f).coeff i j = ∑ t ∈ s, (f t).coeff i j

Bivariate coefficients distribute over finite sums.

theorem CompPoly.CBivariate.coeff_monomialXY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a b : ℕ) (c : R) (i j : ℕ) : (monomialXY a b c).coeff i j = if i = a ∧ j = b then c else 0

Coefficient of a bivariate monomial c * X^a * Y^b.

theorem CompPoly.CBivariate.coeff_monomialY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (m : ℕ) (c : CPolynomial R) (i j : ℕ) : coeff (CPolynomial.monomial m c) i j = if j = m then c.coeff i else 0

Coefficient of Y^m * c(X) as a bivariate polynomial.

theorem CompPoly.CBivariate.eq_iff_coeff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : CBivariate R} : p = q ↔ ∀ (i j : ℕ), p.coeff i j = q.coeff i j

Two bivariate polynomials are equal iff all their coefficients agree.

theorem CompPoly.CBivariate.totalDegree_eq_natWeightedDegree {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.

theorem CompPoly.CBivariate.natDegreeX_eq_natWeightedDegree {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.

theorem CompPoly.CBivariate.natDegreeY_eq_natWeightedDegree {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (f : CBivariate R) : f.natDegreeY = f.natWeightedDegree 0 1

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

theorem CompPoly.CBivariate.natWeightedDegree_monomialXY {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] {n m : ℕ} {c : R} (hc : c ≠ 0) (u v : ℕ) : (monomialXY n m c).natWeightedDegree u v = u * n + v * m

The weighted degree of a nonzero monomial c * X^n * Y^m is u * n + v * m where u is the weight of X and v the weight of Y.

theorem CompPoly.CBivariate.natWeightedDegree_zero {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (u v : ℕ) : natWeightedDegree 0 u v = 0

The weighted degree of the zero polynomial is zero.

theorem CompPoly.CBivariate.natWeightedDegree_le_iff {R : Type u_1} [BEq R] [Semiring R] (f : CBivariate R) (u v d : ℕ) : f.natWeightedDegree u v ≤ d ↔ ∀ j ∈ f.supportY, u * ((↑f).coeff j).natDegree + v * j ≤ d

The weighted degree is at most d iff every Y-support index satisfies the weighted bound.

theorem CompPoly.CBivariate.natWeightedDegree_le_iff_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (f : CBivariate R) (u v d : ℕ) : f.natWeightedDegree u v ≤ d ↔ ∀ (i j : ℕ), f.coeff i j ≠ 0 → u * i + v * j ≤ d

The weighted degree is at most d iff every monomial index satisfies the weighted bound.

theorem CompPoly.CBivariate.natWeightedDegree_CC {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] {r : R} (u v : ℕ) : (CC r).natWeightedDegree u v = 0

The natWeightedDegree of a constant bivariate polynomial CBivariate.CC is zero.

theorem CompPoly.CBivariate.natWeightedDegree_add_le {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : CBivariate R) (u v : ℕ) : (p + q).natWeightedDegree u v ≤ max (p.natWeightedDegree u v) (q.natWeightedDegree u v)

The weighted degree of a sum is at most the max of the weighted degrees.