Marker word of a list of blocks to Duality for OOZ-qMZVs

DefinitionMarker word of a list of blocks#✓fully proved

A marker is either a weight \(k \in \mathbb{N}\) (a weighted position) or a blank (an unweighted position). The marker word of a list of blocks \((s_1, k_1), \dots, (s_r, k_r)\) of natural numbers is the concatenation, in order, of the words consisting of the weight \(k_t\) followed by \(s_t - 1\) blanks (no blanks when \(s_t \le 1\)).

public def bzChainWord (b : List (ℕ × ℕ)) : List (Option ℕ) :=
  b.flatMap fun sk => some sk.2 :: List.replicate (sk.1 - 1) none

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 1 (block t of the chain is m_t > n > ⋯ > n with d_t - 1 entries n).

Used by 2

Used byChain sum of the single block \((1, 1)\) · Combinatorial form of Bradley–Zhao duality

TheoremChain sum of the single block \((1, 1)\)#✓fully proved

The marker word of the single block \((1, 1)\) is one position weighted by \(1\), and its chain sum with bound \(M = 3\) and target \(R = 2\) equals \(3\): it is the sum of \(\binom{j}{1} = j\) over \(0 < m < 3\) and \(j \ge 0\) with \(m j = 2\), which is \(2 + 1 = 3\).

public theorem bzChainSum_bzChainWord_one_one :
    bzChainSum (bzChainWord [(1, 1)]) 3 2 = 3

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 1 (case r = 1, k₁ = d₁ = 1, N = 2).

Uses 2

Statement usesWeighted chain sums · Marker word of a list of blocks

TheoremCombinatorial form of Bradley–Zhao duality#●ready to prove

For a list of blocks \((s_1, w_1), \dots, (s_r, w_r)\) of positive integers and an integer \(N \ge 1\), let \(S_N((s_1, w_1), \dots, (s_r, w_r))\) be the sum of \(\binom{j_1}{w_1} \cdots \binom{j_r}{w_r}\) over all strictly decreasing chains \(N + 1 > a_1 > \dots > a_n > 0\) of length \(n = s_1 + \dots + s_r\) and all multiplicities \(c_1, \dots, c_n \ge 0\) with \(a_1 c_1 + \dots + a_n c_n = N\), where the chain is cut into consecutive blocks of lengths \(s_1, \dots, s_r\) and \(j_t\) is the multiplicity of the first entry of block \(t\). Let \(r \ge 1\) and \(k_1, \dots, k_r, d_1, \dots, d_r \ge 1\). Then

\[S_N((d_1, k_1), \dots, (d_r, k_r)) = S_N((k_r, d_r), \dots, (k_1, d_1)).\]

The bound \(N + 1\) loses nothing: since \(w_1 \ge 1\), a nonzero term has \(j_1 \ge 1\) and hence \(a_1 \le N\).

public theorem_wanted bzChainSum_dual (k d : List ℕ) (hlen : k.length = d.length)
    (hr : k ≠ []) (hk : ∀ x ∈ k, 1 ≤ x) (hd : ∀ x ∈ d, 1 ≤ x) (N : ℕ) (hN : 1 ≤ N) :
    bzChainSum (bzChainWord (d.zip k)) (N + 1) N =
      bzChainSum (bzChainWord (k.zip d).reverse) (N + 1) N

Sources

• arXiv:2111.00051, Theorem 4.18; the record's formula is garbled and is read from there, and the paper's closing remark (equivalence with BZ duality) is not part of this statement.
• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 1.

Uses 2

Statement usesWeighted chain sums · Marker word of a list of blocks

DefinitionThe SZ dual index#✓fully proved

Identify an index \(k = (k_1, \dots, k_r)\) of natural numbers with the word \(p^{k_1} y \cdots p^{k_r} y\) in the letters \(p\) and \(y\), and let \(\tilde\tau\) be the anti-automorphism of words with \(\tilde\tau(p) = y\) and \(\tilde\tau(y) = p\) (reverse the word and swap the letters). Write \(\tilde\tau(p^{k_1} y \cdots p^{k_r} y)\) as \(p^{a_1} y \cdots p^{a_s} y\) followed by a possibly empty run of letters \(p\) (nonempty only when \(k_1 = 0\)); that run is dropped, and the SZ dual index is \(k^\dagger = (a_1, \dots, a_s)\).

For \(k = (k_1, \{0\}^{d_1 - 1}, \dots, k_r, \{0\}^{d_r - 1})\) with all \(k_i, d_i \ge 1\), where \(\{0\}^m\) stands for \(m\) zeros, this gives \(k^\dagger = (d_r, \{0\}^{k_r - 1}, \dots, d_1, \{0\}^{k_1 - 1})\).

