Mathlib-Facing Bivariate Weighted-Degree Helpers

This file extends Polynomial.Bivariate with weighted-degree algebra that is generic and reusable across downstream protocol developments.

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

The monomial X^i Y^j as a bivariate polynomial.

theorem Polynomial.Bivariate.natWeightedDegree_add_le {F : Type u_1} [Semiring F] (p q : Polynomial (Polynomial F)) (u v : ℕ) : natWeightedDegree (p + q) u v ≤ max (natWeightedDegree p u v) (natWeightedDegree q u v)

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

theorem Polynomial.Bivariate.natWeightedDegree_sum_le {F : Type u_1} [Semiring F] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial (Polynomial F)) (u v : ℕ) : natWeightedDegree (∑ i ∈ s, f i) u v ≤ s.sup fun (i : ι) => natWeightedDegree (f i) u v

The weighted degree of a sum is bounded by the supremum of the weighted degrees.

theorem Polynomial.Bivariate.natWeightedDegree_smul_le {F : Type u_1} [Semiring F] (a : F) (p : Polynomial (Polynomial F)) (u v : ℕ) : natWeightedDegree (a • p) u v ≤ natWeightedDegree p u v

The weighted degree of a scalar multiple is at most the weighted degree of the polynomial.

theorem Polynomial.Bivariate.degree_eval_le_weightedDegree {F : Type u_1} [Semiring F] (Q : Polynomial (Polynomial F)) (P : Polynomial F) (k : ℕ) (hP : P.natDegree ≤ k - 1) : (eval P Q).natDegree ≤ natWeightedDegree Q 1 (k - 1)

The degree of Q(X, P(X)) is bounded by the weighted degree of Q, provided deg(P) ≤ k - 1.

theorem Polynomial.Bivariate.natWeightedDegree_monomial {F : Type u_1} [Semiring F] [Nontrivial F] (i j u v : ℕ) : natWeightedDegree (monomial i j) u v = u * i + v * j

The weighted degree of X^i Y^j is u * i + v * j.