Jacobi triple product

DefinitionJacobi theta function, product form#✓fully proved

For complex numbers \(x\) and \(q\) with \(|q| < 1\),

\[j(x; q) = (x; q)_\infty \, (q/x; q)_\infty \, (q; q)_\infty,\]

where \((a; q)_\infty = \prod_{n \ge 0} (1 - a q^n)\) is the infinite \(q\)-Pochhammer symbol. Division by zero is read as \(q/0 = 0\), so \(j(0; q) = (q; q)_\infty\).

noncomputable def jacobiThetaProduct (x q : ℂ) (hq : ‖q‖ < 1) : ℂ :=
  qPochhammerInf x q hq * qPochhammerInf (q / x) q hq * qPochhammerInf q q hq

Uses 1 · Used by 3

Statement usesInfinite q-Pochhammer symbol

Used bySymmetry of the Jacobi theta product under \(x \mapsto q/x\) · Jacobi theta product with vanishing first argument · Jacobi theta product at nome zero

TheoremSymmetry of the Jacobi theta product under \(x \mapsto q/x\)#✓fully proved

Write \((a; q)_\infty = \prod_{n \ge 0} (1 - a q^n)\) for the infinite \(q\)-Pochhammer symbol and \(j(x; q) = (x; q)_\infty \, (q/x; q)_\infty \, (q; q)_\infty\) for the product-form Jacobi theta function. For all complex numbers \(x\) and \(q\) with \(0 < |q| < 1\), \(j(q/x; q) = j(x; q)\). This includes \(x = 0\), where \(q/0\) is read as \(0\).

theorem jacobiThetaProduct_symm (x q : ℂ) (hq : ‖q‖ < 1) (h0 : q ≠ 0) :
    jacobiThetaProduct (q / x) q hq = jacobiThetaProduct x q hq

Uses 2

Statement usesJacobi theta function, product form

Proof usesInfinite q-Pochhammer symbol

TheoremJacobi theta product with vanishing first argument#✓fully proved

Write \((a; q)_\infty = \prod_{n \ge 0} (1 - a q^n)\) for the infinite \(q\)-Pochhammer symbol and \(j(x; q) = (x; q)_\infty \, (q/x; q)_\infty \, (q; q)_\infty\) for the product-form Jacobi theta function. For every complex number \(q\) with \(|q| < 1\), \(j(0; q) = (q; q)_\infty\). Here \(q/0\) is read as \(0\), so the first two factors of \(j(0; q)\) both equal \((0; q)_\infty = 1\).

@[simp]
theorem jacobiThetaProduct_zero_left (q : ℂ) (hq : ‖q‖ < 1) :
    jacobiThetaProduct 0 q hq = qPochhammerInf q q hq

Uses 3

Statement usesJacobi theta function, product form · Infinite q-Pochhammer symbol

Proof usesThe q-Pochhammer symbol with a = 0

TheoremJacobi theta product at nome zero#✓fully proved

Write \((a; q)_\infty = \prod_{n \ge 0} (1 - a q^n)\) for the infinite \(q\)-Pochhammer symbol and \(j(x; q) = (x; q)_\infty \, (q/x; q)_\infty \, (q; q)_\infty\) for the product-form Jacobi theta function, where \(|q| < 1\). For every complex number \(x\), \(j(x; 0) = (x; 0)_\infty\): since \(0/x = 0\) (also for \(x = 0\), reading \(0/0\) as \(0\)), the last two factors of \(j(x; 0)\) both equal \((0; 0)_\infty = 1\).

@[simp]
theorem jacobiThetaProduct_zero_right (x : ℂ) :
    jacobiThetaProduct x 0 (by simp) = qPochhammerInf x 0 (by simp)

Uses 3

Statement usesJacobi theta function, product form · Infinite q-Pochhammer symbol

Proof usesThe q-Pochhammer symbol with a = 0

TheoremJacobi triple product identity#✓fully proved

For complex numbers \(z \ne 0\) and \(q\) with \(|q| < 1\), the bilateral series \(\sum_{n \in \mathbb{Z}} z^n q^{n^2}\) is summable, the family of factors \((1 - q^{2n+2})(1 + z q^{2n+1})(1 + z^{-1} q^{2n+1})\), \(n \ge 0\), is multipliable, and

\[\sum_{n \in \mathbb{Z}} z^n q^{n^2} = \prod_{n \ge 0} (1 - q^{2n+2})(1 + z q^{2n+1})(1 + z^{-1} q^{2n+1}).\]

