Algebraic identities for FPS q-series

Purely algebraic proofs of the Euler second identity and the key identity S_k = (qPochhammerInf X)⁻¹ in the formal power series ring R⟦X⟧ over any commutative ring with discrete topology. Combined with the product expansion and Cauchy product, these identities yield the Jacobi triple product.

Main results

• QSeries.FormalPowerSeries.euler_second_identity — FPS Euler second identity.
• QSeries.FormalPowerSeries.keySum_eq_qPochhammerInfInv — S_k = (qPochhammerInf X)⁻¹ for all k.
• QSeries.FormalPowerSeries.hasSum_pow_choose_two_nonneg — Cauchy diagonal coefficient for n ≥ 0.
• QSeries.FormalPowerSeries.hasSum_pow_choose_two_neg — Cauchy diagonal coefficient for n < 0.
• QSeries.FormalPowerSeries.jacobiTripleProduct — FPS Jacobi Triple Product Identity.

noncomputable def QSeries.FormalPowerSeries.qPochhammerInv {R : Type u_1} [CommRing R] (k : ℕ) : PowerSeries R

Inverse of qPochhammer X k in R⟦X⟧, defined via invOfUnit since the constant coefficient is 1.

Equations

• QSeries.FormalPowerSeries.qPochhammerInv k = MvPowerSeries.invOfUnit (QSeries.FormalPowerSeries.qPochhammer PowerSeries.X k) 1

@[simp]

theorem QSeries.FormalPowerSeries.qPochhammer_X_mul_qPochhammerInv {R : Type u_1} [CommRing R] (k : ℕ) : qPochhammer PowerSeries.X k * qPochhammerInv k = 1

qPochhammer X k times its formal power series inverse equals 1.

@[simp]

theorem QSeries.FormalPowerSeries.qPochhammerInv_mul_qPochhammer_X {R : Type u_1} [CommRing R] (k : ℕ) : qPochhammerInv k * qPochhammer PowerSeries.X k = 1

The formal power series inverse of qPochhammer X k times qPochhammer X k equals 1.

theorem QSeries.FormalPowerSeries.one_sub_pow_mul_qPochhammerInv_succ {R : Type u_1} [CommRing R] (k : ℕ) : (1 - PowerSeries.X ^ (k + 1)) * qPochhammerInv (k + 1) = qPochhammerInv k

The recursion (1 - X^{k+1}) * qPochhammerInv(k+1) = qPochhammerInv(k) for the inverse q-Pochhammer symbol.

theorem QSeries.FormalPowerSeries.isUnit_qPochhammerInf_X {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] : IsUnit (qPochhammerInf PowerSeries.X)

qPochhammerInf X is a unit.

noncomputable def QSeries.FormalPowerSeries.qPochhammerInfInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] : PowerSeries R

Inverse of qPochhammerInf X.

Equations

• QSeries.FormalPowerSeries.qPochhammerInfInv = ↑⋯.unit⁻¹

@[simp]

theorem QSeries.FormalPowerSeries.qPochhammerInf_X_mul_qPochhammerInfInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] : qPochhammerInf PowerSeries.X * qPochhammerInfInv = 1

qPochhammerInf X times its formal power series inverse equals 1.

@[simp]

theorem QSeries.FormalPowerSeries.qPochhammerInfInv_mul_qPochhammerInf_X {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] : qPochhammerInfInv * qPochhammerInf PowerSeries.X = 1

The formal power series inverse of qPochhammerInf X times qPochhammerInf X equals 1.

theorem QSeries.FormalPowerSeries.qPochhammerInf_X_mul_qPochhammerInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (n : ℕ) : qPochhammerInf PowerSeries.X * qPochhammerInv n = qPochhammerInf (PowerSeries.X * PowerSeries.X ^ n)

qPochhammerInf X * qPochhammerInv n = qPochhammerInf (X * X^n): multiplying the infinite product by the n-th inverse Pochhammer symbol shifts the argument.

theorem QSeries.FormalPowerSeries.coeff_qBinom_eq_coeff_qPochhammerInv {R : Type u_1} [CommRing R] {k j n : ℕ} (hjk : j + k ≤ n) : (PowerSeries.coeff j) (qBinom n k PowerSeries.X) = (PowerSeries.coeff j) (qPochhammerInv k)

For j + k ≤ n, the j-th coefficient of qBinom n k X equals that of qPochhammerInv k.

theorem QSeries.FormalPowerSeries.euler_second_identity {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) : qPochhammerInf (-a) = ∑' (k : ℕ), PowerSeries.X ^ k.choose 2 * a ^ k * qPochhammerInv k

