TBZ-qMZV of the empty index to Coefficients of the SZ generating series

TheoremTBZ-qMZV of the empty index#✓fully proved

The Takeyama–Bradley–Zhao qMZV of the empty index is \(1\): \(\zeta_q^{\mathrm{TBZ}}(\varnothing) = 1\).

public theorem tbzQMZV_nil : tbzQMZV [] = 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the Takeyama–Bradley–Zhao model.

Uses 1

Statement usesTakeyama–Bradley–Zhao qMZVs

TheoremThe TBZ model extends the BZ model#✓fully proved

For every index \((k_1, \dots, k_r)\) of natural numbers, read as a TBZ index without the symbol \(\bar 1\), the TBZ-qMZV equals the Bradley–Zhao qMZV: \(\zeta_q^{\mathrm{TBZ}}(k_1, \dots, k_r) = \zeta_q^{\mathrm{BZ}}(k_1, \dots, k_r)\).

public theorem tbzQMZV_map_some (k : List ℕ) : tbzQMZV (k.map some) = bzQMZV k

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the Takeyama–Bradley–Zhao model.

Uses 4

Statement usesBradley–Zhao q-multiple zeta values · Takeyama–Bradley–Zhao qMZVs

Proof usesGeneral q-multiple zeta values · Letters of the Takeyama–Bradley–Zhao model as qMZV data

TheoremThe Takeyama–Bradley–Zhao model spans \(\mathcal{Z}_q\)#●ready to prove

Let \(\overline{\mathbb{N}}\) consist of the positive integers and one further symbol \(\bar 1\). The space \(\mathcal{Z}_q = \mathcal{Z}_{q,0}\) equals the \(\mathbb{Q}\)-linear span of the TBZ-qMZVs \(\zeta_q^{\mathrm{TBZ}}(k_1, \dots, k_r)\) over all \(r \ge 0\) and all \(k_1, \dots, k_r \in \overline{\mathbb{N}}\) with \(k_1 \ne 1\) when \(r \ge 1\).

public theorem_wanted qMZVSpace_zero_eq_span_tbzQMZV :
    qMZVSpace 0 = Submodule.span ℚ {f | ∃ k : List (Option ℕ),
        (∀ j ∈ k, ∀ kⱼ ∈ j, 1 ≤ kⱼ) ∧ k.head? ≠ some (some 1) ∧ f = tbzQMZV k}

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 6.

Uses 2

Statement usesSpaces of general qMZVs · Takeyama–Bradley–Zhao qMZVs

DefinitionThe spaces \(\mathcal{Z}^\circ_{q,d}\)#✓fully proved

For a natural number \(d\), the space \(\mathcal{Z}^\circ_{q,d}\) is the \(\mathbb{Q}\)-linear span, in the formal power series ring \(\mathbb{Q}[[q]]\), of the general qMZVs \(\zeta_q(k_1, \dots, k_r; Q_1, \dots, Q_r)\) over all \(r \ge 0\), natural numbers \(k_1, \dots, k_r\) and polynomials \(Q_1, \dots, Q_r \in \mathbb{Q}[X]\) such that for every \(j\) we have \(k_j \ge 1\), \(\deg Q_j + d \le k_j\) and \(Q_j(0) = 0\). Here the zero polynomial has degree \(0\).

public noncomputable def qMZVSpaceCirc (d : ℕ) : Submodule ℚ ℚ⟦X⟧ :=
  Submodule.span ℚ {f | ∃ kQ : List (ℕ × Polynomial ℚ),
    (∀ p ∈ kQ, 1 ≤ p.1 ∧ p.2.natDegree + d ≤ p.1 ∧ p.2.coeff 0 = 0) ∧ f = qMZV kQ}

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of 𝒵_{q,d} and 𝒵°_{q,d} (after Bachmann–Kühn).

Uses 1 · Used by 4

Statement usesGeneral q-multiple zeta values

