Generating functions for partitions

This file defines generating functions related to partitions. Given a character function $f(i, c)$ of a part $i$ and the number of occurrences of the part $c$, the related generating function is $$ G_f(X) = \sum_{n = 0}^{\infty} \left(\sum_{p \in P_{n}} \prod_{i \in p} f(i, \#i)\right) X^n = \prod_{i = 1}^{\infty}\left(1 + \sum_{j = 1}^{\infty} f(i, j) X^{ij}\right) $$ where $P_n$ is all partitions of $n$, $\#i$ is the count of $i$ in the partition $p$. We give the definition Nat.Partition.genFun using the first equation, and prove the second equation in Nat.Partition.hasProd_genFun (with shifted indices).

This generating function can be specialized to

• When $f(i, c) = 1$, this is the generating function for partition function $p(n)$.
• When $f(i, 1) = 1$ and $f(i, c) = 0$ for $c > 1$, this is the generating function for #(Nat.Partition.distincts n).
• When $f(i, c) = 1$ for odd $i$ and $f(i, c) = 0$ for even $i$, this is the generating function for #(Nat.Partition.odds n). (TODO: prove these)

The definition of Nat.Partition.genFun ignores the value of $f(0, c)$ and $f(i, 0)$. The formula can be interpreted as assuming $f(i, 0) = 1$ and $f(0, c) = 0$ for $c \ne 0$. In theory we could respect the actual value of $f(0, c)$ and $f(i, 0)$, but it makes the otherwise finite sum and product potentially infinite.

def Nat.Partition.genFun {R : Type u_1} [CommSemiring R] (f : ℕ → ℕ → R) : PowerSeries R

Generating function associated with character $f(i, c)$ for partition functions, where $i$ is a part of the partition, and $c$ is the count of that part in the partition. The character function is multiplied within one n.Partition, and summed among all n.Partition for a fixed n. This way, each n is assigned a value, which we use as the coefficients of the power series.

See the module docstring of Combinatorics.Enumerative.Partition.GenFun for more details.

Equations

• Nat.Partition.genFun f = PowerSeries.mk fun (n : ℕ) => ∑ p : n.Partition, (Multiset.toFinsupp p.parts).prod f

@[simp]

theorem Nat.Partition.coeff_genFun {R : Type u_1} [CommSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : (PowerSeries.coeff n) (genFun f) = ∑ p : n.Partition, (Multiset.toFinsupp p.parts).prod f

theorem Nat.Partition.summable_genFun_term {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (f : ℕ → ℕ → R) (i : ℕ) : Summable fun (j : ℕ) => f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))

The infinite sum in the formula Nat.Partition.hasProd_genFun always converges.

theorem Nat.Partition.summable_genFun_term' {R : Type u_1} [CommSemiring R] [TopologicalSpace R] (f : ℕ → ℕ → R) {i : ℕ} (hi : i ≠ 0) : Summable fun (j : ℕ) => f i (j + 1) • PowerSeries.X ^ (i * (j + 1))

Alternative form of summable_genFun_term that unshifts the first index.

theorem Nat.Partition.hasProd_genFun {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : HasProd (fun (i : ℕ) => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))) (genFun f)

theorem Nat.Partition.multipliable_genFun {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : Multipliable fun (i : ℕ) => 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1))

theorem Nat.Partition.genFun_eq_tprod {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) : genFun f = ∏' (i : ℕ), (1 + ∑' (j : ℕ), f (i + 1) (j + 1) • PowerSeries.X ^ ((i + 1) * (j + 1)))