The maximal orthants determine the leading term of the Hilbert polynomial. In particular its factorial-normalized leading coefficient is a positive integer, counted by cells of the standard-exponent partition.

theorem CCDN.sum_preHilbertPoly_leading {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (dim shift : ι → ℕ) : have m := s.sup dim; have d := {i ∈ s | dim i = m}.card; have P := ∑ i ∈ s, Polynomial.preHilbertPoly ℚ (dim i) (shift i); 0 < d ∧ P.natDegree = m ∧ P.leadingCoeff = ↑d / ↑m.factorial

A nonempty sum of shifted binomial polynomials of dimensions dim i has degree the maximal dimension m and leading coefficient d / m!, where d > 0 is the number of summands of maximal dimension.

noncomputable def CCDN.lowerSetOrthantPatterns {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (B : ℕ) : Finset (σ → Fin (B + 1))

The cells b ∈ {0, …, B}^σ of the clamped orthant partition that lie in S.

Equations

• CCDN.lowerSetOrthantPatterns S B = {b : σ → Fin (B + 1) | (fun (i : σ) => ↑(b i)) ∈ S}

theorem CCDN.lowerSetOrthantPolynomial_eq_sum {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (B : ℕ) : lowerSetOrthantPolynomial S B = ∑ b ∈ lowerSetOrthantPatterns S B, Polynomial.preHilbertPoly ℚ (Fintype.card (orthantFree b)) (orthantBaseDegree b)

The orthant polynomial of S is the sum, over the cells of S, of the shifted binomial polynomials of the corresponding orthants.

theorem CCDN.lowerSet_eventually_polynomial_positive {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (hS : IsLowerSet S) (hSne : S.Nonempty) : ∃ (P : Polynomial ℚ) (d : ℕ), 0 < d ∧ P.natDegree ≤ Fintype.card σ ∧ P.leadingCoeff = ↑d / ↑P.natDegree.factorial ∧ ∃ (N : ℕ), ∀ n ≥ N, Polynomial.eval (↑n) P = ↑(Nat.card { a : σ → ℕ // a ∈ S ∧ ∑ i : σ, a i ≤ n })

A nonempty lower set has a positive integer multiplicity and an eventual polynomial of degree at most the number of exponent coordinates.