theorem jacobi_triple_product (z q : ℂ) (hz : z ≠ 0) (hq : ‖q‖ < 1) :
    Summable (fun n : ℤ => z ^ n * q ^ (n * n).toNat) ∧
    Multipliable (fun n : ℕ =>
      (1 - q ^ (2 * n + 2)) * (1 + z * q ^ (2 * n + 1)) *
        (1 + z⁻¹ * q ^ (2 * n + 1))) ∧
    (∑' n : ℤ, z ^ n * q ^ (n * n).toNat) =
      ∏' n : ℕ, (1 - q ^ (2 * n + 2)) * (1 + z * q ^ (2 * n + 1)) *
        (1 + z⁻¹ * q ^ (2 * n + 1))

Sources

• Aritram Dhar, Avi Mukhopadhyay, and Rishabh Sarma, "Generalization of the Extended Minimal Excludant of Andrews and Newman," Journal of Integer Sequences 26 (2023), Article 23.3.7, theorem at source lines 455-458 of https://cs.uwaterloo.ca/journals/JIS/VOL26/Sarma/sarma5.tex.

Uses 6 · Used by 2

Proof usesGaussian binomial coefficient · Gaussian binomial coefficients vanish when \(k > M\) · Product formula for Gaussian binomial coefficients · \(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(k = 0\) · Finite \(Q\)-Pochhammer symbol

Used byOverpartitions of \(5n\) modulo \(5\), explicit form · Andrews' form of the Jacobi triple product identity

TheoremAndrews' form of the Jacobi triple product identity#✓fully proved

Let \(q\) be a complex number with \(|q| < 1\), and let \(k\) and \(i\) be natural numbers with \(0 < i \le k\). Then

\[\sum_{n \in \mathbb{Z}} (-1)^n q^{(2k+1)n(n+1)/2 - in} = \prod_{n=0}^{\infty} \left(1 - q^{(2k+1)(n+1)}\right) \left(1 - q^{(2k+1)n + i}\right) \left(1 - q^{(2k+1)(n+1) - i}\right).\]

theorem andrews_jacobi_triple_product
    (q : ℂ) (k i : ℕ) (hi_pos : 0 < i) (hi_le : i ≤ k) (hq : ‖q‖ < 1) :
    ∑' n : ℤ, (-1 : ℂ) ^ n * q ^ ((2 * (k : ℤ) + 1) * n * (n + 1) / 2 - (i : ℤ) * n) =
      ∏' n : ℕ, (1 - q ^ ((2 * (k : ℤ) + 1) * ((n : ℤ) + 1))) *
        (1 - q ^ ((2 * (k : ℤ) + 1) * (n : ℤ) + (i : ℤ))) *
        (1 - q ^ ((2 * (k : ℤ) + 1) * ((n : ℤ) + 1) - (i : ℤ)))

Sources

• Aritram Dhar, Avi Mukhopadhyay, and Rishabh Sarma, "Generalization of the Extended Minimal Excludant of Andrews and Newman," Journal of Integer Sequences 26 (2023), Article 23.3.7, Theorem (Andrews, An98 p. 22, label JTP1), lines 459–462, https://cs.uwaterloo.ca/journals/JIS/VOL26/Sarma/sarma5.tex

Uses 1

Proof usesJacobi triple product identity

TheoremConvergence of the series in Andrews' triple product identity#✓fully proved

Let \(q\) be a complex number with \(|q| < 1\), and let \(k\) and \(i\) be natural numbers with \(i \le k\). Then the bilateral series

\[\sum_{n \in \mathbb{Z}} (-1)^n q^{(2k+1)n(n+1)/2 - in}\]

is summable over \(\mathbb{Z}\).

theorem andrews_jacobi_triple_product_summable
    (q : ℂ) (k i : ℕ) (hi_le : i ≤ k) (hq : ‖q‖ < 1) :
    Summable (fun n : ℤ => (-1 : ℂ) ^ n *
      q ^ ((2 * (k : ℤ) + 1) * n * (n + 1) / 2 - (i : ℤ) * n))

TheoremConvergence of the product in Andrews' triple product identity#✓fully proved

Let \(q\) be a complex number with \(|q| < 1\), and let \(k\) and \(i\) be natural numbers with \(0 < i \le k\). Then the infinite product

\[\prod_{n=0}^{\infty} \left(1 - q^{(2k+1)(n+1)}\right) \left(1 - q^{(2k+1)n + i}\right) \left(1 - q^{(2k+1)(n+1) - i}\right)\]

is multipliable: its products over finite sets of indices converge in \(\mathbb{C}\) (unconditional convergence, where the limit is not required to be nonzero).

theorem andrews_jacobi_triple_product_multipliable
    (q : ℂ) (k i : ℕ) (hi_pos : 0 < i) (hi_le : i ≤ k) (hq : ‖q‖ < 1) :
    Multipliable (fun n : ℕ => (1 - q ^ ((2 * (k : ℤ) + 1) * ((n : ℤ) + 1))) *
      (1 - q ^ ((2 * (k : ℤ) + 1) * (n : ℤ) + (i : ℤ))) *
      (1 - q ^ ((2 * (k : ℤ) + 1) * ((n : ℤ) + 1) - (i : ℤ))))

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.