Partial sums of SZ-star qMZVs to Duality for TBZ-qMZVs

DefinitionPartial sums of SZ-star qMZVs#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of natural numbers and a bound \(M \in \mathbb{N}\), the partial sum is the formal power series in \(q\) over \(\mathbb{Q}\)

\[ \sum_{M \ge m_1 \ge \dots \ge m_r > 0} \prod_{j=1}^{r} \frac{q^{m_j k_j}}{(1 - q^{m_j})^{k_j}}; \]

for the empty index it is \(1\).

public noncomputable def szStarQMZVPartial : List ℕ → ℕ → ℚ⟦X⟧
  | [], _ => 1
  | k :: ks, M => ∑ m ∈ Finset.Icc 1 M, (X ^ m * (1 - X ^ m)⁻¹) ^ k * szStarQMZVPartial ks m

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 17 (iii) (SZ-star qMZVs, defining sum truncated at m₁ ≤ M).

Used by 3

Used byThe coefficient of \(q\) in \(\zeta_q^{SZ,\star}(1)\) · SZ-star qMZVs · The empty SZ-star qMZV

DefinitionSZ-star qMZVs#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of natural numbers, the SZ-star qMZV \(\zeta_q^{SZ,\star}(k)\) is the formal power series in \(q\) over \(\mathbb{Q}\)

\[ \zeta_q^{SZ,\star}(k_1, \dots, k_r) = \sum_{m_1 \ge \dots \ge m_r > 0} \prod_{j=1}^{r} \frac{q^{m_j k_j}}{(1 - q^{m_j})^{k_j}}, \]

with \(\zeta_q^{SZ,\star}(\varnothing) = 1\). Precisely, its coefficient of \(q^N\) is defined as the coefficient of \(q^N\) in the partial sum over \(N \ge m_1 \ge \dots \ge m_r > 0\). For \(k_1 \ge 1\) the summands with \(m_1 > N\) have \(q\)-adic order \(> N\), so this is the coefficient of \(q^N\) in the full sum; for \(k_1 = 0\) the full sum is not a formal power series and the value is a junk value.

public noncomputable def szStarQMZV (k : List ℕ) : ℚ⟦X⟧ :=
  PowerSeries.mk fun N => coeff N (szStarQMZVPartial k N)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 17 (iii) (the map ζ_q^{SZ,⋆} of SZ-star qMZVs).

Uses 1 · Used by 3

Statement usesPartial sums of SZ-star qMZVs

Used byThe coefficient of \(q\) in \(\zeta_q^{SZ,\star}(1)\) · OOZ-qMZVs are SZ-star qMZVs of the dual index · The empty SZ-star qMZV

TheoremThe empty SZ-star qMZV#✓fully proved

The SZ-star qMZV of the empty index is \(1\): \(\zeta_q^{SZ,\star}(\varnothing) = 1\).

public theorem szStarQMZV_nil : szStarQMZV [] = 1

Sources

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

Uses 2

Statement usesSZ-star qMZVs

Proof usesPartial sums of SZ-star qMZVs

TheoremThe coefficient of \(q\) in \(\zeta_q^{SZ,\star}(1)\)#✓fully proved

The coefficient of \(q\) in the SZ-star qMZV \(\zeta_q^{SZ,\star}(1) = \sum_{m > 0} q^m / (1 - q^m)\) is \(1\).

public theorem coeff_one_szStarQMZV_singleton_one : coeff 1 (szStarQMZV [1]) = 1

Sources

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

Uses 2

Statement usesSZ-star qMZVs

Proof usesPartial sums of SZ-star qMZVs

TheoremOOZ-qMZVs are SZ-star qMZVs of the dual index#●ready to prove

For every index \(k = (k_1, \dots, k_r)\) of natural numbers that is empty or has \(k_1 \ge 1\), the Ohno–Okuda–Zudilin qMZV of \(k\) equals the SZ-star qMZV of the SZ dual index \(k^\dagger\): \(\zeta_q^{OOZ}(k) = \zeta_q^{SZ,\star}(k^\dagger)\).

public theorem_wanted oozQMZV_eq_szStarQMZV_szDualIndex (k : List ℕ)
    (hk₁ : ∀ a ∈ k.head?, 1 ≤ a) :
    oozQMZV k = szStarQMZV (szDualIndex k)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 17 (iii) (after Ebrahimi-Fard, Manchon and Singer).

Uses 3

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · The SZ dual index · SZ-star qMZVs

DefinitionThe map from TBZ words to SZ indices#✓fully proved

