q-Pochhammer symbols as formal power series

This file reformulates the q-Pochhammer symbols and the Jacobi triple product identity in the ring of formal power series A⟦q⟧, where A = ℂ[z, z⁻¹] is the ring of Laurent polynomials.

Key idea

The variable q is the formal power series indeterminate X, while z lives in the coefficient ring A = LaurentPolynomial ℂ. The q-Pochhammer symbol (a; q)_∞ = ∏_{k ≥ 0} (1 - a qᵏ) is a well-defined element of A⟦X⟧ because the factors converge to 1 in the X-adic (pi) topology — no analytic convergence hypotheses are needed.

Main definitions

• QSeries.FormalPowerSeries.qPochhammer — Finite q-Pochhammer (a; X)_n in R⟦X⟧.
• QSeries.FormalPowerSeries.qPochhammerInf — Infinite q-Pochhammer (a; X)_∞ in R⟦X⟧ (via tprod).

Main results

• QSeries.FormalPowerSeries.multipliable_one_sub_mul_pow — The infinite product is multipliable.
• QSeries.FormalPowerSeries.qPochhammerInf_eq_one_sub_mul — (a; X)_∞ = (1 - a) · (aX; X)_∞.
• QSeries.FormalPowerSeries.qPochhammerInf_eq_mk — Coefficient-wise characterisation.
• QSeries.FormalPowerSeries.jacobiTripleProduct — The Jacobi triple product in A⟦X⟧ (proved in QSeries.FPSAlgebra).

noncomputable def QSeries.FormalPowerSeries.qPochhammer {R : Type u_1} [CommRing R] (a : PowerSeries R) (n : ℕ) : PowerSeries R

Finite q-Pochhammer symbol in R⟦X⟧. (a; X)_n = ∏_{k=0}^{n-1} (1 - a · X^k) where a ∈ R⟦X⟧.

Equations

• QSeries.FormalPowerSeries.qPochhammer a n = ∏ k ∈ Finset.range n, (1 - a * PowerSeries.X ^ k)

@[simp]

theorem QSeries.FormalPowerSeries.qPochhammer_zero {R : Type u_1} [CommRing R] (a : PowerSeries R) : qPochhammer a 0 = 1

The empty finite q-Pochhammer product (a; X)_0 = 1.

theorem QSeries.FormalPowerSeries.qPochhammer_succ {R : Type u_1} [CommRing R] (a : PowerSeries R) (n : ℕ) : qPochhammer a (n + 1) = qPochhammer a n * (1 - a * PowerSeries.X ^ n)

The recurrence (a; X)_{n+1} = (a; X)_n * (1 - a X^n).

theorem QSeries.FormalPowerSeries.qPochhammer_succ_eq_one_sub_mul {R : Type u_1} [CommRing R] (a : PowerSeries R) (n : ℕ) : qPochhammer a (n + 1) = (1 - a) * qPochhammer (a * PowerSeries.X) n

The shift identity (a; X)_{n+1} = (1 - a) * (aX; X)_n.

theorem QSeries.FormalPowerSeries.coeff_qPochhammer_succ {R : Type u_1} [CommRing R] (a : PowerSeries R) {d n : ℕ} (hdn : d < n) : (PowerSeries.coeff d) (qPochhammer a (n + 1)) = (PowerSeries.coeff d) (qPochhammer a n)

For d < n, the d-th coefficient of (a; X)_{n+1} equals that of (a; X)_n.

theorem QSeries.FormalPowerSeries.coeff_qPochhammer_eq_of_le {R : Type u_1} [CommRing R] (a : PowerSeries R) {d M N : ℕ} (hM : d < M) (hN : M ≤ N) : (PowerSeries.coeff d) (qPochhammer a N) = (PowerSeries.coeff d) (qPochhammer a M)

For N ≥ M > d, the d-th coefficient of (a; X)_N equals that of (a; X)_M.

theorem QSeries.FormalPowerSeries.multipliable_one_sub_mul_pow {R : Type u_1} [CommRing R] [TopologicalSpace R] (a : PowerSeries R) : Multipliable fun (k : ℕ) => 1 - a * PowerSeries.X ^ k

The infinite product ∏_{k ≥ 0} (1 - a X^k) is multipliable in R⟦X⟧.

noncomputable def QSeries.FormalPowerSeries.qPochhammerInf {R : Type u_1} [CommRing R] [TopologicalSpace R] (a : PowerSeries R) : PowerSeries R

Infinite q-Pochhammer symbol (a; X)_∞ = ∏_{k ≥ 0} (1 - a · X^k). Well-defined in R⟦X⟧ with the pi topology.

Equations

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