FPS Euler second identity: qPochhammerInf(-a) = Σ_{k≥0} X^{C(k,2)} · a^k · (qPochhammer X k)⁻¹ in R⟦X⟧.

noncomputable def QSeries.FormalPowerSeries.keySum {R : Type u_1} [CommRing R] [TopologicalSpace R] (k : ℕ) : PowerSeries R

The key sum S_k = ∑_m X^{m(m+k)} / ((X;X)_m (X;X)_{m+k}).

Equations

• QSeries.FormalPowerSeries.keySum k = ∑' (m : ℕ), PowerSeries.X ^ (m * (m + k)) * QSeries.FormalPowerSeries.qPochhammerInv m * QSeries.FormalPowerSeries.qPochhammerInv (m + k)

theorem QSeries.FormalPowerSeries.summable_keySummand {R : Type u_1} [CommRing R] [TopologicalSpace R] (k : ℕ) : Summable fun (m : ℕ) => PowerSeries.X ^ (m * (m + k)) * qPochhammerInv m * qPochhammerInv (m + k)

The defining series for keySum k is summable in R⟦X⟧.

theorem QSeries.FormalPowerSeries.keySum_sub_keySum_succ {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (k : ℕ) : keySum k - keySum (k + 1) = PowerSeries.X ^ (k + 1) * (keySum (k + 2) - keySum (k + 1))

The recurrence: S_k − S_{k+1} = X^{k+1} (S_{k+2} − S_{k+1}).

theorem QSeries.FormalPowerSeries.keySum_eq_keySum_zero {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (k : ℕ) : keySum k = keySum 0

keySum k is independent of k: all values are equal to keySum 0.

theorem QSeries.FormalPowerSeries.coeff_qPochhammerInv_eq_coeff_qPochhammerInfInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {k d : ℕ} (hkd : d < k) : (PowerSeries.coeff d) (qPochhammerInv k) = (PowerSeries.coeff d) qPochhammerInfInv

For d < k, the d-th coefficient of qPochhammerInv k equals the d-th coefficient of qPochhammerInfInv.

theorem QSeries.FormalPowerSeries.coeff_keySum_eq_coeff_qPochhammerInfInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (k d : ℕ) (hkd : d < k) : (PowerSeries.coeff d) (keySum k) = (PowerSeries.coeff d) qPochhammerInfInv

For d < k, the d-th coefficient of keySum k equals the d-th coefficient of qPochhammerInfInv.

theorem QSeries.FormalPowerSeries.keySum_eq_qPochhammerInfInv {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (k : ℕ) : keySum k = qPochhammerInfInv

Key identity: S_k = (qPochhammerInf X)⁻¹ for all k ≥ 0.

theorem QSeries.FormalPowerSeries.qPochhammerInf_X_mul_qPochhammerInf_neg {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) : qPochhammerInf PowerSeries.X * qPochhammerInf (-a) = ∑' (n : ℕ), PowerSeries.X ^ n.choose 2 * a ^ n * qPochhammerInf (PowerSeries.X * PowerSeries.X ^ n)

qPochhammerInf X * qPochhammerInf(-a) = Σ_n X^{C(n,2)} a^n qPochhammerInf(X · X^n) in R⟦X⟧.

theorem QSeries.FormalPowerSeries.hasSum_pow_choose_two_nonneg {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (k : ℕ) : HasSum (fun (m : ℕ) => PowerSeries.X ^ (m + k).choose 2 * qPochhammerInf (PowerSeries.X * PowerSeries.X ^ (m + k)) * (PowerSeries.X ^ m.choose 2 * PowerSeries.X ^ m * qPochhammerInv m)) (PowerSeries.X ^ k.choose 2)

Cauchy diagonal coefficient for non-negative index k: the (m+k, m) diagonal of the double series sums to X^{C(k,2)} in R⟦X⟧.

theorem QSeries.FormalPowerSeries.hasSum_pow_choose_two_neg {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (l : ℕ) : HasSum (fun (n : ℕ) => PowerSeries.X ^ n.choose 2 * qPochhammerInf (PowerSeries.X * PowerSeries.X ^ n) * (PowerSeries.X ^ (n + (l + 1)).choose 2 * PowerSeries.X ^ (n + (l + 1)) * qPochhammerInv (n + (l + 1)))) (PowerSeries.X ^ (l + 2).choose 2)

Cauchy diagonal coefficient for negative index -(l+1): the (n, n+l+1) diagonal of the double series sums to X^{C(l+2,2)} in R⟦X⟧.

theorem QSeries.FormalPowerSeries.jacobiTripleProduct : jacobiProd = jacobiBilateral

jacobiProd = jacobiBilateral via HasSum.mul, diagonalEquiv, and diagonal HasSum results.