public def szDualIndex (k : List ℕ) : List ℕ :=
  szIndexOfWordAux 0 ((szWord k).reverse.map not)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 5 (SZ duality, the map τ̃ and the SZ dual index).

Uses 2 · Used by 5

Statement usesReading an index off a word in \(p\) and \(y\) · Word of an index

Used byBradley–Zhao dual index · Duality for OOZ-qMZVs · The SZ dual of \((2)\) · OOZ-qMZVs are SZ-star qMZVs of the dual index · Duality for TBZ-qMZVs

TheoremThe SZ dual of \((2)\)#✓fully proved

The SZ dual index of the one-entry index \((2)\) is \((1, 0)\), that is, \((2)^\dagger = (1, 0)\).

public theorem szDualIndex_two : szDualIndex [2] = [1, 0]

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 5 (SZ dual index).

Uses 1

Statement usesThe SZ dual index

DefinitionBradley–Zhao dual index#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of natural numbers, form the word \(x^{k_1 - 1} y \cdots x^{k_r - 1} y\) in two letters \(x\) and \(y\) (each \(k_i - 1\) truncated at \(0\)); when all \(k_i \ge 1\) this is \(z_{k_1} \cdots z_{k_r}\) with \(z_k = x^{k-1} y\). Apply the anti-automorphism \(\tau\) of words with \(\tau(x) = y\) and \(\tau(y) = x\), which reverses a word and swaps its letters, and write the result as \(x^{n_1} y \cdots x^{n_s} y \, x^e\). The BZ dual index of \(k\) is \((n_1 + 1, \dots, n_s + 1)\); the trailing \(x^e\) is dropped. For an admissible index (\(k_1 \ge 2\) and all \(k_i \ge 1\), or empty) \(e = 0\), so the dual index is the index of \(\tau(z_{k_1} \cdots z_{k_r})\).

Equivalently, it is the SZ dual index of \((k_1 - 1, \dots, k_r - 1)\) with every entry increased by one.

public def bzDualIndex (k : List ℕ) : List ℕ :=
  (szDualIndex (k.map (· - 1))).map (· + 1)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 7 (BZ duality, the map τ).

Uses 1 · Used by 2

Statement usesThe SZ dual index

Used byBradley–Zhao dual of \((3)\) · Duality for restricted OOZ-qMZVs

TheoremBradley–Zhao dual of \((3)\)#✓fully proved

The Bradley–Zhao dual index of \((3)\) is \((2, 1)\). In terms of words in the letters \(x\) and \(y\), with \(z_k = x^{k-1} y\) and \(\tau\) the anti-automorphism of words that reverses a word and swaps \(x\) and \(y\), this says \(\tau(z_3) = \tau(x x y) = x y y = z_2 z_1\).

public theorem bzDualIndex_three : bzDualIndex [3] = [2, 1]

Sources

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

Uses 1

Statement usesBradley–Zhao dual index

DefinitionThe tail part of the map \(U\)#✓fully proved

A word is a finite sequence \(z_{k_1} \cdots z_{k_s}\) of letters \(z_k\), \(k \in \mathbb{N}\). This map sends the empty word to itself and, for \(s \ge 1\), sends \(z_{k_1} \cdots z_{k_s}\) to the formal \(\mathbb{Q}\)-linear combination of words

\[\sum \binom{k_1 - 1}{n_1 - 1} \cdots \binom{k_s - 1}{n_s - 1} \, z_{n_1} \cdots z_{n_s}\]

over \(1 \le n_j \le k_j\) for \(1 \le j \le s\) (an empty sum is \(0\)). The map \(U\) from OOZ to BZ words applies it to the letters after the first.

public noncomputable def oozToBZTail : List ℕ → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | b :: k => ∑ n ∈ Finset.Icc 1 b,
      (((b - 1).choose (n - 1) : ℕ) : ℚ) • (oozToBZTail k).mapDomain (List.cons n)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 12 (i) (after Ebrahimi-Fard, Manchon and Singer, the map U).

Used by 2

Used byThe map \(U\) from OOZ to BZ words · The map \(U\) fixes \(z_2\)

DefinitionThe map \(U\) from OOZ to BZ words#✓fully proved

A word is a finite sequence \(z_{k_1} \cdots z_{k_r}\) of letters \(z_k\), \(k \in \mathbb{N}\). The map \(U\) sends each word to a formal \(\mathbb{Q}\)-linear combination of words: \(U(\mathbf{1}) = \mathbf{1}\) for the empty word \(\mathbf{1}\), and for \(r \ge 1\)

