Eventual inequalities compare the degree and leading coefficient of Hilbert polynomials.

theorem CCDN.leadingCoeff_nonneg_of_eventual_nat_eval_nonneg (P : Polynomial ℚ) (hP : ∃ (N : ℕ), ∀ n ≥ N, 0 ≤ Polynomial.eval (↑n) P) : 0 ≤ P.leadingCoeff

A rational polynomial that is eventually nonnegative on the natural numbers has nonnegative leading coefficient.

theorem CCDN.polynomial_natDegree_le_of_eventual_nat_eval_le (P Q : Polynomial ℚ) (hP : 0 < P.leadingCoeff) (hle : ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P ≤ Polynomial.eval (↑n) Q) : P.natDegree ≤ Q.natDegree

If P has positive leading coefficient and P(n) ≤ Q(n) for all large n, then deg P ≤ deg Q.

theorem CCDN.polynomial_leadingCoeff_le_of_eventual_nat_eval_le (P Q : Polynomial ℚ) (hP : 0 < P.leadingCoeff) (hQ : 0 < Q.leadingCoeff) (hd : P.natDegree = Q.natDegree) (hle : ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P ≤ Polynomial.eval (↑n) Q) : P.leadingCoeff ≤ Q.leadingCoeff

If P and Q have the same degree and positive leading coefficients and P(n) ≤ Q(n) for all large n, then the leading coefficient of P is at most that of Q.

theorem CCDN.filteredHilbertPolynomial_leadingCoeff_pos {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) : 0 < (filteredHilbertPolynomial I).leadingCoeff

The filtered Hilbert polynomial of a proper ideal has positive leading coefficient.

theorem CCDN.filteredHilbertPolynomial_natDegree_le {K : Type u_1} {L : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field L] [Fintype σ] [Fintype τ] [LinearOrder σ] [LinearOrder τ] (I : Ideal (MvPolynomial σ K)) (J : Ideal (MvPolynomial τ L)) (hI : I ≠ ⊤) (hle : ∀ (N : ℕ), Module.finrank K ↥(filteredCoordinateSpace I N) ≤ Module.finrank L ↥(filteredCoordinateSpace J N)) : (filteredHilbertPolynomial I).natDegree ≤ (filteredHilbertPolynomial J).natDegree

Any filtered-dimension inequality between proper polynomial quotients compares their Hilbert dimensions.

theorem CCDN.filteredHilbertPolynomial_leadingCoeff_le {K : Type u_1} {L : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field L] [Fintype σ] [Fintype τ] [LinearOrder σ] [LinearOrder τ] (I : Ideal (MvPolynomial σ K)) (J : Ideal (MvPolynomial τ L)) (hI : I ≠ ⊤) (hJ : J ≠ ⊤) (hd : (filteredHilbertPolynomial I).natDegree = (filteredHilbertPolynomial J).natDegree) (hle : ∀ (N : ℕ), Module.finrank K ↥(filteredCoordinateSpace I N) ≤ Module.finrank L ↥(filteredCoordinateSpace J N)) : (filteredHilbertPolynomial I).leadingCoeff ≤ (filteredHilbertPolynomial J).leadingCoeff

When dimensions agree, filtered comparison also compares the leading coefficients, and hence the geometric multiplicities.