Euler function and pentagonal number theorem

This file proves the pentagonal number theorem for $‖x‖ < 1$ in a complete normed ring (e.g. ℂ):

$$ \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 Euler function eulerFunction, defined as a power series whose coefficients are related to pentagonal numbers. We then show that this function is equal to both sides.

Main theorems

• eulerFunction_eq_tprod: eulerFunction is equal to the infinite product on the left-hand side.
• eulerFunction_eq_tsum_pentagonal: eulerFunction is equal to the infinite sum on the right-hand side.

References

• https://en.wikipedia.org/wiki/Euler_function

noncomputable def eulerFunction {R : Type u_1} [NormedCommRing R] (x : R) : R

The Euler function $\phi(x) = \sum_{k=-\infty}^{\infty}(-1)^k x^{k (3k - 1) / 2}$, defined as a power series with the same coefficients as PowerSeries.pentagonalSeries. See eulerFunction_eq_tsum_pentagonal for the expression using pentagonal numbers.

Equations

• eulerFunction x = ∑' (n : ℕ), (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R) * x ^ n

theorem eulerFunction_def {R : Type u_1} [NormedCommRing R] (x : R) : eulerFunction x = ∑' (n : ℕ), (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R) * x ^ n

theorem eulerFunction_eq_tsum_pentagonal {R : Type u_1} [NormedCommRing R] (x : R) : eulerFunction x = ∑' (k : ℤ), ↑↑k.negOnePow * x ^ pentagonal k

theorem hasSum_eulerFunction_pentagonalSeries {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : HasSum (fun (n : ℕ) => (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R) * x ^ n) (eulerFunction x)

theorem hasSum_eulerFunction_pentagonal {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : HasSum (fun (k : ℤ) => ↑↑k.negOnePow * x ^ pentagonal k) (eulerFunction x)

theorem hasSum_eulerFunction_pentagonal_pair {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : HasSum (fun (k : ℕ) => (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))) (eulerFunction x)

theorem eulerFunction_eq_tsum_pentagonal_pair {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : eulerFunction x = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))

theorem eulerFunction_eq_tprod {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : eulerFunction x = ∏' (n : ℕ), (1 - x ^ (n + 1))

Pentagonal number theorem for Euler function, expressed as an infinite product. See eulerFunction_eq_tsum_pentagonal that expresses eulerFunction as an infinite sum.

theorem hasProd_eulerFunction {R : Type u_1} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] {x : R} (hx : ‖x‖ < 1) : HasProd (fun (n : ℕ) => 1 - x ^ (n + 1)) (eulerFunction x)

Pentagonal number theorem for Euler function, expressed as an infinite product. See hasSum_eulerFunction_pentagonal that expresses eulerFunction as an infinite sum.