Products of the series 1 - X ^ d

For a finite family of positive integers d i, the product ∏ i, (1 - X ^ d i) is invertible in R⟦X⟧, and its inverse ∏ i, (1 - X ^ d i)⁻¹ counts the solutions of ∑ i, e i * d i = n in natural numbers: its n-th coefficient is the number of e : ι →₀ ℕ of weight n for the weights d (Finsupp.weight d e = n). This is the Hilbert series of a polynomial algebra whose generators have the degrees d i.

Conversely, the product ∏ i, (1 - X ^ d i) determines the multiset of the positive integers d i, over any coefficient ring of characteristic zero. If every exponent is at least n > 0, the coefficient of X ^ n in the product is minus the number of exponents equal to n; applied to the least exponent occurring in either of two equal products, this lets one cancel a common factor and induct. So the counting functions n ↦ #{e | Finsupp.weight d e = n} determine the multiset of the weights d i.

Main results

• PowerSeries.coeff_prod_expand_mk_one: the n-th coefficient of ∏ c ∈ s, (1 - X ^ m c)⁻¹, written as the product of the expanded geometric series, is the size of the weighted antidiagonal.
• PowerSeries.mk_natCard_weight_mul_prod_one_sub_X_pow: the series counting the e : ι →₀ ℕ of each weight for positive weights d is the inverse of ∏ i, (1 - X ^ d i).
• Multiset.eq_of_prod_map_one_sub_X_pow_eq: the product ∏ d ∈ s, (1 - X ^ d) over a multiset s of positive integers determines s, in characteristic zero.
• Multiset.map_univ_eq_of_natCard_weight_eq: the counting functions of the weights determine the multiset of the weights.

theorem PowerSeries.expand_mk_one_mul_one_sub_X_pow {R : Type u_1} [CommRing R] (p : ℕ) (hp : p ≠ 0) : (expand p hp) (mk 1) * (1 - X ^ p) = 1

The expanded geometric series. ∑ X ^ (p * k) inverts 1 - X ^ p.

theorem PowerSeries.coeff_prod_expand_mk_one {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (m : ι → ℕ+) (n : ℕ) : (coeff n) (∏ c ∈ s, (expand ↑(m c) ⋯) (mk 1)) = ↑(s.weightedFinsuppAntidiag m n).card

The n-th coefficient of the product of the expanded geometric series ∑ X ^ (m c * k), that is of ∏ c ∈ s, (1 - X ^ m c)⁻¹, is the number of l supported in s with ∑ c ∈ s, m c * l c = n.

theorem PowerSeries.mk_natCard_weight_mul_prod_one_sub_X_pow {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] {d : ι → ℕ} (hd : ∀ (i : ι), d i ≠ 0) : (mk fun (n : ℕ) => ↑(Nat.card { e : ι →₀ ℕ // (Finsupp.weight d) e = n })) * ∏ i : ι, (1 - X ^ d i) = 1

Counting solutions of ∑ i, e i * d i = n. For positive weights d i, the series whose n-th coefficient is the number of e : ι →₀ ℕ of weight n is the inverse of ∏ i, (1 - X ^ d i).

theorem PowerSeries.coeff_prod_map_one_sub_X_pow_of_le {R : Type u_1} [CommRing R] {n : ℕ} (hn : n ≠ 0) {s : Multiset ℕ} (hs : ∀ d ∈ s, n ≤ d) : (coeff n) (Multiset.map (fun (d : ℕ) => 1 - X ^ d) s).prod = -↑(Multiset.count n s)

If every exponent in the multiset s is at least n > 0, the coefficient of X ^ n in ∏ d ∈ s, (1 - X ^ d) is minus the number of exponents equal to n.

theorem Multiset.eq_of_prod_map_one_sub_X_pow_eq {R : Type u_1} [CommRing R] [CharZero R] {s t : Multiset ℕ} (hs : 0 ∉ s) (ht : 0 ∉ t) (h : (map (fun (d : ℕ) => 1 - PowerSeries.X ^ d) s).prod = (map (fun (d : ℕ) => 1 - PowerSeries.X ^ d) t).prod) : s = t

The exponents of ∏ (1 - X ^ d). Over a coefficient ring of characteristic zero, the product ∏ d ∈ s, (1 - X ^ d) determines the multiset s of positive integers.

theorem Multiset.map_univ_eq_of_natCard_weight_eq {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] {d : ι → ℕ} {d' : κ → ℕ} (hd : ∀ (i : ι), d i ≠ 0) (hd' : ∀ (i : κ), d' i ≠ 0) (h : ∀ (n : ℕ), Nat.card { e : ι →₀ ℕ // (Finsupp.weight d) e = n } = Nat.card { e : κ →₀ ℕ // (Finsupp.weight d') e = n }) : map d Finset.univ.val = map d' Finset.univ.val

Weights from their counting functions. If two finite families of positive weights have the same number of e of each weight n, then they have the same multiset of weights.