Documentation

LeanPool.PentagonalNumberTheoremAnalytic.QSeries.JacobiTripleProduct

Jacobi triple product identity #

The Jacobi triple product identity states that 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}.$$

Proof strategy #

The proof uses:

  1. Both sides satisfy the functional equation $H(qz) = H(z)/z$.
  2. The Euler identities (first and second) provide series expansions.
  3. The Cauchy identity (hasSum_qPochhammer_div_mul_pow) relates the product to sums.
  4. Extension from the annulus ‖q‖ < ‖z‖ < 1 to the full punctured disk.

Main results #

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

Summability of the non-negative part $\sum_{k \geq 0} z^k q^{\binom{k}{2}}$.

source
theorem QSeries.summable_inv_pow_mul_pow_choose_two {q z : ℂ} (hq : ‖q‖ < 1) :
Summable fun (m : ℕ) => z⁻¹ ^ (m + 1) * q ^ (m + 2).choose 2

Summability of the negative-index part $\sum_{m \geq 0} z^{-(m+1)} q^{\binom{m+2}{2}}$ for $\|q\| < 1$ and $z \neq 0$.

source
noncomputable def QSeries.jacobiProd (q z : ℂ) :
ℂ

The Jacobi triple product function $f(z) = (q;q)_\infty \cdot (-z;q)_\infty \cdot (-q/z;q)_\infty$.

Equations
Instances For
    source
    noncomputable def QSeries.jacobiBilateralPos (q z : ℂ) :
    ℂ

    The bilateral Jacobi series (non-negative part).

    Equations
    Instances For
      source
      noncomputable def QSeries.jacobiBilateralNeg (q z : ℂ) :
      ℂ

      The bilateral Jacobi series (negative part). For $k = -(m+1)$ with $m \geq 0$, the exponent is $\binom{m+2}{2} = (m+1)(m+2)/2$.

      Equations
      Instances For
        source
        noncomputable def QSeries.jacobiBilateral (q z : ℂ) :
        ℂ

        The full bilateral Jacobi series.

        Equations
        Instances For
          source
          theorem QSeries.qPochhammerInf_neg_eq_one_add_mul {z q : ℂ} (hq : ‖q‖ < 1) :
          qPochhammerInf (-z) q = (1 + z) * qPochhammerInf (-(z * q)) q

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

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

          The product satisfies $f(qz) = f(z)/z$ when $q \neq 0$ and $z \neq 0$.

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

          The bilateral Jacobi series satisfies the same functional equation $f(qz) = f(z)/z$ as the triple product.

          source
          theorem QSeries.summable_euler_second' {q z : ℂ} (hq : ‖q‖ < 1) :
          Summable fun (n : ℕ) => q ^ n.choose 2 * z ^ n / qPochhammer q q n

          Summability of the Euler second series $\sum_{n \geq 0} q^{\binom{n}{2}} z^n / (q;q)_n$ for all $z$ when $\|q\| < 1$.

          source
          theorem QSeries.tsum_euler_second_eq_one_add_mul {q z : ℂ} (hq : ‖q‖ < 1) :
          ∑' (n : ℕ), q ^ n.choose 2 * z ^ n / qPochhammer q q n = (1 + z) * ∑' (n : ℕ), q ^ n.choose 2 * (z * q) ^ n / qPochhammer q q n

          The Euler second series satisfies the recursion $E(z) = (1+z) \cdot E(qz)$.

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

          Euler second identity for all $z$: the series $\sum_{n \geq 0} q^{\binom{n}{2}} z^n / (q;q)_n$ has sum $(-z;q)_\infty$.

          source
          theorem QSeries.euler_second_identity_div' {q z : ℂ} (hq : ‖q‖ < 1) :
          HasSum (fun (m : ℕ) => q ^ m.choose 2 * q ^ m * z⁻¹ ^ m / qPochhammer q q m) (qPochhammerInf (-q / z) q)

          Euler second identity evaluated at $q/z$: the series $\sum_{m \geq 0} q^{\binom{m}{2}+m} z^{-m} / (q;q)_m$ has sum $(-q/z;q)_\infty$.

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

          Jacobi triple product identity: $(q;q)_\infty (-z;q)_\infty (-q/z;q)_\infty$ equals the bilateral theta series $\sum_{k \in \mathbb{Z}} z^k q^{k(k-1)/2}$ for $\|q\| < 1$, $\|z\| < 1$, and $z \neq 0$.