The Cauchy identity (infinite q-binomial theorem)

This file proves the infinite q-binomial / Cauchy identity: for $\|q\| < 1$ and $\|z\| < 1$, $$\sum_{n=0}^{\infty} \frac{(a;q)_n}{(q;q)_n} z^n = \frac{(az;q)_\infty}{(z;q)_\infty}.$$

The proof follows Heine's classical functional-equation argument.

Main results

• QSeries.hasSum_qPochhammer_div_mul_pow — the Cauchy identity.

noncomputable def QSeries.cauchyCoeff (a q : ℂ) (n : ℕ) : ℂ

The coefficient sequence $c_n = (a;q)_n / (q;q)_n$.

Equations

• QSeries.cauchyCoeff a q n = QSeries.qPochhammer a q n / QSeries.qPochhammer q q n

@[simp]

theorem QSeries.cauchyCoeff_zero (a q : ℂ) : cauchyCoeff a q 0 = 1

The zeroth Cauchy coefficient $c_0 = 1$.

theorem QSeries.cauchyCoeff_succ_mul {q : ℂ} (hq : ‖q‖ < 1) (a : ℂ) (n : ℕ) : cauchyCoeff a q (n + 1) * (1 - q ^ (n + 1)) = cauchyCoeff a q n * (1 - a * q ^ n)

Coefficient recurrence. $c_{n+1}(1 - q^{n+1}) = c_n(1 - aq^n)$.

theorem QSeries.exists_norm_cauchyCoeff_le {q : ℂ} (hq : ‖q‖ < 1) (a : ℂ) : ∃ (C : ℝ), ∀ (n : ℕ), ‖cauchyCoeff a q n‖ ≤ C

Boundedness of the coefficients.

The quotients (a;q)_n / (q;q)_n converge, hence form a bounded sequence.

theorem QSeries.summable_cauchyCoeff_mul_pow {a q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : Summable fun (n : ℕ) => cauchyCoeff a q n * z ^ n

The series $\sum_n c_n z^n$ is summable for $\|z\| < 1$.

theorem QSeries.one_sub_mul_qPochhammerInf_div_eq (a z : ℂ) {q : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : (1 - z) * (qPochhammerInf (a * z) q / qPochhammerInf z q) = (1 - a * z) * (qPochhammerInf (a * z * q) q / qPochhammerInf (z * q) q)

Functional equation for $G$. $(1-z)\, G(z) = (1 - az)\, G(qz)$.

theorem QSeries.one_sub_mul_tsum_cauchyCoeff_eq {a q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : (1 - z) * ∑' (n : ℕ), cauchyCoeff a q n * z ^ n = (1 - a * z) * ∑' (n : ℕ), cauchyCoeff a q n * (q * z) ^ n

Functional equation for $F$. $(1-z)\, F(z) = (1 - az)\, F(qz)$.

theorem QSeries.mul_qPochhammer_eq_of_functional_eq {H : ℂ → ℂ} {a q : ℂ} (hq : ‖q‖ < 1) (hH : ∀ (w : ℂ), ‖w‖ < 1 → (1 - w) * H w = (1 - a * w) * H (q * w)) {z : ℂ} (hz : ‖z‖ < 1) (n : ℕ) : H z * qPochhammer z q n = H (q ^ n * z) * qPochhammer (a * z) q n

Iterated functional equation.

theorem QSeries.tendsto_tsum_cauchyCoeff_mul_pow {a q z : ℂ} (hq : ‖q‖ < 1) (hz : ‖z‖ < 1) : Filter.Tendsto (fun (n : ℕ) => ∑' (k : ℕ), cauchyCoeff a q k * (q ^ n * z) ^ k) Filter.atTop (nhds 1)

$F(q^n z) \to 1$ as $n \to \infty$, by Tannery's theorem.

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

Infinite q-binomial / Cauchy identity.

For $\|q\| < 1$ and $\|z\| < 1$, $$\sum_{n=0}^{\infty} \frac{(a;q)_n}{(q;q)_n} z^n = \frac{(az;q)_\infty}{(z;q)_\infty}.$$