Infinite q-Pochhammer symbol

Under $\|q\| < 1$, the infinite product $(a;q)_\infty = \prod_{k \geq 0}(1 - aq^k)$ converges. We define it via tprod and prove convergence, non-vanishing, and partial-product convergence.

Main definitions

• QSeries.qPochhammerInf a q — the infinite q-Pochhammer symbol $(a;q)_\infty$.

Main results

• QSeries.multipliable_one_sub_mul_pow — multipliability for $\|q\| < 1$.
• QSeries.tendsto_qPochhammer — partial products converge to $(a;q)_\infty$.
• QSeries.qPochhammerInf_ne_zero — non-vanishing for $\|z\| < 1$, $\|q\| < 1$.
• QSeries.qPochhammerInf_eq_one_sub_mul — telescoping $(z;q)_\infty = (1-z)(zq;q)_\infty$.

noncomputable def QSeries.qPochhammerInf (a q : ℂ) : ℂ

Infinite q-Pochhammer symbol $(a;q)_\infty = \prod_{k=0}^{\infty}(1 - aq^k)$.

Defined unconditionally as a tprod; convergence (under $\|q\| < 1$) is provided by multipliable_one_sub_mul_pow.

Equations

• QSeries.qPochhammerInf a q = ∏' (k : ℕ), (1 - a * q ^ k)

theorem QSeries.summable_norm_neg_mul_pow {a q : ℂ} (hq : ‖q‖ < 1) : Summable fun (n : ℕ) => ‖-(a * q ^ n)‖

For $\|q\| < 1$ the sequence $n \mapsto \|{-}(a q^n)\|$ is summable: it is the geometric series $\|a\| \cdot \|q\|^n$.

theorem QSeries.one_sub_mul_pow_ne_zero {z q : ℂ} (hz : ‖z‖ < 1) (hq : ‖q‖ ≤ 1) (k : ℕ) : 1 - z * q ^ k ≠ 0

If $\|z\| < 1$ and $\|q\| \le 1$ then $z q^k \ne 1$, so the q-Pochhammer factors $1 - z q^k$ are all nonzero.

theorem QSeries.multipliable_one_sub_mul_pow {a q : ℂ} (hq : ‖q‖ < 1) : Multipliable fun (k : ℕ) => 1 - a * q ^ k

For $\|q\| < 1$, the product $\prod_{k \geq 0}(1 - aq^k)$ is multipliable.

theorem QSeries.qPochhammer_self_ne_zero {q : ℂ} (hq : ‖q‖ < 1) (n : ℕ) : qPochhammer q q n ≠ 0

Non-vanishing of $(q;q)_n$ for $\|q\| < 1$.

theorem QSeries.qPochhammer_ne_zero {z q : ℂ} (hz : ‖z‖ < 1) (hq : ‖q‖ ≤ 1) (n : ℕ) : qPochhammer z q n ≠ 0

Non-vanishing of $(z;q)_n$ when $\|z\| < 1$ and $\|q\| \le 1$.

theorem QSeries.qPochhammerInf_ne_zero_of_forall_ne_zero {a q : ℂ} (hq : ‖q‖ < 1) (hfac : ∀ (k : ℕ), 1 - a * q ^ k ≠ 0) : qPochhammerInf a q ≠ 0

Helper: $(a;q)_\infty \neq 0$ when every factor is nonzero.

theorem QSeries.qPochhammerInf_ne_zero {z q : ℂ} (hz : ‖z‖ < 1) (hq : ‖q‖ < 1) : qPochhammerInf z q ≠ 0

Non-vanishing of $(z;q)_\infty$ for $\|z\| < 1, \|q\| < 1$.

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

Partial products converge to $(a;q)_\infty$.

theorem QSeries.qPochhammerInf_eq_one_sub_mul {z q : ℂ} (hq : ‖q‖ < 1) : qPochhammerInf z q = (1 - z) * qPochhammerInf (z * q) q

Telescoping recursion for $(z;q)_\infty$. $(z;q)_\infty = (1 - z) \cdot (zq;q)_\infty$.