\[U(z_{k_1} \cdots z_{k_r}) = \sum \binom{k_1 - 2}{n_1 - 2} \binom{k_2 - 1}{n_2 - 1} \cdots \binom{k_r - 1}{n_r - 1} \, z_{n_1} \cdots z_{n_r}\]

where the sum runs over \(2 \le n_1 \le k_1\) and \(1 \le n_j \le k_j\) for \(2 \le j \le r\) (an empty sum is \(0\)).

public noncomputable def oozToBZ : List ℕ → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | a :: k => ∑ n ∈ Finset.Icc 2 a,
      (((a - 2).choose (n - 2) : ℕ) : ℚ) • (oozToBZTail k).mapDomain (List.cons n)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 12 (i) (after Ebrahimi-Fard, Manchon and Singer, the map U).

Uses 1 · Used by 5

Statement usesThe tail part of the map \(U\)

Used byThe map \(U\) is a bijection on combinations of admissible indices · OOZ-qMZVs of admissible indices via BZ-qMZVs · \(U\) fixes the empty index · The map \(U\) fixes \(z_2\) · Duality for restricted OOZ-qMZVs

Theorem\(U\) fixes the empty index#✓fully proved

Write \(\mathbf{1}\) for the empty index. The map \(U\) from OOZ to BZ indices sends \(\mathbf{1}\) to the \(\mathbb{Q}\)-linear combination of indices consisting of \(\mathbf{1}\) with coefficient \(1\); that is, \(U(\mathbf{1}) = \mathbf{1}\).

public theorem oozToBZ_nil : oozToBZ [] = Finsupp.single [] 1

Sources

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

Uses 1

Statement usesThe map \(U\) from OOZ to BZ words

TheoremThe map \(U\) fixes \(z_2\)#✓fully proved

The map \(U\) from OOZ to BZ words sends the one-letter word \(z_2\) to itself with coefficient \(1\): \(U(z_2) = z_2\).

public theorem oozToBZ_two : oozToBZ [2] = Finsupp.single [2] 1

Sources

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

Uses 2

Statement usesThe map \(U\) from OOZ to BZ words

Proof usesThe tail part of the map \(U\)

DefinitionThe tail part of the map \(V\)#✓fully proved

Identify an index \((k_1, \dots, k_s)\) of natural numbers with the word \(p^{k_1} y \cdots p^{k_s} y\) in the letters \(p\) and \(y\). This map sends the empty word to itself and, for \(s \ge 1\), sends \(p^{k_1} y \cdots p^{k_s} y\) to the formal \(\mathbb{Q}\)-linear combination of words

\[\sum \binom{k_1}{n_1} \cdots \binom{k_s}{n_s} \, p^{n_1} y \cdots p^{n_s} y\]

over \(0 \le n_j \le k_j\) for \(1 \le j \le s\). The map \(V\) from OOZ to SZ words applies it to the blocks \(p^{k_j} y\) after the first.

public noncomputable def oozToSZTail : List ℕ → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | b :: k => ∑ n ∈ Finset.range (b + 1),
      ((b.choose n : ℕ) : ℚ) • (oozToSZTail k).mapDomain (List.cons n)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 12 (ii) (after Ebrahimi-Fard, Manchon and Singer, the map V).

Used by 2

Used byThe map \(V\) from OOZ to SZ words · The map \(V\) fixes \(py\)

DefinitionThe map \(V\) from OOZ to SZ words#✓fully proved

Identify an index \((k_1, \dots, k_r)\) of natural numbers with the word \(p^{k_1} y \cdots p^{k_r} y\) in the letters \(p\) and \(y\). The map \(V\) sends each such word to a formal \(\mathbb{Q}\)-linear combination of words: \(V(\mathbf{1}) = \mathbf{1}\) for the empty word \(\mathbf{1}\), and for \(r \ge 1\)

\[V(p^{k_1} y \cdots p^{k_r} y) = \sum \binom{k_1 - 1}{n_1 - 1} \binom{k_2}{n_2} \cdots \binom{k_r}{n_r} \, p^{n_1} y \cdots p^{n_r} y\]

where the sum runs over \(1 \le n_1 \le k_1\) and \(0 \le n_j \le k_j\) for \(2 \le j \le r\) (an empty sum is \(0\)).

public noncomputable def oozToSZ : List ℕ → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | a :: k => ∑ n ∈ Finset.Icc 1 a,
      (((a - 1).choose (n - 1) : ℕ) : ℚ) • (oozToSZTail k).mapDomain (List.cons n)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Proposition 12 (ii) (after Ebrahimi-Fard, Manchon and Singer, the map V).

Uses 1 · Used by 4

