Locally uniform convergence and analytic Jacobi triple product

We prove that both sides of the Jacobi triple product (JTP) identity converge locally uniformly for $\|q\| < 1$ on $\{z \neq 0\}$, and deduce the analytic JTP: the identity holds for all $\|q\| < 1$ and $z \neq 0$ (removing the earlier restriction $\|z\| < 1$).

Main results

• QSeries.summable_pow_mul_pow_choose_two' — Summability of the nonneg bilateral sum for all $z$ when $\|q\| < 1$.
• QSeries.tendstoLocallyUniformlyOn_jacobiProd — The product side converges locally uniformly on $\{z \neq 0\}$.
• QSeries.tendstoLocallyUniformlyOn_jacobiBilateral — The series side converges locally uniformly on $\{z \neq 0\}$.
• QSeries.jacobiTripleProduct' — The analytic JTP for all $\|q\| < 1$ and $z \neq 0$.

theorem QSeries.summable_pow_add_mul_norm_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (c : ℝ) (j : ℕ) : Summable fun (k : ℕ) => c ^ (k + j) * ‖q‖ ^ (k + 2 * j).choose 2

Ratio-test core for the Weierstrass M-test bounds appearing in the Jacobi triple product: for ‖q‖ < 1 the family k ↦ c ^ (k + j) * ‖q‖ ^ (k + 2 * j).choose 2 is summable for every real c and every shift j.

theorem QSeries.summable_pow_mul_pow_choose_two' {q z : ℂ} (hq : ‖q‖ < 1) : Summable fun (k : ℕ) => z ^ k * q ^ k.choose 2

The nonneg bilateral sum $\sum_{k \ge 0} z^k q^{\binom{k}{2}}$ converges for all $z \in \mathbb{C}$ when $\|q\| < 1$.

theorem QSeries.summable_pow_mul_norm_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) : Summable fun (k : ℕ) => R ^ k * ‖q‖ ^ k.choose 2

Summability of the Weierstrass M-test bound $R^k \|q\|^{\binom{k}{2}}$ for any real $R$.

theorem QSeries.summable_pow_succ_mul_norm_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (R' : ℝ) : Summable fun (m : ℕ) => R' ^ (m + 1) * ‖q‖ ^ (m + 2).choose 2

Summability of the Weierstrass M-test bound $(R')^{m+1} \|q\|^{\binom{m+2}{2}}$ for any real $R'$.

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

Extended product expansion for all $z$.

theorem QSeries.tendstoUniformlyOn_sum_pow_mul_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) : TendstoUniformlyOn (fun (N : ℕ) (z : ℂ) => ∑ k ∈ Finset.range N, z ^ k * q ^ k.choose 2) (fun (z : ℂ) => ∑' (k : ℕ), z ^ k * q ^ k.choose 2) Filter.atTop (Metric.closedBall 0 R)

The nonneg partial sums $\sum_{k < N} z^k q^{\binom{k}{2}}$ converge uniformly on $\{z : \|z\| \le R\}$ by the Weierstrass M-test.

theorem QSeries.tendstoUniformlyOn_sum_inv_pow_mul_pow_choose_two {q : ℂ} (hq : ‖q‖ < 1) (R' : ℝ) : TendstoUniformlyOn (fun (N : ℕ) (z : ℂ) => ∑ m ∈ Finset.range N, z⁻¹ ^ (m + 1) * q ^ (m + 2).choose 2) (fun (z : ℂ) => ∑' (m : ℕ), z⁻¹ ^ (m + 1) * q ^ (m + 2).choose 2) Filter.atTop {z : ℂ | ‖z⁻¹‖ ≤ R'}

The negative-index partial sums converge uniformly on $\{z : \|z^{-1}\| \le R'\}$.

theorem QSeries.tendstoLocallyUniformly_qPochhammer {q : ℂ} (hq : ‖q‖ < 1) : TendstoLocallyUniformly (fun (n : ℕ) (a : ℂ) => qPochhammer a q n) (fun (a : ℂ) => qPochhammerInf a q) Filter.atTop

The partial Pochhammer products $(a;q)_n$ converge locally uniformly in $a$ when $\|q\| < 1$.

theorem QSeries.tendstoLocallyUniformlyOn_jacobiBilateral {q : ℂ} (hq : ‖q‖ < 1) : TendstoLocallyUniformlyOn (fun (N : ℕ) (z : ℂ) => ∑ k ∈ Finset.range N, z ^ k * q ^ k.choose 2 + ∑ m ∈ Finset.range N, z⁻¹ ^ (m + 1) * q ^ (m + 2).choose 2) (fun (z : ℂ) => jacobiBilateral q z) Filter.atTop {z : ℂ | z ≠ 0}

The partial sums of the bilateral Jacobi series converge locally uniformly on $\{z \neq 0\}$ for fixed $\|q\| < 1$.

theorem QSeries.tendstoUniformlyOn_mul_of_bounded {s : Set ℂ} {f₁ f₂ : ℕ → ℂ → ℂ} {F₁ F₂ : ℂ → ℂ} (h₁ : TendstoUniformlyOn f₁ F₁ Filter.atTop s) (h₂ : TendstoUniformlyOn f₂ F₂ Filter.atTop s) (hb₁ : ∃ (C : ℝ), ∀ (n : ℕ), ∀ z ∈ s, ‖f₁ n z‖ ≤ C) (hb₂ : ∃ (C : ℝ), ∀ z ∈ s, ‖F₂ z‖ ≤ C) : TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => f₁ n z * f₂ n z) (fun (z : ℂ) => F₁ z * F₂ z) Filter.atTop s

Uniform convergence of the product of two bounded sequences in a normed ring.

theorem QSeries.exists_norm_qPochhammer_le {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) : ∃ (C : ℝ), ∀ (n : ℕ), ∀ a ∈ Metric.closedBall 0 R, ‖qPochhammer a q n‖ ≤ C

The partial Pochhammer products are uniformly bounded on any closed ball.

theorem QSeries.tendstoUniformlyOn_qPochhammer_closedBall {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) : TendstoUniformlyOn (fun (n : ℕ) (a : ℂ) => qPochhammer a q n) (fun (a : ℂ) => qPochhammerInf a q) Filter.atTop (Metric.closedBall 0 R)

The Pochhammer products $(a;q)_n$ converge uniformly on any closed ball as $n \to \infty$.

theorem QSeries.exists_norm_qPochhammerInf_le {q : ℂ} (hq : ‖q‖ < 1) (R : ℝ) : ∃ (C : ℝ), ∀ a ∈ Metric.closedBall 0 R, ‖qPochhammerInf a q‖ ≤ C

The infinite Pochhammer product $\mathrm{qPochhammerInf}$ is uniformly bounded on any closed ball.

theorem QSeries.tendstoUniformlyOn_qPochhammer_neg_closedBall {q : ℂ} (hq : ‖q‖ < 1) (z₀ : ℂ) (r : ℝ) : TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => qPochhammer (-z) q n) (fun (z : ℂ) => qPochhammerInf (-z) q) Filter.atTop (Metric.closedBall z₀ r)

The Pochhammer products qPochhammer (-z) q n converge uniformly to qPochhammerInf (-z) q on any Metric.closedBall z₀ r when ‖q‖ < 1.

theorem QSeries.tendstoUniformlyOn_qPochhammer_neg_div {q : ℂ} (hq : ‖q‖ < 1) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) : TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => qPochhammer (-q / z) q n) (fun (z : ℂ) => qPochhammerInf (-q / z) q) Filter.atTop (Metric.closedBall z₀ (‖z₀‖ / 2))

