Finite geometric products and weighted multiplicity counts

theorem NairTenenbaum.weightedMultiplicity_coordinate_le {ι : Type u_1} [Fintype ι] (w e : ι → ℕ) (hw : ∀ (i : ι), 0 < w i) (i : ι) : e i ≤ ∑ j : ι, w j * e j

noncomputable def NairTenenbaum.weightedMultiplicityBoundEquiv {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (hw : ∀ (i : ι), 0 < w i) {k N : ℕ} (hk : k ≤ N) : { e : ι → ℕ // ∑ i : ι, w i * e i = k } ≃ { e : ι → Fin (N + 1) // ∑ i : ι, w i * ↑(e i) = k }

The equivalence used to count multiplicity vectors of bounded weighted sum.

Equations

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

noncomputable def NairTenenbaum.weightedGeometricPolynomial {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (N : ℕ) : Polynomial ℝ

The finite geometric polynomial encoding weighted multiplicities.

Equations

• NairTenenbaum.weightedGeometricPolynomial w N = ∏ i : ι, ∑ j : Fin (N + 1), Polynomial.X ^ (w i * ↑j)

noncomputable def NairTenenbaum.weightedEulerPolynomial {ι : Type u_1} [Fintype ι] (w : ι → ℕ) : Polynomial ℝ

The product of the linear factors corresponding to the multiplicity weights.

Equations

• NairTenenbaum.weightedEulerPolynomial w = ∏ i : ι, (1 - Polynomial.X ^ w i)

theorem NairTenenbaum.weightedGeometricPolynomial_coeff {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (hw : ∀ (i : ι), 0 < w i) {k N : ℕ} (hk : k ≤ N) : (weightedGeometricPolynomial w N).coeff k = ↑(Nat.card { e : ι → ℕ // ∑ i : ι, w i * e i = k })

theorem NairTenenbaum.weightedGeometricPolynomial_mul_euler {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (N : ℕ) : weightedGeometricPolynomial w N * weightedEulerPolynomial w = ∏ i : ι, (1 - Polynomial.X ^ (w i * (N + 1)))

theorem NairTenenbaum.weightedGeometricPolynomial_mul_euler_coeff {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (hw : ∀ (i : ι), 0 < w i) {k N : ℕ} (hk : k ≤ N) : (weightedGeometricPolynomial w N * weightedEulerPolynomial w).coeff k = (Polynomial.coeff 1) k