Used byThe constant \(1\) lies in \(\mathcal{Z}^\circ_{q,d}\) · \(\mathcal{Z}^\circ_{q,d}\) is contained in \(\mathcal{Z}_{q,d}\) · Okounkov qMZVs span \(\mathcal{Z}^\circ_{q,1}\) · Brackets, Okounkov qMZVs and Bradley–Zhao qMZVs span \(\mathcal{Z}^\circ_{q,1}\)

TheoremThe constant \(1\) lies in \(\mathcal{Z}^\circ_{q,d}\)#✓fully proved

For every natural number \(d\), the constant power series \(1\) (the qMZV of the empty index) lies in the space \(\mathcal{Z}^\circ_{q,d}\).

public theorem one_mem_qMZVSpaceCirc (d : ℕ) : (1 : ℚ⟦X⟧) ∈ qMZVSpaceCirc d

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of 𝒵°_{q,d}.

Uses 2

Statement usesThe spaces \(\mathcal{Z}^\circ_{q,d}\)

Proof usesGeneral q-multiple zeta values

Theorem\(\mathcal{Z}^\circ_{q,d}\) is contained in \(\mathcal{Z}_{q,d}\)#✓fully proved

For every natural number \(d\), the space \(\mathcal{Z}^\circ_{q,d}\) is a subspace of \(\mathcal{Z}_{q,d}\).

public theorem qMZVSpaceCirc_le_qMZVSpace (d : ℕ) : qMZVSpaceCirc d ≤ qMZVSpace d

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of 𝒵°_{q,d} (a subspace of 𝒵_{q,d}).

Uses 3

Statement usesSpaces of general qMZVs · The spaces \(\mathcal{Z}^\circ_{q,d}\)

Proof usesGeneral q-multiple zeta values

DefinitionOkounkov polynomials#✓fully proved

For \(k \in \mathbb{N}\), the Okounkov polynomial \(p_k \in \mathbb{Q}[X]\) is \(p_k(X) = X^{k/2}\) if \(k\) is even and \(p_k(X) = X^{(k-1)/2}(1 + X)\) if \(k\) is odd.

public noncomputable def okounkovPoly (k : ℕ) : Polynomial ℚ :=
  if k % 2 = 0 then Polynomial.X ^ (k / 2) else Polynomial.X ^ ((k - 1) / 2) * (1 + Polynomial.X)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of Okounkov qMZVs.

Used by 2

Used byThe Okounkov polynomials \(p_2\) and \(p_3\) · Okounkov \(q\)-multiple zeta values

TheoremThe Okounkov polynomials \(p_2\) and \(p_3\)#✓fully proved

The Okounkov polynomials of index \(2\) and \(3\) are \(p_2(X) = X\) and \(p_3(X) = X(1 + X)\).

public theorem okounkovPoly_two_three :
    okounkovPoly 2 = Polynomial.X ∧ okounkovPoly 3 = Polynomial.X * (1 + Polynomial.X)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of Okounkov qMZVs.

Uses 1

Statement usesOkounkov polynomials

DefinitionOkounkov \(q\)-multiple zeta values#✓fully proved

For a natural number \(k\) let \(p_k\) be Okounkov's polynomial: \(p_k(X) = X^{k/2}\) if \(k\) is even and \(p_k(X) = X^{(k-1)/2}(1 + X)\) if \(k\) is odd. For an index \((k_1, \dots, k_r)\) of natural numbers, the Okounkov qMZV is the general qMZV \(\zeta_q^{\mathrm{Oko}}(k_1, \dots, k_r) = \zeta_q(k_1, \dots, k_r; p_{k_1}, \dots, p_{k_r})\), a formal power series in \(q\) over \(\mathbb{Q}\).

The paper uses it only for indices with every \(k_i \ge 2\); for other indices the value is a placeholder.

public noncomputable def okounkovQMZV (k : List ℕ) : ℚ⟦X⟧ :=
  qMZV (k.map fun k => (k, okounkovPoly k))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of Okounkov qMZVs.

