Generic framework for Pentagonal number theorem

This file partially proves the Pentagonal number theorem for arbitrary topological ring, without concerning about summability, multipliability, or the existence of certain limits.

Complete proof is delegated to Complex.lean and PowerSeries.lean.

Reference: https://math.stackexchange.com/questions/55738/how-to-prove-eulers-pentagonal-theorem-some-hints-will-help

theorem tprod_one_sub_ordererd {ι : Type u_1} {α : Type u_2} [CommRing α] [TopologicalSpace α] [T2Space α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsTopologicalAddGroup α] {f : ι → α} (hsum : Summable fun (i : ι) => f i * ∏ j ∈ Finset.Iio i, (1 - f j)) (hmul : Multipliable fun (x : ι) => 1 - f x) : ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j ∈ Finset.Iio i, (1 - f j)

def Pentagonal.γ {R : Type u_1} [CommRing R] (k n : ℕ) (x : R) : R

We define an auxiliary sequence

$$Γ_N = \sum_{n=0}^{\infty} γ_{k, n} = \sum_{n=0}^{\infty} \left( x^{(k+1)n} \prod_{i=0}^{n} 1 - x^{k + i + 1} \right)$$

Equations

• Pentagonal.γ k n x = x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))

def Pentagonal.ψ {R : Type u_1} [CommRing R] (k n : ℕ) (x : R) : R

And a second auxiliary sequence

$$ ψ_{k, n} = x^{(k+1)n} (x^{2N + n + 3} - 1) \prod_{i=0}^{n-1} 1 - x^{k + i + 2} $$

Equations

• Pentagonal.ψ k n x = x ^ ((k + 1) * n) * (x ^ (2 * k + n + 3) - 1) * ∏ i ∈ Finset.range n, (1 - x ^ (k + i + 2))

theorem Pentagonal.ψ_sub_ψ {R : Type u_1} [CommRing R] (k n : ℕ) (x : R) : γ k n x + x ^ (3 * k + 5) * γ (k + 1) n x = ψ k (n + 1) x - ψ k n x

$γ$ and $ψ$ have relation

$$ γ_{k,n} + x^{3N + 5}γ_{k + 1, n} = ψ_{k, n+1} - ψ_{k, n} $$

theorem Pentagonal.γ_rec {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (k : ℕ) {x : R} (hx : IsTopologicallyNilpotent x) (hγ : ∀ (k : ℕ), Summable fun (x_1 : ℕ) => γ k x_1 x) (h : ∀ (k : ℕ), Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1)) : ∑' (n : ℕ), γ k n x = 1 - x ^ (2 * k + 3) - x ^ (3 * k + 5) * ∑' (n : ℕ), γ (k + 1) n x

By summing with telescoping, we get a recurrence formlua for $Γ$

$$ Γ_{k} = 1 - x^{2N + 3} - x^{3N + 5}Γ_{k + 1} $$

theorem Pentagonal.pentagonalLhs_γ0 {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R} (hγ : ∀ (k : ℕ), Summable fun (x_1 : ℕ) => γ k x_1 x) (h : ∀ (k : ℕ), Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1)) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = 1 - x - x ^ 2 * ∑' (n : ℕ), γ 0 n x

The Euler function is related to $Γ$ by

$$ \prod_{n = 0}^{\infty} 1 - x^{n + 1} = 1 - x - x^2 Γ_0 $$

theorem Pentagonal.pentagonalLhs_γ {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (k : ℕ) {x : R} (hx : IsTopologicallyNilpotent x) (hγ : ∀ (k : ℕ), Summable fun (x_1 : ℕ) => γ k x_1 x) (h : ∀ (k : ℕ), Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1)) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑ k ∈ Finset.range (k + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) + (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) * ∑' (n : ℕ), γ k n x

Applying the recurrence formula repeatedly, we get

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

theorem pentagonalNumberTheorem_generic {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R} (hx : IsTopologicallyNilpotent x) (hγ : ∀ (k : ℕ), Summable fun (x_1 : ℕ) => Pentagonal.γ k x_1 x) (hlhs : ∀ (k : ℕ), Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1)) (hrhs : Summable fun (k : ℕ) => (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))) (htail : Filter.Tendsto (fun (k : ℕ) => (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) * ∑' (n : ℕ), Pentagonal.γ k n x) Filter.atTop (nhds 0)) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))

Taking $k \to \infty$, we get the pentagonal number theorem in the generic form

$$ \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) $$