Starlib-Specific Bivariate Polynomial Extensions

The core bivariate polynomial definitions and degree/eval/multiplicity theory are provided by CompPoly (CompPoly.ToMathlib.Polynomial.BivariateDegree, BivariateWeightedDegree, BivariateMultiplicity). This file contains only Starlib-specific extensions:

• Finset-level coefficient and evaluation helpers (coeffs, evalSetX, evalSetY)
• Quotient (divisibility) predicates and degree bounds
• Linear-map monomial constructors (monomialY, monomialXY) and their algebra

noncomputable def Polynomial.Bivariate.coeffs {F : Type} [Semiring F] [DecidableEq F] (f : Polynomial (Polynomial F)) : Finset (Polynomial F)

The set of coefficients of a bivariate polynomial.

theorem Polynomial.Bivariate.ne_zero_iff_coeffs_ne_zero {F : Type} [Semiring F] (f : Polynomial (Polynomial F)) : f ≠ 0 ↔ f.coeff ≠ 0

A bivariate polynomial is non-zero if and only if its coefficient function is non-zero.

theorem Polynomial.Bivariate.degreesY_nonempty {F : Type} [Semiring F] {f : Polynomial (Polynomial F)} (hf : f ≠ 0) : f.toFinsupp.support.Nonempty

The set of Y-degrees is non-empty.

theorem Polynomial.Bivariate.natDegree_sum_lt_of_forall_lt {F : Type} [Semiring F] {α : Type} {s : Finset α} {g : α → Polynomial F} {deg : ℕ} : 0 < deg → (∀ x ∈ s, (g x).natDegree < deg) → (∑ x ∈ s, g x).natDegree < deg

theorem Polynomial.Bivariate.natDeg_sum_eq_of_unique {F : Type} [Semiring F] {α : Type} {s : Finset α} {f : α → Polynomial F} {deg : ℕ} (mx : α) (h : mx ∈ s) : (f mx).natDegree = deg → (∀ y ∈ s, y ≠ mx → (f y).natDegree < deg ∨ f y = 0) → (∑ x ∈ s, f x).natDegree = deg

theorem Polynomial.Bivariate.sup_eq_of_le_of_reach {α β : Type} [SemilatticeSup β] [OrderBot β] {s : Finset α} {f : α → β} (x : α) {y : β} (h : x ∈ s) : f x = y → (∀ x ∈ s, f x ≤ y) → s.sup f = y

If some element x ∈ s maps to y under f, and every element of s maps to a value less than or equal to y, then the supremum of f over s is exactly y.

noncomputable def Polynomial.Bivariate.evalSetX {F : Type} [Semiring F] [DecidableEq F] (f : Polynomial (Polynomial F)) (P : Finset F) [Nonempty ↥P] : Finset (Polynomial F)

Evaluating a bivariate polynomial in the first variable X on a set of points. This results in a set of univariate polynomials in Y.

noncomputable def Polynomial.Bivariate.evalSetY {F : Type} [Semiring F] [DecidableEq F] (f : Polynomial (Polynomial F)) (P : Finset F) [Nonempty ↥P] : Finset (Polynomial F)

Evaluating a bivariate polynomial in the second variable Y on a set of points resulting in a set of univariate polynomials in X.

def Polynomial.Bivariate.quotient {F : Type} [Semiring F] (f g : Polynomial (Polynomial F)) : Prop

The bivariate quotient polynomial.

theorem Polynomial.Bivariate.quotient_nezero {F : Type} [Semiring F] {f q : Polynomial (Polynomial F)} (hg : q * f ≠ 0) : q ≠ 0

The quotient of two non-zero bivariate polynomials is non-zero.

theorem Polynomial.Bivariate.coeff_ne_zero {F : Type} [Semiring F] {f q : Polynomial (Polynomial F)} (hg : q * f ≠ 0) : q.coeff ≠ 0

If a non-zero bivariate polynomial f divides a non-zero bivariate polynomial g, then all the coefficients of the quoetient are non-zero.

theorem Polynomial.Bivariate.degreeX_le_degreeX_sub_degreeX {F : Type} [Semiring F] [IsDomain F] {f q : Polynomial (Polynomial F)} (hf : f ≠ 0) (hg : q * f ≠ 0) : degreeX q ≤ degreeX (q * f) - degreeX f

theorem Polynomial.Bivariate.degreeY_le_degreeY_sub_degreeY {F : Type} [Semiring F] [IsDomain F] {f q : Polynomial (Polynomial F)} (hf : f ≠ 0) (hg : q * f ≠ 0) : natDegreeY q ≤ natDegreeY (q * f) - natDegreeY f

theorem Polynomial.Bivariate.coeff_totalDegree_le {F : Type} [Semiring F] (f : Polynomial (Polynomial F)) {n : ℕ} (hn : n ∈ f.support) : (f.coeff n).natDegree + n ≤ totalDegree f

Each coefficient's total-degree contribution is bounded by totalDegree when in support.

theorem Polynomial.Bivariate.coeff_totalDegree_le' {F : Type} [Semiring F] (f : Polynomial (Polynomial F)) (n : ℕ) : (f.coeff n).natDegree + n ≤ totalDegree f ∨ f.coeff n = 0

