Pentagonal number theorem for real/complex numbers

This file proves the pentagonal number theorem for real/complex numbers.

theorem Pentagonal.γ_bound {K : Type u_1} [RCLike K] (k n : ℕ) {x : K} (hx : ‖x‖ < 1) : ‖γ k n x‖ ≤ ‖x‖ ^ ((k + 1) * n) * ∏' (i : ℕ), (1 + ‖x‖ ^ i)

theorem Pentagonal.summable_γ_complex {K : Type u_1} [RCLike K] (k : ℕ) {x : K} (hx : ‖x‖ < 1) : Summable fun (x_1 : ℕ) => γ k x_1 x

theorem Pentagonal.tsum_γ_bound {K : Type u_1} [RCLike K] (k : ℕ) {x : K} (hx : ‖x‖ < 1) : ‖∑' (n : ℕ), γ k n x‖ ≤ (1 - ‖x‖)⁻¹ * ∏' (i : ℕ), (1 + ‖x‖ ^ i)

theorem Pentagonal.multipliable_pentagonalLhs_complex' {K : Type u_1} [RCLike K] (k : ℕ) {x : K} (hx : ‖x‖ < 1) : Multipliable fun (n : ℕ) => 1 - x ^ (n + k + 1)

theorem multipliable_pentagonalLhs_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : Multipliable fun (n : ℕ) => 1 - x ^ (n + 1)

theorem summable_pentagonalRhs_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : Summable fun (k : ℕ) => (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))

theorem pentagonalNumberTheorem_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2))

Pentagonal number theorem for real/complex numbers, 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_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : Summable fun (k : ℤ) => (-1) ^ k * x ^ (k * (3 * k + 1) / 2)

theorem pentagonalNumberTheorem_intNeg_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℤ), (-1) ^ k * x ^ (k * (3 * k + 1) / 2)

Pentagonal number theorem for real/complex numbers, 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_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : Summable fun (k : ℤ) => (-1) ^ k * x ^ (k * (3 * k - 1) / 2)

theorem pentagonalNumberTheorem_intPos_complex {K : Type u_1} [RCLike K] {x : K} (hx : ‖x‖ < 1) : ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℤ), (-1) ^ k * x ^ (k * (3 * k - 1) / 2)

Pentagonal number theorem for real/complex numbers, summation over integers, classic order.

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