theorem QSeries.FormalPowerSeries.coeff_qPochhammerInf {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) (d : ℕ) : (PowerSeries.coeff d) (qPochhammerInf a) = (PowerSeries.coeff d) (qPochhammer a (d + 1))

The d-th coefficient of (a; X)_∞ equals the d-th coefficient of (a; X)_{d+1}.

theorem QSeries.FormalPowerSeries.qPochhammerInf_eq_mk {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) : qPochhammerInf a = PowerSeries.mk fun (d : ℕ) => (PowerSeries.coeff d) (qPochhammer a (d + 1))

Coefficient-wise definition.

theorem QSeries.FormalPowerSeries.coeff_zero_qPochhammerInf {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) (ha : (PowerSeries.coeff 0) a = 0) : (PowerSeries.coeff 0) (qPochhammerInf a) = 1

If the constant coefficient of a is zero, then that of (a; X)_∞ is 1.

theorem QSeries.FormalPowerSeries.qPochhammerInf_eq_one_sub_mul {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) : qPochhammerInf a = (1 - a) * qPochhammerInf (a * PowerSeries.X)

The recursion (a; X)_∞ = (1 - a) * (aX; X)_∞.

theorem QSeries.FormalPowerSeries.isUnit_qPochhammerInf {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) (ha : IsUnit (1 - (PowerSeries.coeff 0) a)) : IsUnit (qPochhammerInf a)

(a; X)_∞ is a unit in R⟦X⟧ whenever 1 - coeff 0 a is a unit in R.

@[instance_reducible]

def QSeries.FormalPowerSeries.instTopologicalSpaceLaurentPolyComplex : TopologicalSpace (LaurentPolynomial ℂ)

The discrete topology on LaurentPolynomial ℂ, the coefficient ring of the formal-power-series Jacobi triple product. It is all the X-adic arguments below require.

This is scoped deliberately: a global instance would silently equip Mathlib's LaurentPolynomial ℂ with a discrete topology for every downstream import, which is not this library's decision to make. Consumers opt in with open scoped QSeries.FormalPowerSeries.

Equations

• QSeries.FormalPowerSeries.instTopologicalSpaceLaurentPolyComplex = ⊥

theorem QSeries.FormalPowerSeries.instDiscreteTopologyLaurentPolyComplex : DiscreteTopology (LaurentPolynomial ℂ)

The topology on LaurentPolynomial ℂ from the scoped instance above is discrete.

@[reducible, inline]

noncomputable abbrev QSeries.FormalPowerSeries.laurentZ : PowerSeries (LaurentPolynomial ℂ)

z = T(1) viewed as a constant power series in A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.laurentZ = PowerSeries.C (LaurentPolynomial.T 1)

@[reducible, inline]

noncomputable abbrev QSeries.FormalPowerSeries.laurentZInv : PowerSeries (LaurentPolynomial ℂ)

z⁻¹ = T(-1) viewed as a constant power series in A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.laurentZInv = PowerSeries.C (LaurentPolynomial.T (-1))

noncomputable def QSeries.FormalPowerSeries.qPochhammerInfX : PowerSeries (LaurentPolynomial ℂ)

(q; q)_∞ in A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.qPochhammerInfX = QSeries.FormalPowerSeries.qPochhammerInf PowerSeries.X

noncomputable def QSeries.FormalPowerSeries.qPochhammerInfNegZ : PowerSeries (LaurentPolynomial ℂ)

(-z; q)_∞ in A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.qPochhammerInfNegZ = QSeries.FormalPowerSeries.qPochhammerInf (-QSeries.FormalPowerSeries.laurentZ)

noncomputable def QSeries.FormalPowerSeries.qPochhammerInfNegXMulZInv : PowerSeries (LaurentPolynomial ℂ)

(-q/z; q)_∞ in A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.qPochhammerInfNegXMulZInv = QSeries.FormalPowerSeries.qPochhammerInf (-PowerSeries.X * QSeries.FormalPowerSeries.laurentZInv)

noncomputable def QSeries.FormalPowerSeries.jacobiProd : PowerSeries (LaurentPolynomial ℂ)

The Jacobi triple product (LHS) as an element of A⟦X⟧.

Equations

• QSeries.FormalPowerSeries.jacobiProd = QSeries.FormalPowerSeries.qPochhammerInfX * QSeries.FormalPowerSeries.qPochhammerInfNegZ * QSeries.FormalPowerSeries.qPochhammerInfNegXMulZInv

noncomputable def QSeries.FormalPowerSeries.jacobiBilateral : PowerSeries (LaurentPolynomial ℂ)

The bilateral theta series (RHS).

Equations

• One or more equations did not get rendered due to their size.