Uses 2 · Used by 3

Statement usesOkounkov polynomials · General q-multiple zeta values

Used byOkounkov qMZV of the empty index · Okounkov qMZVs span \(\mathcal{Z}^\circ_{q,1}\) · Brackets, Okounkov qMZVs and Bradley–Zhao qMZVs span \(\mathcal{Z}^\circ_{q,1}\)

TheoremOkounkov qMZV of the empty index#✓fully proved

The Okounkov \(q\)-multiple zeta value of the empty index is \(1\): \(\zeta_q^{\mathrm{Oko}}(\varnothing) = 1\).

public theorem okounkovQMZV_nil : okounkovQMZV [] = 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of Okounkov qMZVs.

Uses 1

Statement usesOkounkov \(q\)-multiple zeta values

TheoremOkounkov qMZVs span \(\mathcal{Z}^\circ_{q,1}\)#●ready to prove

The space \(\mathcal{Z}^\circ_{q,1}\) equals the \(\mathbb{Q}\)-linear span of the Okounkov qMZVs \(\zeta_q^{\mathrm{Oko}}(k_1, \dots, k_r)\) over all indices of length \(r \ge 0\) with every \(k_i \ge 2\).

public theorem_wanted qMZVSpaceCirc_one_eq_span_okounkovQMZV :
    qMZVSpaceCirc 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 2 ≤ kᵢ) ∧ f = okounkovQMZV k}

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 13 (after Bachmann–Kühn).

Uses 2

Statement usesOkounkov \(q\)-multiple zeta values · The spaces \(\mathcal{Z}^\circ_{q,d}\)

DefinitionEulerian q-series#✓fully proved

For natural numbers \(k\) and \(m \ge 1\), the Eulerian \(q\)-series is

\[ \sum_{n \ge 1} \frac{n^{k-1}}{(k-1)!} \, q^{mn}, \]

the inner sum of a bi-bracket; here \(k - 1\) is read as \(0\) when \(k = 0\). For \(m = 0\) the series is defined to be \(0\).

For \(k, m \ge 1\) it equals \(P_k(q^m)/(1 - q^m)^k\), where \(P_k\) is the \(k\)-th Eulerian polynomial.

public noncomputable def eulerianQSeries (k m : ℕ) : ℚ⟦X⟧ :=
  PowerSeries.mk fun e =>
    if 0 < e ∧ m ∣ e then ((e / m : ℕ) : ℚ) ^ (k - 1) / (k - 1).factorial else 0

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition-Proposition of bi-brackets (Eulerian polynomials).

Used by 2

Used byPartial sums of bi-brackets · Coefficients of the Eulerian q-series

TheoremCoefficients of the Eulerian q-series#✓fully proved

For natural numbers \(k\), \(m\) and \(n\) with \(m > 0\) and \(n > 0\), the coefficient of \(q^{mn}\) in the Eulerian \(q\)-series \(\sum_{\ell \ge 1} \frac{\ell^{k-1}}{(k-1)!} q^{m\ell}\) is \(\frac{n^{k-1}}{(k-1)!}\), where \(k - 1\) is read as \(0\) when \(k = 0\).