theorem Polynomial.Bivariate.exists_max_index_totalDegree {F : Type} [Semiring F] (f : Polynomial (Polynomial F)) (hf : f ≠ 0) : ∃ mm ∈ f.support, (f.coeff mm).natDegree + mm = totalDegree f ∧ ∀ (n : ℕ), mm < n → (f.coeff n).natDegree + n < totalDegree f ∨ f.coeff n = 0

There exists a maximal Y-index achieving totalDegree. Above it, total-degree contributions are strictly smaller or the coefficient vanishes.

theorem Polynomial.Bivariate.totalDegree_mul_le {F : Type} [Semiring F] (f g : Polynomial (Polynomial F)) : totalDegree (f * g) ≤ totalDegree f + totalDegree g

@[simp]

theorem Polynomial.Bivariate.totalDegree_mul {F : Type} [Semiring F] [IsDomain F] {f g : Polynomial (Polynomial F)} (hf : f ≠ 0) (hg : g ≠ 0) : totalDegree (f * g) = totalDegree f + totalDegree g

The total degree of the product of two bivariate polynomials is the sum of their total degrees.

noncomputable def Polynomial.Bivariate.monomialY {F : Type} [Semiring F] (n : ℕ) : Polynomial F →ₗ[Polynomial F] Polynomial (Polynomial F)

Definition of a monomial when the bivariate polynomial is considered as a univariate polynomial in Y.

noncomputable def Polynomial.Bivariate.monomialXY {F : Type} [Semiring F] (n m : ℕ) : F →ₗ[F] Polynomial (Polynomial F)

Definition of the bivariate monomial X^n * Y^m

theorem Polynomial.Bivariate.monomialXY_def {F : Type} [Semiring F] {n m : ℕ} {a : F} : (monomialXY n m) a = (Polynomial.monomial m) ((Polynomial.monomial n) a)

The bivariate monomial is well-defined.

@[simp]

theorem Polynomial.Bivariate.monomialXY_add {F : Type} [Semiring F] {n m : ℕ} {a b : F} : (monomialXY n m) (a + b) = (monomialXY n m) a + (monomialXY n m) b

Adding bivariate monomials works as expected. In particular, (a + b) * X^n * Y^m = a * X^n * Y^m + b * X^n * Y^m.

theorem Polynomial.Bivariate.monomialXY_mul_monomialXY {F : Type} [Semiring F] {n m p q : ℕ} {a b : F} : (monomialXY n m) a * (monomialXY p q) b = (monomialXY (n + p) (m + q)) (a * b)

Multiplying bivariate monomials works as expected. In particular, (a * X^n * Y^m) * (b * X^p * Y^q) = (a * b) * X^(n+p) * Y^(m+q).

@[simp]

theorem Polynomial.Bivariate.monomialXY_pow {F : Type} [Semiring F] {n m k : ℕ} {a : F} : (monomialXY n m) a ^ k = (monomialXY (n * k) (m * k)) (a ^ k)

Taking a bivariate monomial to a power works as expected. In particular, (a * X^n * Y^m)^k = (a^k) * X^(n * k) * Y^(m * k).

@[simp]

theorem Polynomial.Bivariate.smul_monomialXY {F : Type} [Semiring F] {n m : ℕ} {a : F} {S : Type u_1} [SMulZeroClass S F] {b : S} : (monomialXY n m) (b • a) = b • (monomialXY n m) a

Multiplying a bivariate monomial by a scalar works as expected. In particular, b * a * X^n * Y^m = b * (a * X^n * Y^m).

@[simp]

theorem Polynomial.Bivariate.monomialXY_eq_zero_iff {F : Type} [Semiring F] {n m : ℕ} {a : F} : (monomialXY n m) a = 0 ↔ a = 0

A bivariate monimial a * X^n * Y^m is equal to zero if and only if a = 0.

theorem Polynomial.Bivariate.monomialXY_eq_monomialXY_iff {F : Type} [Semiring F] {n m p q : ℕ} {a b : F} : (monomialXY n m) a = (monomialXY p q) b ↔ n = p ∧ m = q ∧ a = b ∨ a = 0 ∧ b = 0

Two bivariate monomials a * X^n * Y^m and b * X^p * Y^q are equal if and only if a = b n = p and m = q or if both are zero, i.e., a = b = 0.

@[simp]

theorem Polynomial.Bivariate.totalDegree_monomialXY {F : Type} [Semiring F] {n m : ℕ} {a : F} (ha : a ≠ 0) : totalDegree ((monomialXY n m) a) = n + m

The total degree of the monomial a * X^n * Y^m is n + m.

@[simp]

theorem Polynomial.Bivariate.degreeX_monomialXY {F : Type} [Semiring F] {n m : ℕ} {a : F} (ha : a ≠ 0) : degreeX ((monomialXY n m) a) = n

The X-degree of the monomial a * X^n * Y^m is n.

@[simp]

theorem Polynomial.Bivariate.degreeY_monomialXY {F : Type} [Semiring F] {n m : ℕ} {a : F} (ha : a ≠ 0) : natDegreeY ((monomialXY n m) a) = m

The Y-degree of the monomial a * X^n * Y^m is m.

noncomputable def Polynomial.Bivariate.weightedDegreeMonomialXY {n m : ℕ} (a b t : ℕ) : ℕ

(a,b)-weighted degree of a monomial X^i * Y^j

theorem Polynomial.Bivariate.evalX_mul {F : Type} [CommSemiring F] (x : F) (f g : Polynomial (Polynomial F)) : evalX x (f * g) = evalX x f * evalX x g

evalX is multiplicative.