Statement usesThe tail part of the map \(V\)

Used byThe map \(V\) is a bijection on combinations of SZ-admissible indices · OOZ-qMZVs via SZ-qMZVs · The map \(V\) fixes \(py\) · Duality for OOZ-qMZVs

TheoremThe map \(V\) fixes \(py\)#✓fully proved

The map \(V\) from OOZ to SZ words sends the word \(py\) (the index \((1)\)) to itself with coefficient \(1\): \(V(py) = py\).

public theorem oozToSZ_one : oozToSZ [1] = Finsupp.single [1] 1

Sources

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

Uses 2

Statement usesThe map \(V\) from OOZ to SZ words

Proof usesThe tail part of the map \(V\)

TheoremOOZ-qMZVs of admissible indices via BZ-qMZVs#●ready to prove

Write \(\zeta_q^{\mathrm{OOZ}}\) and \(\zeta_q^{\mathrm{BZ}}\) for the Ohno–Okuda–Zudilin and Bradley–Zhao qMZVs. Let \(k = (k_1, \dots, k_r)\) be an index of natural numbers with all \(k_i \ge 1\) and, when \(r \ge 1\), \(k_1 \ge 2\) (the empty index is allowed). Write the image of \(k\) under the map \(U\) from OOZ to BZ indices as a \(\mathbb{Q}\)-linear combination \(U(k) = \sum_w c_w \, w\) of indices. Then \(\zeta_q^{\mathrm{OOZ}}(k) = \sum_w c_w \, \zeta_q^{\mathrm{BZ}}(w)\).

On admissible indices \(\zeta_q^{\mathrm{OOZ}}\) is the restricted OOZ-qMZV \(\zeta_q^{\mathrm{OBZ}}\) of the source.

public theorem_wanted oozQMZV_eq_sum_bzQMZV_oozToBZ (k : List ℕ) (hk : ∀ a ∈ k, 1 ≤ a)
    (hk₁ : ∀ a ∈ k.head?, 2 ≤ a) :
    oozQMZV k = (oozToBZ k).sum fun w c => c • bzQMZV w

Sources

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

Uses 3

Statement usesBradley–Zhao q-multiple zeta values · Ohno–Okuda–Zudilin q-multiple zeta values · The map \(U\) from OOZ to BZ words

TheoremThe map \(U\) is a bijection on combinations of admissible indices#●ready to prove

Call an index \((k_1, \dots, k_r)\) of natural numbers admissible if all \(k_i \ge 1\) and, when \(r \ge 1\), \(k_1 \ge 2\); the empty index is admissible. Extend the map \(U\) from OOZ to BZ indices \(\mathbb{Q}\)-linearly to finite \(\mathbb{Q}\)-linear combinations of indices. This extension maps the set of \(\mathbb{Q}\)-linear combinations of admissible indices bijectively onto itself.

public theorem_wanted bijOn_linearCombination_oozToBZ :
    Set.BijOn (Finsupp.linearCombination ℚ oozToBZ)
      (Finsupp.supported ℚ ℚ {w : List ℕ | (∀ a ∈ w, 1 ≤ a) ∧ ∀ a ∈ w.head?, 2 ≤ a})
      (Finsupp.supported ℚ ℚ {w : List ℕ | (∀ a ∈ w, 1 ≤ a) ∧ ∀ a ∈ w.head?, 2 ≤ a})

Sources

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

Uses 1

Statement usesThe map \(U\) from OOZ to BZ words

TheoremOOZ-qMZVs via SZ-qMZVs#●ready to prove

Write \(\zeta_q^{\mathrm{OOZ}}\) and \(\zeta_q^{\mathrm{SZ}}\) for the Ohno–Okuda–Zudilin and Schlesinger–Zudilin qMZVs. Let \(k = (k_1, \dots, k_r)\) be an index of natural numbers that is empty or has \(k_1 \ge 1\) (the entries \(k_2, \dots, k_r\) may be \(0\)). Write the image of \(k\) under the map \(V\) from OOZ to SZ indices as a \(\mathbb{Q}\)-linear combination \(V(k) = \sum_w c_w \, w\) of indices. Then \(\zeta_q^{\mathrm{OOZ}}(k) = \sum_w c_w \, \zeta_q^{\mathrm{SZ}}(w)\).

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

Sources

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

Uses 3

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · The map \(V\) from OOZ to SZ words · Schlesinger–Zudilin qMZVs

TheoremThe map \(V\) is a bijection on combinations of SZ-admissible indices#●ready to prove

