Euler's q-exponential identities

Two classical specializations of the Cauchy identity:

1. First Euler identity ($a = 0$): $$\frac{1}{(z;q)_\infty} = \sum_{n \geq 0} \frac{z^n}{(q;q)_n}.$$

2. Second Euler identity (limit of the finite q-binomial theorem): $$(-z;q)_\infty = \sum_{n \geq 0} \frac{q^{\binom{n}{2}}}{(q;q)_n} z^n.$$

Main results

• QSeries.euler_first_identity — the first Euler identity.
• QSeries.euler_second_identity — the second Euler identity.

@[simp]

theorem QSeries.qPochhammer_zero_left {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qPochhammer 0 q n = 1

$(0;q)_n = 1$ for all $n$.

@[simp]

theorem QSeries.qPochhammerInf_zero_left (q : ℂ) : qPochhammerInf 0 q = 1

$(0;q)_\infty = 1$.

theorem QSeries.euler_first_identity {q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : HasSum (fun (n : ℕ) => z ^ n / qPochhammer q q n) (1 / qPochhammerInf z q)

First Euler identity. $$\sum_{n=0}^{\infty} \frac{z^n}{(q;q)_n} = \frac{1}{(z;q)_\infty}$$ for $\|q\| < 1$ and $\|z\| < 1$.

theorem QSeries.sum_pow_choose_two_mul_qBinom_mul_neg_one_pow {R : Type u_1} [CommRing R] (q : R) (n : ℕ) (hn : 0 < n) : ∑ k ∈ Finset.range (n + 1), q ^ k.choose 2 * qBinom n k q * (-1) ^ k = 0

The finite q-binomial theorem specialised to $z = -1$ gives a vanishing alternating sum for every positive $n$.

theorem QSeries.summable_euler_second {q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : Summable fun (n : ℕ) => q ^ n.choose 2 * z ^ n / qPochhammer q q n

The series $\sum_{n \geq 0} q^{\binom{n}{2}} z^n / (q;q)_n$ is summable for $\|q\| < 1$ and $\|z\| < 1$.

theorem QSeries.euler_second_identity {q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : HasSum (fun (n : ℕ) => q ^ n.choose 2 * z ^ n / qPochhammer q q n) (qPochhammerInf (-z) q)

Second Euler identity: for $\|q\|, \|z\| < 1$, the infinite product $(-z;q)_\infty$ equals the series $\sum_{n \geq 0} q^{\binom{n}{2}} z^n / (q;q)_n$.