Words in the letters \(\bar{1}\) and \(k \in \mathbb{N}\) are sent to formal \(\mathbb{Q}\)-linear combinations of finite sequences of natural numbers (SZ indices) letter by letter: the empty word goes to the empty index with coefficient \(1\), and a word \(x w\) with first letter \(x\) goes to the image of \(w\) with a new first entry prepended to each index, where \(\bar{1}\) contributes the entry \(1\) and a letter \(k\) contributes the sum of the two terms obtained with the entries \(k\) and \(k - 1\) (subtraction truncated at \(0\), so the letter \(0\) gives the entry \(0\) with coefficient doubled). This is the map \(U_{\mathrm{TBZ}}\) on words.

public noncomputable def tbzToSZ : List (Option ℕ) → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | none :: w => (tbzToSZ w).mapDomain (List.cons 1)
  | some k :: w => (tbzToSZ w).mapDomain (List.cons k) + (tbzToSZ w).mapDomain (List.cons (k - 1))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 9 (i) (the map U_TBZ).

Used by 3

Used byTBZ-qMZVs in the SZ model · Duality for TBZ-qMZVs · The TBZ-to-SZ map on the letter \(\bar{1}\)

TheoremThe TBZ-to-SZ map on the letter \(\bar{1}\)#✓fully proved

The map \(U_{\mathrm{TBZ}}\) sends the one-letter word \(\bar{1}\) to the index \((1)\) with coefficient \(1\).

public theorem tbzToSZ_bar : tbzToSZ [none] = Finsupp.single [1] 1

Sources

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

Uses 1

Statement usesThe map from TBZ words to SZ indices

DefinitionThe map \(V_{TBZ}\) from SZ indices to TBZ words#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of natural numbers, \(V_{TBZ}(k)\) is the formal \(\mathbb{Q}\)-linear combination of TBZ words (words in the letters \(\bar 1\) and \(j \ge 1\); write \(z_a\) for the one-letter word \(a\)) obtained by replacing each letter \(k_i = 0\) by \(z_1 - z_{\bar 1}\) and each letter \(k_i \ge 1\) by \(\sum_{j=1}^{k_i} (-1)^{k_i - j} z_{j'}\), where \(j' = \bar 1\) for \(j = 1\) and \(j' = j\) otherwise, and multiplying out by concatenation of words. The empty index goes to the empty word with coefficient \(1\).

public noncomputable def szToTBZ : List ℕ → (List (Option ℕ) →₀ ℚ)
  | [] => Finsupp.single [] 1
  | 0 :: k => (szToTBZ k).mapDomain (List.cons (some 1)) - (szToTBZ k).mapDomain (List.cons none)
  | (a + 1) :: k => ∑ j ∈ Finset.Icc 1 (a + 1),
      ((-1 : ℚ) ^ (a + 1 - j)) •
        (szToTBZ k).mapDomain (List.cons (if j = 1 then none else some j))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 9 (ii) (the map V_TBZ).

Used by 3

Used bySZ-qMZVs in the TBZ model · The map \(V_{TBZ}\) on the index \((1)\) · Duality for TBZ-qMZVs

TheoremThe map \(V_{TBZ}\) on the index \((1)\)#✓fully proved

The map \(V_{TBZ}\) sends the SZ index \((1)\) to the one-letter TBZ word \(\bar 1\) with coefficient \(1\).

public theorem szToTBZ_one : szToTBZ [1] = Finsupp.single [none] 1

Sources

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

Uses 1

Statement usesThe map \(V_{TBZ}\) from SZ indices to TBZ words

TheoremTBZ-qMZVs in the SZ model#●ready to prove

Let \(w = (w_1, \dots, w_r)\) be a TBZ word: each letter is either \(\bar 1\) or a natural number \(k \ge 1\), and \(w_1\) is not the number \(1\). Let \(U_{TBZ}(w) = \sum_v c_v\, v\) be the formal \(\mathbb{Q}\)-linear combination of SZ indices obtained by replacing each letter \(\bar 1\) by \(1\) and each letter \(k\) by \(k\) or by \(k - 1\), summed over all choices. Then the Takeyama–Bradley–Zhao qMZV of \(w\) is the corresponding combination of Schlesinger–Zudilin qMZVs: \(\zeta_q^{TBZ}(w) = \sum_v c_v\, \zeta_q^{SZ}(v)\).

In block form, writing \(\{a\}^d\) for \(d\) copies of the letter \(a\): for \(d_1, \dots, d_s \ge 0\) and \(k_1, \dots, k_{s-1} \ge 1\) with \(k_1 \ge 2\) if \(d_1 = 0\),

\[ \zeta_q^{TBZ}(\{\bar 1\}^{d_1}, k_1, \{\bar 1\}^{d_2}, \dots, k_{s-1}, \{\bar 1\}^{d_s}) = \sum_{\delta \in \{0,1\}^{s-1}} \zeta_q^{SZ}(\{1\}^{d_1}, k_1 - \delta_1, \{1\}^{d_2}, \dots, k_{s-1} - \delta_{s-1}, \{1\}^{d_s}). \]