The Pochhammer products qPochhammer (-q / z) q n converge uniformly to qPochhammerInf (-q / z) q on Metric.closedBall z₀ (‖z₀‖ / 2) for z₀ ≠ 0, ‖q‖ < 1.

theorem QSeries.tendstoLocallyUniformlyOn_jacobiProd {q : ℂ} (hq : ‖q‖ < 1) : TendstoLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => qPochhammer q q n * qPochhammer (-z) q n * qPochhammer (-q / z) q n) (fun (z : ℂ) => jacobiProd q z) Filter.atTop {z : ℂ | z ≠ 0}

The partial products qPochhammer q q n * qPochhammer (-z) q n * qPochhammer (-q / z) q n converge locally uniformly to jacobiProd q z on {z : ℂ | z ≠ 0} when ‖q‖ < 1.

theorem QSeries.jacobiBilateral_mul_eq_div' {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠ 0) (hz' : z ≠ 0) : jacobiBilateral q (q * z) = jacobiBilateral q z / z

The bilateral series satisfies $g(qz) = g(z)/z$ for all $z \neq 0$.

theorem QSeries.jacobiProd_eq_pow_mul_pow_choose_two_mul {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠ 0) (hz : z ≠ 0) (N : ℕ) : jacobiProd q z = z ^ N * q ^ N.choose 2 * jacobiProd q (q ^ N * z)

Iterating the product-side FE $N$ times.

theorem QSeries.jacobiBilateral_eq_pow_mul_pow_choose_two_mul {q z : ℂ} (hq : ‖q‖ < 1) (hq' : q ≠ 0) (hz : z ≠ 0) (N : ℕ) : jacobiBilateral q z = z ^ N * q ^ N.choose 2 * jacobiBilateral q (q ^ N * z)

Iterating the series-side FE $N$ times.

theorem QSeries.jacobiTripleProduct' {q z : ℂ} (hq : ‖q‖ < 1) (hz : z ≠ 0) : jacobiProd q z = jacobiBilateral q z

Analytic Jacobi triple product identity. For $\|q\| < 1$ and $z \neq 0$: $$(q;q)_\infty \cdot (-z;q)_\infty \cdot (-q/z;q)_\infty \;=\; \sum_{k \in \mathbb{Z}} z^k \, q^{k(k-1)/2}.$$

This extends the basic JTP (which required $\|z\| < 1$) to all $z \neq 0$ using the functional equation $f(qz) = f(z)/z$ satisfied by both sides.