Degree bounds for products and sums of products of polynomials

Mathlib's Polynomial.degree_mul_le bounds the degree of a product by the sum of the degrees. This file records the strict form with one factor of degree below a natural number a and the other of natDegree at most n: the product has degree below a + n. Stating the bound with degree on the strict side lets the zero polynomial through on either side, which is what a coefficient window of prescribed length needs when it is read off polynomials that may vanish.

TauCeti.degree_mul_add_mul_lt_of_degree_lt_of_natDegree_le combines two such product bounds into the coefficient window used for polynomial relations with formal degree bounds m and n.

theorem Polynomial.degree_mul_lt_of_degree_lt_of_natDegree_le {R : Type u_1} [Semiring R] {A q : Polynomial R} {a n : ℕ} (hA : A.degree < ↑a) (hq : q.natDegree ≤ n) : (A * q).degree < ↑(a + n)

The product of a polynomial of degree below a with one of degree at most n has degree below a + n; the zero polynomial is allowed on either side.

theorem TauCeti.degree_mul_add_mul_lt_of_degree_lt_of_natDegree_le {R : Type u_1} [Semiring R] {p q A B : Polynomial R} {m n j : ℕ} (hm : p.natDegree ≤ m) (hn : q.natDegree ≤ n) (hjm : j ≤ m) (hjn : j ≤ n) (hA : A.degree < ↑(m - j)) (hB : B.degree < ↑(n - j)) : (A * q + B * p).degree < ↑(m - j + (n - j) + j)

A relation with multipliers of degrees below m - j and n - j has degree below (m - j) + (n - j) + j, provided the input degrees are bounded by m and n and j lies below both bounds. Either input or multiplier may be zero.