public theorem_wanted tbzQMZV_eq_sum_szQMZV_tbzToSZ (w : List (Option ℕ))
    (hw : ∀ j ∈ w, ∀ k ∈ j, 1 ≤ k) (hw₁ : w.head? ≠ some (some 1)) :
    tbzQMZV w = (tbzToSZ w).sum fun v c => c • szQMZV v

Sources

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

Uses 3

Statement usesSchlesinger–Zudilin qMZVs · Takeyama–Bradley–Zhao qMZVs · The map from TBZ words to SZ indices

TheoremSZ-qMZVs in the TBZ model#●ready to prove

Let \(k = (k_1, \dots, k_r)\) be an index of natural numbers that is empty or has \(k_1 \ge 1\). Let \(V_{TBZ}(k) = \sum_w c_w\, w\) be the formal \(\mathbb{Q}\)-linear combination of TBZ words (words in the letters \(\bar 1\) and \(j \ge 1\); write \(z_a\) for the one-letter word \(a\)) obtained by replacing each letter \(k_i = 0\) by \(z_1 - z_{\bar 1}\) and each letter \(k_i \ge 1\) by \(\sum_{j=1}^{k_i} (-1)^{k_i - j} z_{j'}\), where \(j' = \bar 1\) for \(j = 1\) and \(j' = j\) otherwise, and multiplying out by concatenation of words. Then the Schlesinger–Zudilin qMZV of \(k\) is the corresponding combination of Takeyama–Bradley–Zhao qMZVs: \(\zeta_q^{SZ}(k) = \sum_w c_w\, \zeta_q^{TBZ}(w)\), that is, \(\zeta_q^{SZ}(k) = \zeta_q^{TBZ}(V_{TBZ}(k))\) with \(\zeta_q^{TBZ}\) extended \(\mathbb{Q}\)-linearly.

public theorem_wanted szQMZV_eq_sum_tbzQMZV_szToTBZ (k : List ℕ) (hk₁ : ∀ a ∈ k.head?, 1 ≤ a) :
    szQMZV k = (szToTBZ k).sum fun w c => c • tbzQMZV w

Sources

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

Uses 3

Statement usesSchlesinger–Zudilin qMZVs · The map \(V_{TBZ}\) from SZ indices to TBZ words · Takeyama–Bradley–Zhao qMZVs

TheoremDuality for TBZ-qMZVs#●ready to prove

Let \(w\) be a TBZ word: each letter is either \(\bar 1\) or a natural number \(k \ge 1\), and the first letter is not the number \(1\). Let \(U_{TBZ}(w) = \sum_v c_v\, v\) be the formal \(\mathbb{Q}\)-linear combination of SZ indices obtained by replacing each letter \(\bar 1\) by \(1\) and each letter \(k\) by \(k\) or by \(k - 1\), summed over all choices. For an SZ index \(u = (u_1, \dots, u_s)\) of natural numbers, let \(V_{TBZ}(u) = \sum_x d_{u,x}\, x\) be the formal \(\mathbb{Q}\)-linear combination of TBZ words obtained by replacing each letter \(u_i = 0\) by \(z_1 - z_{\bar 1}\) and each letter \(u_i \ge 1\) by \(\sum_{j=1}^{u_i} (-1)^{u_i - j} z_{j'}\), where \(z_a\) is the one-letter word \(a\), \(j' = \bar 1\) for \(j = 1\) and \(j' = j\) otherwise, and multiplying out by concatenation of words. Then the Takeyama–Bradley–Zhao qMZVs satisfy

\[ \zeta_q^{TBZ}(w) = \sum_v c_v \sum_x d_{v^\dagger, x}\, \zeta_q^{TBZ}(x), \]

where \(v^\dagger\) is the SZ dual index of \(v\); that is, \(\zeta_q^{TBZ} = \zeta_q^{TBZ} \circ V_{TBZ} \circ \tilde\tau \circ U_{TBZ}\) on such words, where \(\tilde\tau\) is the dual-index map and \(V_{TBZ}\), \(\tilde\tau\) and \(\zeta_q^{TBZ}\) are extended \(\mathbb{Q}\)-linearly.

public theorem_wanted tbzQMZV_eq_sum_tbzQMZV_szToTBZ_szDual (w : List (Option ℕ))
    (hw : ∀ j ∈ w, ∀ k ∈ j, 1 ≤ k) (hw₁ : w.head? ≠ some (some 1)) :
    tbzQMZV w = ((tbzToSZ w).mapDomain szDualIndex).sum fun v c =>
      c • (szToTBZ v).sum fun u d => d • tbzQMZV u

Sources

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

Uses 4

Statement usesThe SZ dual index · The map \(V_{TBZ}\) from SZ indices to TBZ words · Takeyama–Bradley–Zhao qMZVs · The map from TBZ words to SZ indices

8 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.