Counting the finite orthant partition gives an eventual polynomial for every lower set of exponent vectors, in arbitrary finite dimension.

noncomputable def CCDN.boundedExponentVectorEquivSym (σ : Type u_1) [Fintype σ] (N : ℕ) : { a : σ → ℕ // ∑ i : σ, a i ≤ N } ≃ Sym (Option σ) N

The bijection between exponent vectors in σ → ℕ of total degree at most N and multisets of size N on Option σ.

Equations

• CCDN.boundedExponentVectorEquivSym σ N = (Sym.equivNatSumLeOfFintype σ N).symm

instance CCDN.finite_boundedExponentVectors {σ : Type u_1} [Fintype σ] (N : ℕ) : Finite { a : σ → ℕ // ∑ i : σ, a i ≤ N }

instance CCDN.finite_boundedLowerExponents {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (N : ℕ) : Finite { a : σ → ℕ // a ∈ S ∧ ∑ i : σ, a i ≤ N }

noncomputable def CCDN.lowerSetOrthantPolynomial {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (B : ℕ) : Polynomial ℚ

The orthant polynomial is a finite positive sum of shifted binomial polynomials. Its coefficients are rational, while its large integer values count exponent vectors exactly.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.lowerSetOrthantPolynomial_eval {σ : Type u_1} [Fintype σ] (S : Set (σ → ℕ)) (B : ℕ) (hstable : ∀ (a : σ → ℕ), a ∈ S ↔ clampExponent B a ∈ S) (N : ℕ) (hN : Fintype.card σ * B ≤ N) : Polynomial.eval (↑N) (lowerSetOrthantPolynomial S B) = ↑(Nat.card { a : σ → ℕ // a ∈ S ∧ ∑ i : σ, a i ≤ N })

If membership in S is determined by clamping exponents at B, then for N ≥ |σ| · B the orthant polynomial of S evaluated at N counts the vectors of S of total degree at most N.

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

Every lower exponent set has an eventual counting polynomial. The threshold and the polynomial are constructed from its finite orthant partition.