A bounded integer direction where the highest homogeneous part does not vanish. The direction polynomial packages the top-degree coefficients.

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

Highest homogeneous part, evaluated at outer coordinate one and inner coordinate the polynomial variable.

Equations

• CCDN.leadingDirectionPolynomial f d = ∑ j ∈ Finset.range (d + 1), (Polynomial.monomial j) ((f.coeff (d - j)).coeff j)

theorem CCDN.leadingDirectionPolynomial_coeff {R : Type u_1} [CommRing R] (f : Polynomial (Polynomial R)) (d j : ℕ) : (leadingDirectionPolynomial f d).coeff j = if j ≤ d then (f.coeff (d - j)).coeff j else 0

The j-th coefficient of the leading direction polynomial of degree d is the coefficient of f with outer exponent d - j and inner exponent j when j ≤ d, and zero otherwise.

theorem CCDN.exists_bounded_leading_direction (f : Polynomial (Polynomial ℤ)) (hf : f ≠ 0) : ∃ a ≤ bivariateTotalDegree f, Polynomial.eval (↑a) (leadingDirectionPolynomial f (bivariateTotalDegree f)) ≠ 0

Among 0,...,d, at least one integer parameter gives a nonvanishing leading direction. The proof uses only the univariate root bound.