q-Pochhammer symbol

DefinitionRaw infinite q-Pochhammer product#✓fully proved

For complex numbers \(a\) and \(q\), the raw infinite q-Pochhammer product is the unconditional infinite product \(\prod_{n=0}^{\infty} (1 - a q^n)\), defined for every \(q\): when this product does not converge unconditionally (in particular for most \(q\) with \(|q| \ge 1\)), its value is \(1\) by convention.

noncomputable def qPochhammerInfRaw (a q : ℂ) : ℂ :=
  tprod (fun n : ℕ => (1 - a * q ^ n))

Used by 40

Used byEta-quotient congruence for sums of overpartition minimal excludants · Generating function of the overpartition r-mex sums · Ramanujan's 5-dissection of Euler's product · Ramanujan's 7-dissection of Euler's product · The 3-dissection of \(f_1^3\) for complex \(q\) · The 3-dissection of \(f_1 f_2\) for complex \(q\) · The 3-dissection of \(f_4/f_1\) for complex \(q\) · 2-dissection of the reciprocal square of Euler's product · 2-dissection of the square of Euler's product · 3-dissection of the product form of Ramanujan's phi function at negated argument · 3-dissection of the product form of Ramanujan's psi function at negated argument · 3-dissection of the product form of Ramanujan's psi function · Cui–Gu \(p\)-dissection of \(f_1\) · Jacobi's identity for the cube of Euler's product · Infinite q-Pochhammer symbol · The raw q-Pochhammer product at a = 2 and q = 1 equals 1 · Odd Lambert series for Ramanujan's continued fractions of order sixteen · Lambert series of order sixteen twisted by the Legendre symbol modulo \(3\) · Weighted Lambert series for the continued fractions of order sixteen · Product forms of Ramanujan's theta functions \(\psi\), \(f\) and \(\chi\) · Ramanujan's function \(k(q)\) · Ramanujan's function \(k\) at \(q\) and \(q^2\) as an eta quotient · Eta-quotient expressions for Ramanujan's function \(k\) · Ramanujan's function \(k\) vanishes at \(0\) · Ramanujan's level-10 theta function identities · Eta-quotients of Ramanujan's theta functions · Ramanujan's theta function at \((q, q^5)\) · Ramanujan's theta function at \((q, q^2)\) · Modular relations for the order-eighteen Rogers–Ramanujan–Slater functions · Relations between the order-eighteen and the nonic Rogers–Ramanujan functions · Eisenstein-series formula for \(\varphi(q)\varphi(q^3)\varphi(q^5)\varphi(q^{15})\) · Eisenstein-series formula for \(\varphi(q)^2\varphi(q^{15})^2\) · Eisenstein-series formula for \(\varphi(q)^2\varphi(q^{10})^2\) · A theta identity for \(\varphi(q)^2\varphi(q^{10})^2 + 5\varphi(q^2)^2\varphi(q^5)^2\) · Eisenstein-series formula for \(\varphi(q^3)^2\varphi(q^5)^2\) · Eisenstein-series formula for \(\varphi(q^2)^2\varphi(q^5)^2\) · A product identity for Ramanujan's \(f(q)f(q^3)f(q^5)f(q^{15})\) · Representation numbers of the quaternary forms \((1,1,15,15)\), \((3,3,5,5)\) and \((1,3,5,15)\) · Representation numbers of the quaternary forms \((1,1,10,10)\) and \((2,2,5,5)\) · A theta identity for \(12\varphi(q)^2\varphi(q^{10})^2 + 12\varphi(q^2)^2\varphi(q^5)^2\)

DefinitionInfinite q-Pochhammer symbol#✓fully proved

For complex numbers \(a\) and \(q\) with \(|q| < 1\), the infinite q-Pochhammer symbol is \((a;q)_\infty = \prod_{n=0}^{\infty} (1 - a q^n)\), the unconditional infinite product of the factors \(1 - a q^n\).

The hypothesis \(|q| < 1\) is an argument of the definition, so the symbol cannot be applied to \(q\) outside the open unit disk.

noncomputable def qPochhammerInf (a q : ℂ) (_hq : ‖q‖ < 1) : ℂ :=
  qPochhammerInfRaw a q

Sources

2607.10576:D01 / 2608.13818:D02 jointly define (a;q)_∞ := ∏_{j=0}^{∞} (1 - a·q^j) for complex a, q with ‖q‖ < 1.

Uses 1 · Used by 17

Statement usesRaw infinite q-Pochhammer product

Used by\(2\)-adic multisection of the infinite \(q\)-Pochhammer symbol · \(3\)-adic factorization of the Euler function · 2-adic dissection of the Euler function · 2-adic product factorization of the Euler function · Generating function of the largest max-rook number · Three-dissection of \((q;q)_\infty / (q^2;q^2)_\infty^2\) · Eta-quotient identity in the powers \(q^3\), \(q^6\), \(q^9\) and \(q^{18}\) · Andrews' identity for the first Rogers–Ramanujan series · Andrews' identity for the second Rogers–Ramanujan series · Jacobi's identity for the cube of Euler's product · Jacobi theta function, product form · Symmetry of the Jacobi theta product under \(x \mapsto q/x\) · Jacobi theta product with vanishing first argument · Jacobi theta product at nome zero · Convergence of the infinite q-Pochhammer product · The q-Pochhammer symbol vanishes at a = 1 and q = 0 · The q-Pochhammer symbol with a = 0

TheoremThe q-Pochhammer symbol with a = 0#✓fully proved

