Pentagonal number theorem for power series

This file proves the pentagonal number theorem for power series:

$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) = \sum_{k=-\infty}^{\infty} (-1)^k x^{a_k} $$

where $a_k = k(3k - 1)/2$ are the pentagonal numbers. We state the theorem in two parts by introducing the intermediate power series PowerSeries.pentagonalSeries, whose coefficients are defined using pentagonal numbers. We then show that this series is equal to both sides.

Main theorems

• PowerSeries.WithPiTopology.hasProd_one_sub_X_pow: PowerSeries.pentagonalSeries is equal to infinite product on the left-hand side of the formula.
• PowerSeries.coeff_prod_one_sub_X_pow_eventually_eq restates the left-hand side without requiring topology.
• PowerSeries.WithPiTopology.hasSum_pentagonalSeries: PowerSeries.pentagonalSeries is equal to the infinite sum on the right-hand side of the formula.
• PowerSeries.coeff_pentagonalSeries restates the right-hand side without requiring topology.

noncomputable def PowerSeries.pentagonalSeries (R : Type u_1) [CommRing R] : PowerSeries R

The power series $\sum_{k=-\infty}^{\infty}(-1)^k x^{k * (3k - 1) / 2}$.

Equations

• PowerSeries.pentagonalSeries R = PowerSeries.mk fun (n : ℕ) => if h : ∃ (k : ℤ), pentagonal k = n then ↑↑h.choose.negOnePow else 0

theorem PowerSeries.coeff_pentagonalSeries_eq_zero (R : Type u_1) [CommRing R] {n : ℕ} (h : n ∉ Set.range pentagonal) : (coeff n) (pentagonalSeries R) = 0

@[simp]

theorem PowerSeries.coeff_pentagonalSeries_pentagonal (R : Type u_1) [CommRing R] (k : ℤ) : (coeff (pentagonal k)) (pentagonalSeries R) = ↑↑k.negOnePow

@[simp]

theorem PowerSeries.coeff_pentagonalSeries_eq_zero_iff (R : Type u_1) [CommRing R] [Nontrivial R] {n : ℕ} : (coeff n) (pentagonalSeries R) = 0 ↔ n ∉ Set.range pentagonal

theorem PowerSeries.WithPiTopology.hasSum_pentagonalSeries (R : Type u_1) [CommRing R] [TopologicalSpace R] : HasSum (fun (k : ℤ) => ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)

PowerSeries.pentagonalSeries as an infinite sum over integers

theorem PowerSeries.WithPiTopology.pentagonalSeries_eq_tsum (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] : pentagonalSeries R = ∑' (k : ℤ), ↑↑k.negOnePow * X ^ pentagonal k

theorem PowerSeries.WithPiTopology.hasSum_pow_pentagonal_sub_pentagonalSeries (R : Type u_1) [CommRing R] [TopologicalSpace R] : HasSum (fun (k : ℕ) => (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))) (pentagonalSeries R)

PowerSeries.pentagonalSeries as an infinite sum over natural numbers. In this version, terms are ordered by strictly increasing exponent pentagonal k for k = 0, 1, -1, 2, -2, 3, ..., and every two terms are grouped together.

theorem PowerSeries.WithPiTopology.pentagonalSeries_eq_tsum_pow_pentagonal_sub (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] : pentagonalSeries R = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

theorem PowerSeries.coeff_prod_one_sub_X_pow_eventually_eq (R : Type u_1) [CommRing R] (n : ℕ) : ∀ᶠ (s : Finset ℕ) in Filter.atTop, (coeff n) (∏ n ∈ s, (1 - X ^ (n + 1))) = (coeff n) (pentagonalSeries R)

Pentagonal number theorem for power series, expressed as the statement that the coefficients of the product ∏ n, 1 - X ^ (n + 1) are eventually constants as (pentagonalSeries R).coeff.

theorem PowerSeries.WithPiTopology.hasProd_one_sub_X_pow (R : Type u_1) [CommRing R] [TopologicalSpace R] : HasProd (fun (n : ℕ) => 1 - X ^ (n + 1)) (pentagonalSeries R)

Pentagonal number theorem for power series, expressed as an infinite product. See also PowerSeries.WithPiTopology.hasSum_pentagonalSeries that expresses pentagonalSeries as an infinite sum.

theorem PowerSeries.WithPiTopology.tprod_one_sub_X_pow (R : Type u_1) [CommRing R] [TopologicalSpace R] [T2Space R] : ∏' (n : ℕ), (1 - X ^ (n + 1)) = pentagonalSeries R