Pentagonal number theorem for power series

This file proves the pentagonal number theorem for power series.

theorem Pentagonal.summable_γ_powerSeries (R : Type u_1) [CommRing R] [TopologicalSpace R] (k : ℕ) : Summable fun (x : ℕ) => γ k x PowerSeries.X

theorem Pentagonal.multipliable_pentagonalLhs_powerSeries' (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] (k : ℕ) : Multipliable fun (n : ℕ) => 1 - PowerSeries.X ^ (n + k + 1)

theorem summable_pentagonalRhs_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : Summable fun (k : ℕ) => (-1) ^ k * (PowerSeries.X ^ (k * (3 * k + 1) / 2) - PowerSeries.X ^ ((k + 1) * (3 * k + 2) / 2))

theorem pentagonalNumberTheorem_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : ∏' (n : ℕ), (1 - PowerSeries.X ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (PowerSeries.X ^ (k * (3 * k + 1) / 2) - PowerSeries.X ^ ((k + 1) * (3 * k + 2) / 2))

Pentagonal number theorem for formal power series, summation over natural numbers.

$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = \sum_{k=0}^{\infty} (-1)^k \left(x^{k(3k+1)/2} + x^{(k+1)(3k+2)/2}\right) $$

theorem summable_pentagonalRhs_intNeg_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : Summable fun (k : ℤ) => ↑↑k.negOnePow * PowerSeries.X ^ (k * (3 * k + 1) / 2).toNat

theorem pentagonalNumberTheorem_intNeg_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : ∏' (n : ℕ), (1 - PowerSeries.X ^ (n + 1)) = ∑' (k : ℤ), ↑↑k.negOnePow * PowerSeries.X ^ (k * (3 * k + 1) / 2).toNat

Pentagonal number theorem for formal power series, summation over integers, opposite order.

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

theorem summable_pentagonalRhs_intPos_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : Summable fun (k : ℤ) => ↑↑k.negOnePow * PowerSeries.X ^ (k * (3 * k - 1) / 2).toNat

theorem pentagonalNumberTheorem_intPos_powerSeries (R : Type u_1) [CommRing R] [Nontrivial R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] : ∏' (n : ℕ), (1 - PowerSeries.X ^ (n + 1)) = ∑' (k : ℤ), ↑↑k.negOnePow * PowerSeries.X ^ (k * (3 * k - 1) / 2).toNat

Pentagonal number theorem for formal power series, summation over integers, classic order.

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