Basic hypergeometric series
DefinitionCoefficients of the basic hypergeometric series#✓fully proved
Let \(r\) and \(s\) be natural numbers, let \(a_1, \dots, a_r\), \(b_1, \dots, b_s\) and \(q\) be complex numbers, and write \((x;q)_n = \prod_{j=0}^{n-1} (1 - x q^j)\) for the finite \(q\)-Pochhammer symbol, so that \((q;q)_n = \prod_{j=0}^{n-1} (1 - q^{j+1})\). For a natural number \(n\), the coefficient of \(z^n\) in the basic hypergeometric series \({}_r\phi_s(a_1, \dots, a_r; b_1, \dots, b_s; q, z)\) is
where the exponent \(1 + s - r\) is an integer and may be negative. This is DLMF 17.4.1, which is written for \(r + 1\) upper parameters, restated for \(r\) upper parameters.
No condition on the parameters is imposed: division by zero gives \(0\), and so does every negative power of \(0\). Analytic applications must separately establish that the denominator does not vanish.
noncomputable def basicHypergeometricCoefficient {r s : ℕ} (a : Fin r → ℂ) (b : Fin s → ℂ)
(q : ℂ) (n : ℕ) : ℂ :=
(∏ i, ∏ j ∈ range n, (1 - a i * q ^ j)) /
((∏ j ∈ range n, (1 - q ^ (j + 1))) * ∏ i, ∏ j ∈ range n, (1 - b i * q ^ j)) *
(((-1 : ℂ) ^ n * q ^ Nat.choose n 2) ^ ((1 : ℤ) + s - r))Used by 2
DefinitionBasic hypergeometric series#✓fully proved
Let \(r\) and \(s\) be natural numbers and let \(a_1, \dots, a_r\), \(b_1, \dots, b_s\) and \(q\) be complex numbers. The basic hypergeometric series \({}_r\phi_s(a_1, \dots, a_r; b_1, \dots, b_s; q, z)\) is the formal power series in \(z\) over \(\mathbb{C}\) whose coefficient of \(z^n\), for each natural number \(n\), is the \(n\)-th basic hypergeometric coefficient of these parameters.
noncomputable def basicHypergeometricSeries {r s : ℕ} (a : Fin r → ℂ) (b : Fin s → ℂ)
(q : ℂ) : PowerSeries ℂ :=
PowerSeries.mk fun n => basicHypergeometricCoefficient a b q nnoncomputable def basicHypergeometricCoefficient {r s : ℕ} (a : Fin r → ℂ) (b : Fin s → ℂ)
(q : ℂ) (n : ℕ) : ℂ :=
(∏ i, ∏ j ∈ range n, (1 - a i * q ^ j)) /
((∏ j ∈ range n, (1 - q ^ (j + 1))) * ∏ i, ∏ j ∈ range n, (1 - b i * q ^ j)) *
(((-1 : ℂ) ^ n * q ^ Nat.choose n 2) ^ ((1 : ℤ) + s - r))MathlibExt/Analysis/SpecialFunctions/BasicHypergeometric.lean:80
Uses 1
TheoremCoefficients of the series \({}_{s+1}\phi_s\)#✓fully proved
Let \(s\) be a natural number, let \(a_1, \dots, a_{s+1}\), \(b_1, \dots, b_s\) and \(q\) be complex numbers, and write \((x;q)_n = \prod_{j=0}^{n-1} (1 - x q^j)\) for the finite \(q\)-Pochhammer symbol, so that \((q;q)_n = \prod_{j=0}^{n-1} (1 - q^{j+1})\). For every natural number \(n\), the coefficient of \(z^n\) in the basic hypergeometric series \({}_{s+1}\phi_s(a_1, \dots, a_{s+1}; b_1, \dots, b_s; q, z)\) is
With \(r = s + 1\) upper parameters, the exponent \(1 + s - r\) of the normalization factor \(\left((-1)^n q^{\binom{n}{2}}\right)^{1+s-r}\) is \(0\), so the factor disappears. As in the definition of the coefficient, division by zero gives \(0\).
theorem basicHypergeometricCoefficient_phi_succ (s : ℕ) (a : Fin (s + 1) → ℂ)
(b : Fin s → ℂ) (q : ℂ) (n : ℕ) :
basicHypergeometricCoefficient a b q n =
(∏ i, ∏ j ∈ range n, (1 - a i * q ^ j)) /
((∏ j ∈ range n, (1 - q ^ (j + 1))) * ∏ i, ∏ j ∈ range n, (1 - b i * q ^ j))noncomputable def basicHypergeometricCoefficient {r s : ℕ} (a : Fin r → ℂ) (b : Fin s → ℂ)
(q : ℂ) (n : ℕ) : ℂ :=
(∏ i, ∏ j ∈ range n, (1 - a i * q ^ j)) /
((∏ j ∈ range n, (1 - q ^ (j + 1))) * ∏ i, ∏ j ∈ range n, (1 - b i * q ^ j)) *
(((-1 : ℂ) ^ n * q ^ Nat.choose n 2) ^ ((1 : ℤ) + s - r))MathlibExt/Analysis/SpecialFunctions/BasicHypergeometric.lean:80
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.