public theorem coeff_mul_eulerianQSeries (k m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
    coeff (m * n) (eulerianQSeries k m) = (n : ℚ) ^ (k - 1) / (k - 1).factorial

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition-Proposition of bi-brackets.

Uses 1

Statement usesEulerian q-series

DefinitionPartial sums of bi-brackets#✓fully proved

For pairs \((k_1, d_1), \dots, (k_r, d_r)\) of natural numbers and a bound \(M \in \mathbb{N}\), the partial bi-bracket is the \(q\)-series

\[ \sum_{M > m_1 > \dots > m_r > 0} \, \prod_{j=1}^{r} \frac{m_j^{d_j}}{d_j!} E_{k_j}(m_j), \]

where \(E_k(m) = \sum_{n \ge 1} \frac{n^{k-1}}{(k-1)!} q^{mn}\) is the Eulerian \(q\)-series (with \(k - 1\) read as \(0\) when \(k = 0\)). For \(r = 0\) it is \(1\).

public noncomputable def biBracketPartial : List (ℕ × ℕ) → ℕ → ℚ⟦X⟧
  | [], _ => 1
  | (k, d) :: kd, M => ∑ m ∈ Finset.Ioo 0 M,
      ((m : ℚ) ^ d / d.factorial) • (eulerianQSeries k m * biBracketPartial kd m)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition-Proposition of bi-brackets (defining sum truncated at m₁ < M).

Uses 1 · Used by 2

Statement usesEulerian q-series

Used byBi-brackets · Empty bi-bracket

DefinitionBi-brackets#✓fully proved

For integers \(k_1, \dots, k_r \ge 1\) and \(d_1, \dots, d_r \ge 0\), the bi-bracket is the \(q\)-series

\[ g(k_1, \dots, k_r; d_1, \dots, d_r) = \sum_{m_1 > \dots > m_r > 0} \, \sum_{n_1, \dots, n_r > 0} \, \prod_{j=1}^{r} \frac{m_j^{d_j}}{d_j!} \frac{n_j^{k_j - 1}}{(k_j - 1)!} \, q^{m_1 n_1 + \dots + m_r n_r}, \]

and \(g(\varnothing; \varnothing) = 1\). The summands with \(m_1 > N\) have \(q\)-adic order greater than \(N\), so the coefficient of \(q^N\) is that of the finite partial sum over \(m_1 \le N\); this is how the series is defined.

The same formula, with \(k_j - 1\) read as \(0\), defines a value when some \(k_j = 0\).

public noncomputable def biBracket (kd : List (ℕ × ℕ)) : ℚ⟦X⟧ :=
  PowerSeries.mk fun N => coeff N (biBracketPartial kd (N + 1))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition-Proposition of bi-brackets (after Bachmann).

Uses 1 · Used by 5

Statement usesPartial sums of bi-brackets

Used byGenerating series of bi-brackets · Empty bi-bracket · Coefficients of the bi-bracket generating series · Bi-brackets form a quasi-shuffle algebra · Brackets, Okounkov qMZVs and Bradley–Zhao qMZVs span \(\mathcal{Z}^\circ_{q,1}\)

TheoremEmpty bi-bracket#✓fully proved

The bi-bracket of the empty index is \(1\): \(g(\varnothing; \varnothing) = 1\).

public theorem biBracket_nil : biBracket [] = 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition-Proposition of bi-brackets.

Uses 2

Statement usesBi-brackets

Proof usesPartial sums of bi-brackets

DefinitionGenerating series of bi-brackets#✓fully proved

For \(r \in \mathbb{N}\), the generating series of the bi-brackets of depth \(r\) is the formal power series in the variables \(X_1, \dots, X_r\), \(Y_1, \dots, Y_r\) with coefficients in \(\mathbb{Q}[[q]]\)

\[ g(X_1, \dots, X_r; Y_1, \dots, Y_r) = \sum_{k_1, \dots, k_r \ge 1} \, \sum_{d_1, \dots, d_r \ge 1} g(k_1, \dots, k_r; d_1 - 1, \dots, d_r - 1) \prod_{j=1}^{r} X_j^{k_j - 1} Y_j^{d_j - 1}, \]

where \(g(k_1, \dots, k_r; d_1, \dots, d_r)\) is the bi-bracket. Equivalently, the coefficient of \(\prod_{j=1}^{r} X_j^{a_j} Y_j^{b_j}\) is \(g(a_1 + 1, \dots, a_r + 1; b_1, \dots, b_r)\).

public noncomputable def biBracketGen (r : ℕ) : MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧ :=
  fun e => biBracket (List.ofFn fun j => (e (Sum.inl j) + 1, e (Sum.inr j)))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 11 (definition of the generating series).

Uses 1 · Used by 4

Statement usesBi-brackets

Used byCoefficients of the bi-bracket generating series · Translation between bi-brackets and the Schlesinger–Zudilin model · Partition relation for bi-brackets · Bi-bracket generating series as a sum of exponentials

TheoremCoefficients of the bi-bracket generating series#✓fully proved

For \(r \in \mathbb{N}\) and exponents \(a_1, \dots, a_r, b_1, \dots, b_r \ge 0\), the coefficient of \(\prod_{j=1}^{r} X_j^{a_j} Y_j^{b_j}\) in the generating series \(g(X_1, \dots, X_r; Y_1, \dots, Y_r)\) of bi-brackets of depth \(r\) is the bi-bracket \(g(a_1 + 1, \dots, a_r + 1; b_1, \dots, b_r)\).

public theorem coeff_biBracketGen (r : ℕ) (e : Fin r ⊕ Fin r →₀ ℕ) :
    MvPowerSeries.coeff e (biBracketGen r) =
      biBracket (List.ofFn fun j => (e (Sum.inl j) + 1, e (Sum.inr j)))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 11.

Uses 2

Statement usesBi-brackets · Generating series of bi-brackets

DefinitionGenerating series of Schlesinger–Zudilin qMZVs#✓fully proved

For a natural number \(r\), the generating series of SZ-qMZVs of depth \(r\) is the formal power series in the \(2r\) variables \(X_1, \dots, X_r, Y_1, \dots, Y_r\) with coefficients in \(\mathbb{Q}[[q]]\)

\[ s(X_1, \dots, X_r; Y_1, \dots, Y_r) = \sum_{k_1, \dots, k_r \ge 1} \sum_{d_1, \dots, d_r \ge 0} \zeta_q^{\mathrm{SZ}}(k_1, \{0\}^{d_1}, \dots, k_r, \{0\}^{d_r}) \prod_{j=1}^{r} X_j^{k_j - 1} Y_j^{d_j}, \]

where \(\{0\}^{d}\) stands for \(d\) consecutive zeros.

public noncomputable def szGen (r : ℕ) : MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧ :=
  fun e => szQMZV (szBlockIndex (List.ofFn fun j => (e (Sum.inl j) + 1, e (Sum.inr j) + 1)))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 4 (definition of the generating series).

Uses 2 · Used by 2

Statement usesBlock indices for Schlesinger–Zudilin qMZVs · Schlesinger–Zudilin qMZVs

Used byCoefficients of the SZ generating series · Translation between bi-brackets and the Schlesinger–Zudilin model

TheoremCoefficients of the SZ generating series#✓fully proved

For \(r \in \mathbb{N}\) and exponents \(a_1, \dots, a_r, b_1, \dots, b_r \ge 0\), the coefficient of \(\prod_{j=1}^{r} X_j^{a_j} Y_j^{b_j}\) in the generating series \(s(X_1, \dots, X_r; Y_1, \dots, Y_r)\) of Schlesinger–Zudilin \(q\)-multiple zeta values of depth \(r\) is \(\zeta_q^{\mathrm{SZ}}(a_1 + 1, \{0\}^{b_1}, \dots, a_r + 1, \{0\}^{b_r})\), where \(\{0\}^b\) stands for \(b\) consecutive zeros.

public theorem coeff_szGen (r : ℕ) (e : Fin r ⊕ Fin r →₀ ℕ) :
    MvPowerSeries.coeff e (szGen r) =
      szQMZV (szBlockIndex (List.ofFn fun j => (e (Sum.inl j) + 1, e (Sum.inr j) + 1)))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 4.

Uses 3

Statement usesBlock indices for Schlesinger–Zudilin qMZVs · Generating series of Schlesinger–Zudilin qMZVs · Schlesinger–Zudilin qMZVs

18 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.