Euler's pentagonal number theorem

Euler's pentagonal number theorem states that for $\|q\| < 1$: $$\prod_{n=1}^{\infty} (1 - q^n) = \sum_{k \in \mathbb{Z}} (-1)^k q^{k(3k-1)/2}$$

This follows from the Jacobi triple product by the substitution $q \to q^3$, $z \to q$, using the index partition $\{3n\} \cup \{3n-2\} \cup \{3n-1\} = \mathbb{Z}_{\geq 1}$.

Main definitions

• QSeries.pentagonal — the generalized pentagonal number $\omega(k) = k(3k-1)/2$.

Main results

• QSeries.euler_pentagonal_number — the pentagonal number theorem.

def QSeries.pentagonal (k : ℤ) : ℕ

The $k$-th generalized pentagonal number $\omega(k) = k(3k-1)/2$, well-defined for $k \in \mathbb{Z}$ (the product $k(3k-1)$ is always even).

Equations

• QSeries.pentagonal k = (k * (3 * k - 1) / 2).toNat

theorem QSeries.euler_pentagonal_number {q : ℂ} (hq : ‖q‖ < 1) : qPochhammerInf q q = ∑' (k : ℕ), (-1) ^ k * q ^ pentagonal ↑k + ∑' (k : ℕ), (-1) ^ (k + 1) * q ^ pentagonal (-(↑k + 1))

Euler's pentagonal number theorem: for $\|q\| < 1$, the infinite product $(q;q)_\infty$ equals the bilateral series $\sum_{k \in \mathbb{Z}} (-1)^k q^{\omega(k)}$ over generalized pentagonal numbers $\omega(k) = k(3k-1)/2$, written as two one-sided sums.