Mathlib-Facing Bivariate Degree Helpers

This file collects degree- and evaluation-oriented helpers for Mathlib's bivariate polynomial surface R[X][Y] that are useful as a bridge layer between CompPoly and downstream developments such as ArkLib.

The intended split is:

• CompPoly/Bivariate/* for the native computable CBivariate representation;
• CompPoly/ToMathlib/* for Mathlib-facing transport and helper lemmas.

noncomputable def Polynomial.Bivariate.coeff {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) (i j : ℕ) : F

(i, j)-coefficient of a polynomial, i.e. the coefficient of X^i Y^j.

noncomputable def Polynomial.Bivariate.leadingCoeffY {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : Polynomial F

The polynomial coefficient of the highest power of Y. This is the leading coefficient in the classical sense if the bivariate polynomial is interpreted as a univariate polynomial over F[X].

@[simp]

theorem Polynomial.Bivariate.leadingCoeffY_eq_zero {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : leadingCoeffY f = 0 ↔ f = 0

The polynomial coefficient of the highest power of Y is 0 if and only if the bivariate polynomial is the zero polynomial.

@[simp]

theorem Polynomial.Bivariate.leadingCoeffY_ne_zero {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : leadingCoeffY f ≠ 0 ↔ f ≠ 0

The polynomial coefficient of the highest power of Y is not 0 if and only if the bivariate polynomial is non-zero.

noncomputable def Polynomial.Bivariate.natDegreeY {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : ℕ

The Y-degree of a bivariate polynomial, as a natural number.

noncomputable def Polynomial.Bivariate.degreeX {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : ℕ

The X-degree of a bivariate polynomial.

noncomputable def Polynomial.Bivariate.totalDegree {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) : ℕ

The total degree of a bivariate polynomial.

noncomputable def Polynomial.Bivariate.weightedDegree {F : Type u_1} [Semiring F] (p : Polynomial (Polynomial F)) (u v : ℕ) : Option ℕ

(u, v)-weighted degree of a polynomial. The maximal u * i + v * j such that the polynomial p contains a monomial x^i * y^j.

noncomputable def Polynomial.Bivariate.natWeightedDegree {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) (u v : ℕ) : ℕ

The natural-number-valued (u, v)-weighted degree.

theorem Polynomial.Bivariate.weightedDegree_ne_none {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) (u v : ℕ) : weightedDegree f u v ≠ none

The weighted degree is always defined (never none).

theorem Polynomial.Bivariate.natWeightedDegree_mem_weight_list {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} {u v : ℕ} : natWeightedDegree f u v ∈ List.map (fun (n : ℕ) => u * (f.coeff n).natDegree + v * n) (List.range f.natDegree.succ)

theorem Polynomial.Bivariate.weight_le_natWeightedDegree_of_lt_natDegree_succ {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} {u v n : ℕ} (hn : n < f.natDegree.succ) : u * (f.coeff n).natDegree + v * n ≤ natWeightedDegree f u v

theorem Polynomial.Bivariate.weightedDegree_eq_natWeightedDegree {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} {u v : ℕ} : weightedDegree f u v = some (natWeightedDegree f u v)

theorem Polynomial.Bivariate.total_deg_as_weighted_deg {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} : totalDegree f = natWeightedDegree f 1 1

The total degree of a bivariate polynomial is equal to the (1, 1)-weighted degree.

theorem Polynomial.Bivariate.degreeX_as_weighted_deg {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} : degreeX f = natWeightedDegree f 1 0

The X-degree of a bivariate polynomial is equal to the (1, 0)-weighted degree.

theorem Polynomial.Bivariate.degreeY_as_weighted_deg {F : Type u_1} [Semiring F] {f : Polynomial (Polynomial F)} : natDegreeY f = natWeightedDegree f 0 1

The Y-degree of a bivariate polynomial is equal to the (0, 1)-weighted degree.

theorem Polynomial.Bivariate.mul_ne_zero {F : Type u_1} [Semiring F] [IsDomain F] (f g : Polynomial (Polynomial F)) (hf : f ≠ 0) (hg : g ≠ 0) : f * g ≠ 0

Over an integral domain, the product of two non-zero bivariate polynomials is non-zero.

@[simp]

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

Over an integral domain, the Y-degree of the product of two non-zero bivariate polynomials is equal to the sum of their degrees.

theorem Polynomial.Bivariate.coeff_natDegree_le_degreeX {F : Type u_1} [Semiring F] (f : Polynomial (Polynomial F)) (n : ℕ) : (f.coeff n).natDegree ≤ degreeX f

theorem Polynomial.Bivariate.degreeX_mul_le {F : Type u_1} [Semiring F] (f g : Polynomial (Polynomial F)) : degreeX (f * g) ≤ degreeX f + degreeX g

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

theorem Polynomial.Bivariate.natDegree_sum_eq_of_unique {F : Type u_1} [Semiring F] {α : Type u_2} {s : Finset α} {f : α → Polynomial F} {deg : ℕ} (mx : α) (hmx : 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.degreeX_mul_ge {F : Type u_1} [Semiring F] [IsDomain F] (f g : Polynomial (Polynomial F)) (hf : f ≠ 0) (hg : g ≠ 0) : degreeX f + degreeX g ≤ degreeX (f * g)

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

noncomputable def Polynomial.Bivariate.evalX {F : Type u_1} [Semiring F] (a : F) (f : Polynomial (Polynomial F)) : Polynomial F

The evaluation at a point of a bivariate polynomial in the first variable X.

noncomputable def Polynomial.Bivariate.evalY {F : Type u_1} [Semiring F] (a : F) (f : Polynomial (Polynomial F)) : Polynomial F

The evaluation at a point of a bivariate polynomial in the second variable Y.

theorem Polynomial.Bivariate.evalX_eq_map {F : Type u_1} [CommSemiring F] (x : F) (f : Polynomial (Polynomial F)) : evalX x f = map (evalRingHom x) f

theorem Polynomial.Bivariate.degreeX_swap {F : Type u_1} [CommRing F] (f : Polynomial (Polynomial F)) : degreeX (swap f) = natDegreeY f

theorem Polynomial.Bivariate.evalY_eq_evalX_swap {F : Type u_1} [CommRing F] (y : F) (f : Polynomial (Polynomial F)) : evalY y f = evalX y (swap f)

theorem Polynomial.Bivariate.natDegreeY_swap {F : Type u_1} [CommRing F] (f : Polynomial (Polynomial F)) : natDegreeY (swap f) = degreeX f

theorem Polynomial.Bivariate.card_evalX_eq_zero_le_degreeX {F : Type u_1} [Field F] [DecidableEq F] (A : Polynomial (Polynomial F)) (hA : A ≠ 0) (P : Finset F) : {x ∈ P | evalX x A = 0}.card ≤ degreeX A

theorem Polynomial.Bivariate.descend_evalX {F : Type u_1} [Field F] {A B G A1 B1 : Polynomial (Polynomial F)} (hA : A = G * A1) (hB : B = G * B1) (x : F) (hx : evalX x G ≠ 0) (q : Polynomial F) (h : evalX x B = q * evalX x A) : evalX x B1 = q * evalX x A1

theorem Polynomial.Bivariate.exists_x_preserve_natDegreeY {F : Type u_1} [Field F] [DecidableEq F] (B : Polynomial (Polynomial F)) (hB : B ≠ 0) (P : Finset F) (hcard : degreeX B < P.card) : ∃ x ∈ P, (evalX x B).natDegree = natDegreeY B

theorem CompPoly.CBivariate.degreeX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : Polynomial.Bivariate.degreeX f.toPoly = f.natDegreeX

The computable X-degree agrees with the Mathlib-facing degreeX after toPoly.

theorem CompPoly.CBivariate.totalDegree_toPoly_spec {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) : Polynomial.Bivariate.totalDegree f.toPoly = f.totalDegree

The computable total degree agrees with the Mathlib-facing total degree after toPoly.

theorem CompPoly.CBivariate.natWeightedDegree_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Ring R] (f : CBivariate R) (u v : ℕ) : Polynomial.Bivariate.natWeightedDegree f.toPoly u v = f.natWeightedDegree u v