Call an index \((k_1, \dots, k_r)\) of natural numbers SZ-admissible if it is empty or \(k_1 \ge 1\) (the entries \(k_2, \dots, k_r\) may be \(0\)). Extend the map \(V\) from OOZ to SZ indices \(\mathbb{Q}\)-linearly to finite \(\mathbb{Q}\)-linear combinations of indices. This extension maps the set of \(\mathbb{Q}\)-linear combinations of SZ-admissible indices bijectively onto itself.

public theorem_wanted bijOn_linearCombination_oozToSZ :
    Set.BijOn (Finsupp.linearCombination ℚ oozToSZ)
      (Finsupp.supported ℚ ℚ {w : List ℕ | ∀ a ∈ w.head?, 1 ≤ a})
      (Finsupp.supported ℚ ℚ {w : List ℕ | ∀ a ∈ w.head?, 1 ≤ a})

Sources

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

Uses 1

Statement usesThe map \(V\) from OOZ to SZ words

TheoremDuality for restricted OOZ-qMZVs#●ready to prove

Call an index \((k_1, \dots, k_r)\) of natural numbers admissible if \(k_j \ge 1\) for all \(j\) and, when \(r \ge 1\), \(k_1 \ge 2\). Extend \(\zeta_q^{\mathrm{OOZ}}\) and the map \(U\) linearly to formal \(\mathbb{Q}\)-linear combinations of indices, and let \(\tau\) act on such a combination by replacing each index with its BZ dual index. Let \(w\) be an admissible index and let \(x\) be a \(\mathbb{Q}\)-linear combination of admissible indices with \(U(x) = \tau(U(w))\). Then \(\zeta_q^{\mathrm{OOZ}}(x) = \zeta_q^{\mathrm{OOZ}}(w)\).

Since \(U\) is a bijection on combinations of admissible indices (Proposition 12 (i) of the source), this is the identity \(\zeta_q^{\mathrm{OOZ}} = \zeta_q^{\mathrm{OOZ}} \circ U^{-1} \circ \tau \circ U\) on admissible indices.

public theorem_wanted sum_oozQMZV_eq_of_oozToBZ_eq_bzDual (w : List ℕ) (hw : ∀ a ∈ w, 1 ≤ a)
    (hw₁ : ∀ a ∈ w.head?, 2 ≤ a) (x : List ℕ →₀ ℚ)
    (hx : x ∈ Finsupp.supported ℚ ℚ {v : List ℕ | (∀ a ∈ v, 1 ≤ a) ∧ ∀ a ∈ v.head?, 2 ≤ a})
    (hUx : Finsupp.linearCombination ℚ oozToBZ x = (oozToBZ w).mapDomain bzDualIndex) :
    (x.sum fun v c => c • oozQMZV v) = oozQMZV w

Sources

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

Uses 3

Statement usesBradley–Zhao dual index · Ohno–Okuda–Zudilin q-multiple zeta values · The map \(U\) from OOZ to BZ words

TheoremDuality for OOZ-qMZVs#●ready to prove

Call an index \((k_1, \dots, k_r)\) of natural numbers SZ-admissible if it is empty or \(k_1 \ge 1\). Extend \(\zeta_q^{\mathrm{OOZ}}\) and the map \(V\) linearly to formal \(\mathbb{Q}\)-linear combinations of indices, and let \(\tilde\tau\) act on such a combination by replacing each index with its SZ dual index. Let \(w\) be an SZ-admissible index and let \(x\) be a \(\mathbb{Q}\)-linear combination of SZ-admissible indices with \(V(x) = \tilde\tau(V(w))\). Then \(\zeta_q^{\mathrm{OOZ}}(x) = \zeta_q^{\mathrm{OOZ}}(w)\).

Since \(V\) is a bijection on combinations of SZ-admissible indices (Proposition 12 (ii) of the source), this is the identity \(\zeta_q^{\mathrm{OOZ}} = \zeta_q^{\mathrm{OOZ}} \circ V^{-1} \circ \tilde\tau \circ V\) on SZ-admissible indices.

public theorem_wanted sum_oozQMZV_eq_of_oozToSZ_eq_szDual (w : List ℕ)
    (hw₁ : ∀ a ∈ w.head?, 1 ≤ a) (x : List ℕ →₀ ℚ)
    (hx : x ∈ Finsupp.supported ℚ ℚ {v : List ℕ | ∀ a ∈ v.head?, 1 ≤ a})
    (hVx : Finsupp.linearCombination ℚ oozToSZ x = (oozToSZ w).mapDomain szDualIndex) :
    (x.sum fun v c => c • oozQMZV v) = oozQMZV w

Sources

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

Uses 3

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · The map \(V\) from OOZ to SZ words · The SZ dual index

13 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.