Pentagonal number theorem #
This is an intermediate file that proves the pentagonal number theorem in a general topological ring
modulo summability and multipliability. The complete proof for formal power series is in
Mathlib/RingTheory/PowerSeries/Pentagonal.lean. TODO: also prove for real/complex numbers.
Declarations #
Pentagonal.tprod_one_sub_pow: pentagonal number theorem with a few summability and multipliability assumptions.
References #
theorem
Pentagonal.tprod_one_sub_pow
{R : Type u_1}
[CommRing R]
[TopologicalSpace R]
[IsTopologicalRing R]
[T2Space R]
{x : R}
(hx : IsTopologicallyNilpotent x)
(hsum : ∀ (k : ℕ), Summable fun (n : ℕ) => x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
(hlhs : ∀ (k : ℕ), Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1))
(hrhs : Summable fun (k : ℕ) => (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1)))
(htail :
Filter.Tendsto
(fun (k : ℕ) =>
(-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) * ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
Filter.atTop (nhds 0))
:
Pentagonal number theorem, assuming appropriate multipliability and summability.
$$ \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) $$