Key identity for the Jacobi triple product

We prove that for ‖q‖ < 1 and all k ≥ 0:

$$S_k(q) := \sum_{m=0}^{\infty} \frac{q^{m(m+k)}}{(q;q)_m (q;q)_{m+k}} = \frac{1}{(q;q)_\infty}$$

The proof uses a recurrence: S_k - S_{k+1} = q^{k+1} (S_{k+2} - S_{k+1})

This forces all differences to be zero (since S_k → 1/(q;q)∞), so all S_k are equal to 1/(q;q)∞.

noncomputable def QSeries.keySum (q : ℂ) (k : ℕ) : ℂ

The key sum S_k(q) = Σ_{m≥0} q^{m(m+k)} / ((q;q)m (q;q){m+k}).

Equations

• QSeries.keySum q k = ∑' (m : ℕ), q ^ (m * (m + k)) / (QSeries.qPochhammer q q m * QSeries.qPochhammer q q (m + k))

noncomputable def QSeries.keySummand (q : ℂ) (k m : ℕ) : ℂ

The summand of S_k.

Equations

• QSeries.keySummand q k m = q ^ (m * (m + k)) / (QSeries.qPochhammer q q m * QSeries.qPochhammer q q (m + k))

theorem QSeries.keySum_eq_tsum (q : ℂ) (k : ℕ) : keySum q k = ∑' (m : ℕ), keySummand q k m

Unfolds keySum as the tsum of keySummand.

theorem QSeries.exists_pos_le_norm_qPochhammer_self {q : ℂ} (hq : ‖q‖ < 1) : ∃ C > 0, ∀ (n : ℕ), C ≤ ‖qPochhammer q q n‖

The finite q-Pochhammer symbols (q;q)_n are bounded away from 0 uniformly in n, since they converge to the nonzero limit (q;q)_∞.

theorem QSeries.summable_keySummand {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : Summable (keySummand q k)

The series defining $S_k(q)$ is summable for $\|q\| < 1$.

theorem QSeries.tendsto_keySum {q : ℂ} (hq : ‖q‖ < 1) : Filter.Tendsto (keySum q) Filter.atTop (nhds (1 / qPochhammerInf q q))

As $k \to \infty$, $S_k(q)$ converges to $1/(q;q)_\infty$.

theorem QSeries.one_sub_norm_le_norm_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1) {n : ℕ} (hn : 1 ≤ n) : 1 - ‖q‖ ≤ ‖1 - q ^ n‖

For ‖q‖ < 1 and n ≥ 1 the tail factor 1 - qⁿ is bounded away from zero, uniformly in n, by the constant 1 - ‖q‖.

theorem QSeries.summable_pow_div_qPochhammer_succ {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : Summable fun (m : ℕ) => q ^ (m * (m + k)) / (qPochhammer q q m * qPochhammer q q (m + k + 1))

The shifted family q ^ (m * (m + k)) / ((q;q)_m (q;q)_{m+k+1}) is summable: it is keySummand q k scaled by the uniformly bounded factor (1 - q ^ (m+k+1))⁻¹.

theorem QSeries.summable_pow_mul_one_sub_pow_div_qPochhammer {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : Summable fun (m : ℕ) => q ^ (m * (m + k)) * (1 - q ^ m) / (qPochhammer q q m * qPochhammer q q (m + k + 1))

Multiplying the shifted family by the bounded factor 1 - q ^ m preserves summability.

theorem QSeries.keySum_sub_keySum_succ {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : keySum q k - keySum q (k + 1) = q ^ (k + 1) * (keySum q (k + 2) - keySum q (k + 1))

The recurrence $S_k - S_{k+1} = q^{k+1}(S_{k+2} - S_{k+1})$ satisfied by $S_k(q)$.

theorem QSeries.keySum_eq_one_div_qPochhammerInf_self {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : keySum q k = 1 / qPochhammerInf q q

All $S_k(q)$ are equal to $1/(q;q)_\infty$ for $\|q\| < 1$.

theorem QSeries.qPochhammerInf_mul_pow_eq_div {q : ℂ} (hq : ‖q‖ < 1) (n : ℕ) : qPochhammerInf (q * q ^ n) q = qPochhammerInf q q / qPochhammer q q n

qPochhammerInf (q * q^n) q = (q;q)_∞ / (q;q)_n.

theorem QSeries.hasSum_pow_choose_two_nonneg {q : ℂ} (hq : ‖q‖ < 1) (k : ℕ) : HasSum (fun (m : ℕ) => q ^ (m + k).choose 2 * qPochhammerInf (q * q ^ (m + k)) q * (q ^ m.choose 2 * q ^ m / qPochhammer q q m)) (q ^ k.choose 2)

The sum over $m$ of the $z^k$ cross-terms in the JTP double product has sum $q^{\binom{k}{2}}$.

theorem QSeries.hasSum_pow_choose_two_neg {q : ℂ} (hq : ‖q‖ < 1) (l : ℕ) : HasSum (fun (n : ℕ) => q ^ n.choose 2 * qPochhammerInf (q * q ^ n) q * (q ^ (n + (l + 1)).choose 2 * q ^ (n + (l + 1)) / qPochhammer q q (n + (l + 1)))) (q ^ (l + 2).choose 2)

The sum over $n$ of the $z^{-(l+1)}$ cross-terms in the JTP double product has sum $q^{\binom{l+2}{2}}$.