For every complex number \(q\) with \(|q| < 1\), \((0;q)_\infty = 1\), since every factor \(1 - 0 \cdot q^n\) equals \(1\).

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

Uses 1 · Used by 2

Statement usesInfinite q-Pochhammer symbol

Used byJacobi theta product with vanishing first argument · Jacobi theta product at nome zero

TheoremConvergence of the infinite q-Pochhammer product#✓fully proved

For all complex numbers \(a\) and \(q\) with \(|q| < 1\), the infinite product \(\prod_{n=0}^{\infty} (1 - a q^n)\) converges unconditionally to the infinite q-Pochhammer symbol \((a;q)_\infty\): the products of the factors \(1 - a q^n\) over finite sets of indices \(n\) tend to \((a;q)_\infty\).

No nonvanishing hypothesis is imposed, so the cases where some factor is zero (and the product is \(0\)) are included.

theorem hasProd_qPochhammerInf (a q : ℂ) (hq : ‖q‖ < 1) :
    HasProd (fun n : ℕ => (1 - a * q ^ n)) (qPochhammerInf a q hq)

Sources

2607.10576:D01, where the infinite product \((a;q)_\infty\) is used under \(|q| < 1\).

Uses 1 · Used by 1

Statement usesInfinite q-Pochhammer symbol

Used byThe q-Pochhammer symbol vanishes at a = 1 and q = 0

TheoremThe q-Pochhammer symbol vanishes at a = 1 and q = 0#✓fully proved

The infinite q-Pochhammer symbol satisfies \((1;0)_\infty = 0\), because its factor for \(n = 0\) is \(1 - 1 \cdot 0^0 = 0\) (with the convention \(0^0 = 1\)).

@[simp]
theorem qPochhammerInf_one_zero : qPochhammerInf 1 0 (by simp) = 0

Uses 2

Statement usesInfinite q-Pochhammer symbol

Proof usesConvergence of the infinite q-Pochhammer product

TheoremThe raw q-Pochhammer product at a = 2 and q = 1 equals 1#✓fully proved

The raw infinite q-Pochhammer product at \(a = 2\) and \(q = 1\) equals \(1\).

Every factor \(1 - 2 \cdot 1^n\) equals \(-1\), so the finite partial products alternate between \(-1\) and \(1\) and the product does not converge; the value \(1\) is the default that the unconditional product takes in that case, not a limit of partial products. The q-Pochhammer symbol \((a;q)_\infty\), which requires \(|q| < 1\), excludes such arguments.

theorem qPochhammerInfRaw_two_one : qPochhammerInfRaw 2 1 = 1

Uses 1

Statement usesRaw infinite q-Pochhammer product

DefinitionThe Euler products of partition theory#✓fully proved

For a natural number \(k\), the Euler product \(f_k = (q^k; q^k)_\infty = \prod_{m \ge 1} (1 - q^{km})\) is this infinite product in the ring of integer power series in \(q\), taken in the coefficientwise topology. It is used for \(k \ge 1\).

noncomputable def qEulerProduct (k : ℕ) : ℤ⟦X⟧ :=
  ∏' m : ℕ, (1 - X ^ (k * (m + 1)))

Sources

James A. Sellers, Elementary Proofs of Congruences for POND and PEND Partitions, Journal of Integer Sequences 27 (2024), Article 24.4.7, Section 2.

Used by 97

TheoremPentagonal series expansion of the first Euler product#✓fully proved

The Euler product \(f_1 = \prod_{m \ge 1} (1 - q^m)\) equals the pentagonal series \(\sum_{j \in \mathbb{Z}} (-1)^j q^{j(3j-1)/2}\) as an integer power series.

theorem qEulerProduct_one : qEulerProduct 1 = pentagonalSeries ℤ

Sources

James A. Sellers, Elementary Proofs of Congruences for POND and PEND Partitions, Journal of Integer Sequences 27 (2024), Article 24.4.7, Section 2.

Uses 1

Statement usesThe Euler products of partition theory

TheoremConstant term of the Euler products#✓fully proved

For every natural number \(k \ge 1\), the integer power series \(f_k = \prod_{m \ge 1} (1 - q^{km})\) has constant coefficient \(1\).

theorem constantCoeff_qEulerProduct {k : ℕ} (hk : 1 ≤ k) :
    constantCoeff (qEulerProduct k) = 1

Sources

S. Shivaprasada Nayaka, B. N. Dharmendra, and M. C. Mahesh Kumar, Divisibility Properties for Overcubic Partition Triples, INTEGERS 24 (2024), Article A80, Section 1 (notation E_k); James A. Sellers, Elementary Proofs of Congruences for POND and PEND Partitions, Journal of Integer Sequences 27 (2024), Article 24.4.7, Section 2.

Uses 1 · Used by 13

Statement usesThe Euler products of partition theory

Used byGenerating function identity for generalized cubic partition numbers · Generalized cubic partitions of zero · Generating function for overcubic partition triples · Overcubic partition triples of \(0\) · Cleared form of the generating function of \((j, k)\)-overpartition pairs with even parts distinct · The count of overpartition pairs of \(0\) with even parts distinct · Product identity for the (9, 18)-overpartition generating function · Generating function identity for \(\mathrm{ped}_{9,9}\) · Values of \(\mathrm{ped}_{9,9}\) and \(\mathrm{ped}_{9,18}\) at \(0\) · Generating function for partitions with designated summands into odd parts · Odd designated-summand partitions of zero · Generating function for \(\ell\)-regular cubic partitions with odd parts overlined · Constant term of the overlined ℓ-regular cubic partition numbers

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.