Total degree of nested bivariate polynomials, transported from the multivariate polynomial ring. This controls the support of factor forms.

noncomputable def CCDN.bivariatePolynomialEquiv (R : Type u_1) [CommRing R] : MvPolynomial (Fin 2) R ≃ₐ[R] Polynomial (Polynomial R)

The identification of polynomials in two variables with nested polynomials R[X][X]: variable zero is the outer variable, and variable one is the inner one.

Equations

• CCDN.bivariatePolynomialEquiv R = (MvPolynomial.finSuccEquiv R 1).trans (Polynomial.mapAlgEquiv (MvPolynomial.uniqueAlgEquiv R (Fin 1)))

theorem CCDN.bivariatePolynomialEquiv_coeff {R : Type u_1} [CommRing R] (f : MvPolynomial (Fin 2) R) (i j : ℕ) : (((bivariatePolynomialEquiv R) f).coeff i).coeff j = f.coeff (Finsupp.cons i (Finsupp.single 0 j))

The coefficient with outer exponent i and inner exponent j of the nested polynomial associated with f is the coefficient of f at the exponent vector (i, j).

theorem CCDN.bivariate_exponent_eq (m : Fin 2 →₀ ℕ) : m = Finsupp.cons (m 0) (Finsupp.single 0 (m 1))

Every exponent vector in two variables is Finsupp.cons of its two components.

theorem CCDN.bivariate_exponent_sum (i j : ℕ) : ((Finsupp.cons i (Finsupp.single 0 j)).sum fun (x : Fin (1 + 1)) (e : ℕ) => e) = i + j

The degree of the two-variable exponent vector with components i and j is i + j.

noncomputable def CCDN.bivariateTotalDegree {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) : ℕ

The total degree of a nested bivariate polynomial, with the usual convention that the zero polynomial has natural-valued total degree zero.

Equations

• CCDN.bivariateTotalDegree f = ((CCDN.bivariatePolynomialEquiv R).symm f).totalDegree

theorem CCDN.bivariateTotalDegree_coeff_le {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) (i j : ℕ) (h : (f.coeff i).coeff j ≠ 0) : i + j ≤ bivariateTotalDegree f

If the coefficient of f with outer exponent i and inner exponent j is nonzero, then i + j is at most the total degree of f.

theorem CCDN.bivariateTotalDegree_le_iff {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) (d : ℕ) : bivariateTotalDegree f ≤ d ↔ ∀ (i j : ℕ), (f.coeff i).coeff j ≠ 0 → i + j ≤ d

The total degree of f is at most d if and only if i + j ≤ d whenever the coefficient of f with outer exponent i and inner exponent j is nonzero.

theorem CCDN.bivariateTotalDegree_mul_le {R : Type u_1} [CommRing R] (f g : Polynomial (Polynomial R)) : bivariateTotalDegree (f * g) ≤ bivariateTotalDegree f + bivariateTotalDegree g

The total degree of a product is at most the sum of the total degrees.

theorem CCDN.bivariateTotalDegree_outerDerivative_le {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) : bivariateTotalDegree (Polynomial.derivative f) ≤ bivariateTotalDegree f - 1

Differentiation in the outer variable lowers the total degree by at least one.

theorem CCDN.bivariateTotalDegree_innerDerivative_le {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) : bivariateTotalDegree ((bivariateCoefficientDerivative R) f) ≤ bivariateTotalDegree f - 1

Differentiation in the inner variable lowers the total degree by at least one.

theorem CCDN.inBivariateGrid_of_totalDegree_lt {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) (hd : bivariateTotalDegree f < d) : InBivariateGrid d f

A bivariate polynomial of total degree less than d is supported in the grid of outer and inner exponents less than d.

@[simp]

theorem CCDN.bivariateTotalDegree_zero {R : Type u_1} [CommRing R] : bivariateTotalDegree 0 = 0

The zero polynomial has total degree zero.

theorem CCDN.bivariate_natDegree_le_totalDegree {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) : f.natDegree ≤ bivariateTotalDegree f

The degree in the outer variable is at most the total degree.

theorem CCDN.bivariate_gradient_in_grid {R : Type u_1} [CommRing R] (d : ℕ) (hd : 0 < d) (f : Polynomial (Polynomial R)) (hf : bivariateTotalDegree f ≤ d) : InBivariateGrid d (Polynomial.derivative f) ∧ InBivariateGrid d ((bivariateCoefficientDerivative R) f)

Both components of the gradient fit the grid for a positive total-degree bound, in every characteristic.

theorem CCDN.bivariate_factor_form_in_grid {R : Type u_1} [CommRing R] [IsDomain R] (d : ℕ) (g h : Polynomial (Polynomial R)) (hg : g ≠ 0) (hh : h ≠ 0) (hgdeg : 0 < bivariateTotalDegree g) (hdeg : bivariateTotalDegree (g * h) ≤ d) : InBivariateGrid d (h * Polynomial.derivative g) ∧ InBivariateGrid d (h * (bivariateCoefficientDerivative R) g)

The logarithmic form associated with a nonconstant factor has strictly smaller total degree than the product, so both numerators fit the matrix.

theorem CCDN.bivariate_power_factor_form_in_grid {R : Type u_1} [CommRing R] [IsDomain R] (d k : ℕ) (g h : Polynomial (Polynomial R)) (hg : g ≠ 0) (hh : h ≠ 0) (hgdeg : 0 < bivariateTotalDegree g) (hdeg : bivariateTotalDegree (g ^ (k + 2) * h) ≤ d) : InBivariateGrid d (g ^ k * h * Polynomial.derivative g) ∧ InBivariateGrid d (g ^ k * h * (bivariateCoefficientDerivative R) g)

If g is nonconstant and g ^ (k + 2) * h has total degree at most d, then the products of g ^ k * h with both partial derivatives of g (the numerators of the higher-pole form) fit strictly inside the grid.

theorem CCDN.bivariate_coefficient_natDegree_le_totalDegree {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) (i : ℕ) : (f.coeff i).natDegree ≤ bivariateTotalDegree f

The inner degree of each outer coefficient is at most the total degree.

theorem CCDN.bivariateMap_monic {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) {f : Polynomial (Polynomial R)} (hf : f.Monic) : ((bivariateMap φ) f).Monic

Applying a coefficient ring homomorphism to both levels preserves monicity in the outer variable.

theorem CCDN.bivariateMap_natDegree_of_monic {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] (φ : R →+* S) {f : Polynomial (Polynomial R)} (hf : f.Monic) : ((bivariateMap φ) f).natDegree = f.natDegree

Applying a coefficient ring homomorphism to a polynomial monic in the outer variable preserves its outer degree, provided the target ring is nontrivial.

theorem CCDN.bivariateTotalDegree_map_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : Polynomial (Polynomial R)) : bivariateTotalDegree ((bivariateMap φ) f) ≤ bivariateTotalDegree f

Reduction of coefficients cannot increase the total degree.