The logarithm series \(\ln(1 + T)\) to Weighted chain sums

DefinitionThe logarithm series \(\ln(1 + T)\)#✓fully proved

The formal power series \(\ln(1 + T)\) over \(\mathbb{Q}\) is \(\sum_{n \ge 1} (-1)^{n+1} T^n / n\); its constant term is \(0\).

public noncomputable def logOneAddSeries : ℚ⟦X⟧ :=
  PowerSeries.mk fun n => if n = 0 then 0 else (-1) ^ (n + 1) / n

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 13 (ii) (the substitution Xⱼ ↦ ln(Xⱼ + 1)).

Used by 2

Used byTranslation between bi-brackets and the Schlesinger–Zudilin model · Low-order coefficients of the logarithm series

TheoremLow-order coefficients of the logarithm series#✓fully proved

The power series \(\ln(1 + T) = \sum_{n \ge 1} (-1)^{n+1} T^n / n\) over \(\mathbb{Q}\) has constant coefficient \(0\) and coefficient \(1\) at \(T\).

public theorem coeff_logOneAddSeries_zero_one :
    coeff 0 logOneAddSeries = 0 ∧ coeff 1 logOneAddSeries = 1

Sources

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

Uses 1

Statement usesThe logarithm series \(\ln(1 + T)\)

TheoremBi-bracket generating series as a sum of exponentials#●ready to prove

Let \(r\) and \(N\) be natural numbers and let \(g(X_1, \dots, X_r; Y_1, \dots, Y_r)\) be the generating series of bi-brackets of depth \(r\), a power series in the \(2r\) variables over \(\mathbb{Q}[[q]]\). The power series over \(\mathbb{Q}\) obtained by taking the coefficient of \(q^N\) in every coefficient of \(g\) equals the finite sum

\[\sum \prod_{j=1}^r e^{m_j Y_j} e^{n_j X_j}\]

over all integers \(m_1 > m_2 > \dots > m_r > 0\) and \(n_1, \dots, n_r \ge 1\) with \(m_1 n_1 + \dots + m_r n_r = N\), where \(e^Z\) is the exponential series evaluated at \(Z\).

This is the \(q^N\)-part of the identity \(g(X; Y) = \sum \prod_j e^{m_j Y_j} e^{n_j X_j} q^{m_j n_j}\).

public theorem_wanted coeff_biBracketGen_eq_sum_exp (r N : ℕ) :
    (fun e => coeff N (MvPowerSeries.coeff e (biBracketGen r)) :
        MvPowerSeries (Fin r ⊕ Fin r) ℚ) =
      ∑ mn ∈ (Fintype.piFinset fun _ : Fin r => Finset.range (N + 1)) ×ˢ
          (Fintype.piFinset fun _ : Fin r => Finset.range (N + 1)) with
          StrictAnti mn.1 ∧ (∀ j, 0 < mn.1 j) ∧ (∀ j, 0 < mn.2 j) ∧
            ∑ j, mn.1 j * mn.2 j = N,
        ∏ j : Fin r,
          PowerSeries.subst ((mn.1 j : ℚ) • MvPowerSeries.X (Sum.inr j)) (exp ℚ) *
            PowerSeries.subst ((mn.2 j : ℚ) • MvPowerSeries.X (Sum.inl j)) (exp ℚ)

Sources

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

Uses 1

Statement usesGenerating series of bi-brackets

TheoremPartition relation for bi-brackets#●ready to prove

For every natural number \(r\), the generating series \(g(X_1, \dots, X_r; Y_1, \dots, Y_r)\) of bi-brackets of depth \(r\) satisfies

\[g(X_1, \dots, X_r; Y_1, \dots, Y_r) = g(Y_1 + \dots + Y_r, \dots, Y_1 + Y_2, Y_1; X_r, X_{r-1} - X_r, \dots, X_1 - X_2),\]

where the right side substitutes linear forms into \(g\) simultaneously: for \(1 \le i \le r\), the variable \(X_i\) is replaced by \(Y_1 + \dots + Y_{r+1-i}\) and the variable \(Y_i\) by \(X_{r+1-i} - X_{r+2-i}\), with \(X_{r+1} := 0\).

public theorem_wanted biBracketGen_partition_relation (r : ℕ) :
    biBracketGen r = MvPowerSeries.subst
      (Sum.elim
        (fun i : Fin r => ∑ j ∈ Finset.univ.filter (fun j : Fin r => j.val < r - i.val),
          MvPowerSeries.X (Sum.inr j))
        (fun i : Fin r => MvPowerSeries.X (Sum.inl i.rev) -
          ∑ j ∈ Finset.univ.filter (fun j : Fin r => j.val = r - i.val),
            MvPowerSeries.X (Sum.inl j)))
      (biBracketGen r)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 12 (partition relation, after Bachmann).

Uses 1

Statement usesGenerating series of bi-brackets

TheoremTranslation between bi-brackets and the Schlesinger–Zudilin model#●ready to prove

Let \(r\) be a natural number, let \(g(X_1, \dots, X_r; Y_1, \dots, Y_r)\) be the generating series of bi-brackets of depth \(r\) and \(s(X_1, \dots, X_r; Y_1, \dots, Y_r)\) the generating series of Schlesinger–Zudilin qMZVs of depth \(r\), both power series in the \(2r\) variables over \(\mathbb{Q}[[q]]\). For a power series \(Z\) without constant term, write \(e^Z\) and \(\ln(1 + Z)\) for the substitution of \(Z\) into the exponential series and into \(\ln(1 + T) = \sum_{n \ge 1} (-1)^{n+1} T^n / n\), and put \(S_j = Y_1 + \dots + Y_j\). Then:

(i) \(\prod_{j=1}^r e^{X_j} e^{S_j} \cdot s(e^{X_1} - 1, \dots, e^{X_r} - 1; e^{S_1} - 1, \dots, e^{S_r} - 1) = g(X_1, \dots, X_r; Y_1, \dots, Y_r)\);

(ii) \(\prod_{j=1}^r (1 + X_j)(1 + Y_j) \cdot s(X_1, \dots, X_r; Y_1, \dots, Y_r)\) equals \(g(\ln(1 + X_1), \dots, \ln(1 + X_r); \ln(1 + Y_1), \ln(1 + Y_2) - \ln(1 + Y_1), \dots, \ln(1 + Y_r) - \ln(1 + Y_{r-1}))\).

Part (ii) is stated with the unit \(\prod_j (1 + X_j)(1 + Y_j)\) multiplied out instead of inverted.

MetaMathlibExt.biBracketGen_eq_szGen_subst · 25 lines

public theorem_wanted biBracketGen_eq_szGen_subst (r : ℕ) :
    (∏ j : Fin r,
        PowerSeries.subst (MvPowerSeries.X (Sum.inl j) :
            MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧) (exp ℚ) *
          PowerSeries.subst (∑ i ∈ Finset.Iic j,
            (MvPowerSeries.X (Sum.inr i) : MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧)) (exp ℚ)) *
        MvPowerSeries.subst
          (Sum.elim
            (fun j : Fin r => PowerSeries.subst (MvPowerSeries.X (Sum.inl j) :
              MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧) (exp ℚ) - 1)
            (fun j : Fin r => PowerSeries.subst (∑ i ∈ Finset.Iic j,
              (MvPowerSeries.X (Sum.inr i) : MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧)) (exp ℚ) - 1))
          (szGen r) = biBracketGen r ∧
    (∏ j : Fin r, (1 + MvPowerSeries.X (Sum.inl j)) * (1 + MvPowerSeries.X (Sum.inr j))) *
        szGen r =
      MvPowerSeries.subst
        (Sum.elim
          (fun j : Fin r => PowerSeries.subst (MvPowerSeries.X (Sum.inl j) :
            MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧) logOneAddSeries)
          (fun j : Fin r => PowerSeries.subst (MvPowerSeries.X (Sum.inr j) :
              MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧) logOneAddSeries -
            ∑ i ∈ Finset.univ.filter (fun i : Fin r => i.val + 1 = j.val),
              PowerSeries.subst (MvPowerSeries.X (Sum.inr i) :
                MvPowerSeries (Fin r ⊕ Fin r) ℚ⟦X⟧) logOneAddSeries))
        (biBracketGen r)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 13 (translation bi-brackets/SZ model).

Uses 3

Statement usesGenerating series of bi-brackets · The logarithm series \(\ln(1 + T)\) · Generating series of Schlesinger–Zudilin qMZVs

TheoremGenerating series of OOZ-qMZVs, coefficientwise#●ready to prove

Let \(r\) and \(N\) be natural numbers and let \(k_1, \dots, k_r \ge 1\) and \(d_1, \dots, d_r \ge 0\) be integers. Writing \(\{0\}^d\) for \(d\) consecutive zeros, the coefficient of \(q^N\) in the Ohno–Okuda–Zudilin qMZV \(\zeta_q^{\mathrm{OOZ}}(k_1, \{0\}^{d_1}, \dots, k_r, \{0\}^{d_r})\) equals the coefficient of \(q^N\) in

\[\sum q^{m_1} \prod_{j=1}^r \binom{m_j - m_{j+1} - 1}{d_j} \frac{1}{(1 - q^{m_j})^{k_j}},\]

the sum running over integers \(N \ge m_1 > m_2 > \dots > m_r > 0\), where \(m_{r+1} := 0\) and the factor \(q^{m_1}\) is read as \(1\) when \(r = 0\).

In the untruncated sum, the summands with \(m_1 > N\) have \(q\)-adic order greater than \(N\). Let \(\mathfrak{oz}(X; Y)\) be the paper's generating series of OOZ-qMZVs of depth \(r\) in the variables \(X_1, \dots, X_r\) and \(Y_1, \dots, Y_r\) over \(\mathbb{Q}[[q]]\). The statement compares the coefficients of \(\prod_j X_j^{k_j}/k_j! \, Y_j^{d_j}\) on both sides of the paper's identity \(\mathfrak{oz}(X; Y) = \sum q^{m_1} \prod_j (1 + Y_j)^{m_j - m_{j+1} - 1} (e^{X_j/(1 - q^{m_j})} - 1)\).

public theorem_wanted coeff_oozQMZV_szBlockIndex_eq_sum_choose (r : ℕ) (k d : Fin r → ℕ)
    (hk : ∀ j, 1 ≤ k j) (N : ℕ) :
    coeff N (oozQMZV (szBlockIndex (List.ofFn fun j => (k j, d j + 1)))) =
      coeff N (∑ m ∈ (Fintype.piFinset fun _ : Fin r => Finset.range (N + 1)) with
          StrictAnti m ∧ ∀ j, 0 < m j,
        X ^ (if h : 0 < r then m ⟨0, h⟩ else 0) *
          ∏ j : Fin r, ((((m j - (if h : j.val + 1 < r then m ⟨j.val + 1, h⟩ else 0) - 1).choose
            (d j) : ℕ) : ℚ⟦X⟧) * ((1 - X ^ m j)⁻¹) ^ k j))

Sources

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

Uses 2

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · Block indices for Schlesinger–Zudilin qMZVs

TheoremBrackets, Okounkov qMZVs and Bradley–Zhao qMZVs span \(\mathcal{Z}^\circ_{q,1}\)#●ready to prove

For an index \(k = (k_1, \dots, k_r)\) of natural numbers let \(g(k) = g(k_1, \dots, k_r; 0, \dots, 0)\) be the bracket, that is, the bi-bracket with all \(d_j = 0\), and let \(\zeta_q^{\mathrm{Oko}}(k)\) and \(\zeta_q^{BZ}(k)\) be the Okounkov and Bradley–Zhao qMZVs. Then the space \(\mathcal{Z}^\circ_{q,1}\) equals the \(\mathbb{Q}\)-linear span of the brackets \(g(k)\), equals the \(\mathbb{Q}\)-linear span of the Okounkov qMZVs \(\zeta_q^{\mathrm{Oko}}(k)\), and equals the \(\mathbb{Q}\)-linear span of the Bradley–Zhao qMZVs \(\zeta_q^{BZ}(k)\), where in each case \(k\) runs over all indices of length \(r \ge 0\) with every \(k_i \ge 2\).

public theorem_wanted qMZVSpaceCirc_one_eq_span_bracket_okounkov_bz :
    qMZVSpaceCirc 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 2 ≤ kᵢ) ∧ f = biBracket (k.map fun kᵢ => (kᵢ, 0))} ∧
      qMZVSpaceCirc 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 2 ≤ kᵢ) ∧ f = okounkovQMZV k} ∧
      qMZVSpaceCirc 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 2 ≤ kᵢ) ∧ f = bzQMZV k}

Sources

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

Uses 4

Statement usesBi-brackets · Bradley–Zhao q-multiple zeta values · Okounkov \(q\)-multiple zeta values · The spaces \(\mathcal{Z}^\circ_{q,d}\)

DefinitionWeighted quasi-shuffle product#✓fully proved

Let \(A\) be an alphabet and let \(d\) assign to any two letters \(a, b \in A\) a finite formal \(\mathbb{Q}\)-linear combination \(d(a, b) = \sum_c d(a, b)_c \, c\) of letters. The weighted quasi-shuffle product \(u \ast v\) of two words over \(A\) is the finite formal \(\mathbb{Q}\)-linear combination of words defined by recursion on total length: \(\mathbf{1} \ast w = w \ast \mathbf{1} = w\) for the empty word \(\mathbf{1}\), and for letters \(a, b\) and words \(u, v\), \(a u \ast b v = a (u \ast b v) + b (a u \ast v) + \sum_c d(a, b)_c \, c (u \ast v)\), where prefixing a letter is extended linearly to combinations of words.

public noncomputable def weightedQuasiShuffle {α : Type*} (d : α → α → (α →₀ ℚ)) :
    List α → List α → (List α →₀ ℚ)
  | [], v => Finsupp.single v 1
  | a :: u, [] => Finsupp.single (a :: u) 1
  | a :: u, b :: v =>
      (weightedQuasiShuffle d u (b :: v)).mapDomain (a :: ·) +
        (weightedQuasiShuffle d (a :: u) v).mapDomain (b :: ·) +
        (d a b).sum fun c x => x • (weightedQuasiShuffle d u v).mapDomain (c :: ·)
termination_by u v => u.length + v.length

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, quasi-shuffle products of Section 2 (with ℚ-valued letter product, as for bi-brackets).

Used by 2

Used byBi-brackets form a quasi-shuffle algebra · The empty word is a left unit for the weighted quasi-shuffle

TheoremThe empty word is a left unit for the weighted quasi-shuffle#✓fully proved

For every alphabet \(A\), every weighted letter product \(d\) on \(A\) (assigning to two letters a finite formal \(\mathbb{Q}\)-linear combination of letters) and every word \(v\) over \(A\), the weighted quasi-shuffle product of the empty word \(\mathbf{1}\) with \(v\) is \(v\): \(\mathbf{1} \ast v = v\).

public theorem weightedQuasiShuffle_nil_left {α : Type*} (d : α → α → (α →₀ ℚ)) (v : List α) :
    weightedQuasiShuffle d [] v = Finsupp.single v 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, quasi-shuffle products of Section 2.

Uses 1

Statement usesWeighted quasi-shuffle product

DefinitionBachmann's coefficients#✓fully proved

For natural numbers \(a\), \(b\) and \(j\),

\[\lambda_{a,b}^j = (-1)^{b-1} \binom{a + b - j - 1}{a - j} \frac{B_{a+b-j}}{(a + b - j)!},\]

where \(B_n\) is the \(n\)-th Bernoulli number with \(B_1 = -1/2\) and every subtraction of natural numbers is truncated at \(0\).

public noncomputable def biBracketLambda (a b j : ℕ) : ℚ :=
  (-1) ^ (b - 1) * ((a + b - j - 1).choose (a - j) : ℚ) * bernoulli (a + b - j) /
    (a + b - j).factorial

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the bi-bracket product ⊠ (after Bachmann).

Used by 2

Used byBachmann's product of bi-bracket letters · Bachmann's coefficient \(\lambda_{1,1}^1\)

TheoremBachmann's coefficient \(\lambda_{1,1}^1\)#✓fully proved

Bachmann's coefficient \(\lambda_{1,1}^1\) equals \(-1/2\), the Bernoulli number \(B_1\).

public theorem biBracketLambda_one_one_one : biBracketLambda 1 1 1 = -1 / 2

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the bi-bracket product ⊠.

Uses 1

Statement usesBachmann's coefficients

DefinitionBachmann's product of bi-bracket letters#✓fully proved

Write \(z_{k,d}\) for the letter indexed by a pair \((k, d)\) of natural numbers, and let \(\lambda_{a,b}^j\) be Bachmann's coefficients. The product of the letters \(z_{k_1,d_1}\) and \(z_{k_2,d_2}\) is the formal \(\mathbb{Q}\)-linear combination of letters

\[z_{k_1,d_1} \boxtimes z_{k_2,d_2} = \binom{d_1 + d_2}{d_1} \Big( \sum_{j=1}^{k_1} \lambda_{k_1,k_2}^j z_{j,d_1+d_2} + \sum_{j=1}^{k_2} \lambda_{k_2,k_1}^j z_{j,d_1+d_2} + z_{k_1+k_2,d_1+d_2} \Big).\]

public noncomputable def biBracketDiamond (x y : ℕ × ℕ) : (ℕ × ℕ) →₀ ℚ :=
  ((x.2 + y.2).choose x.2 : ℚ) •
    ((∑ j ∈ Finset.Icc 1 x.1, biBracketLambda x.1 y.1 j • Finsupp.single (j, x.2 + y.2) 1) +
      (∑ j ∈ Finset.Icc 1 y.1, biBracketLambda y.1 x.1 j • Finsupp.single (j, x.2 + y.2) 1) +
      Finsupp.single (x.1 + y.1, x.2 + y.2) 1)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the bi-bracket product ⊠ (after Bachmann).

Uses 1 · Used by 1

Statement usesBachmann's coefficients

Used byBi-brackets form a quasi-shuffle algebra

TheoremBi-brackets form a quasi-shuffle algebra#●ready to prove

Let \(u\) and \(v\) be words in the letters \(z_{k,d}\), indexed by pairs \((k, d)\) of natural numbers, with \(k \ge 1\) in every letter. Write \(\sum_w c_w w\) for the quasi-shuffle product of \(u\) and \(v\) induced by Bachmann's letter product \(\boxtimes\), a formal \(\mathbb{Q}\)-linear combination of words, and \(g(w)\) for the bi-bracket of a word \(w\). Then \(g(u) g(v) = \sum_w c_w g(w)\).

public theorem_wanted biBracket_mul_eq_sum_weightedQuasiShuffle (u v : List (ℕ × ℕ))
    (hu : ∀ p ∈ u, 1 ≤ p.1) (hv : ∀ p ∈ v, 1 ≤ p.1) :
    biBracket u * biBracket v =
      (weightedQuasiShuffle biBracketDiamond u v).sum fun w c => c • biBracket w

Sources

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

Uses 3

Statement usesBi-brackets · Bachmann's product of bi-bracket letters · Weighted quasi-shuffle product

DefinitionThe map \(T\) of the OOZ quasi-shuffle product#✓fully proved

Words are finite sequences of letters \(z_k\) with \(k\) a natural number. The map \(T\) sends each word to a finite formal \(\mathbb{Q}\)-linear combination of words: it sends the empty word \(\mathbf{1}\) to \(\mathbf{1}\), and a word \(z_n v\) with first letter \(z_n\) to \(z_n v - z_{n-1} v\), where \(n - 1\) is truncated at \(0\) (so \(T(z_0 v) = 0\)).

In the paper \(T\) is defined only on a subspace of the combinations of words; here it is defined on all words.

public noncomputable def oozT : List ℕ → (List ℕ →₀ ℚ)
  | [] => Finsupp.single [] 1
  | n :: v => Finsupp.single (n :: v) 1 - Finsupp.single ((n - 1) :: v) 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the OOZ quasi-shuffle product.

Used by 3

Used byOOZ qMZVs respect the OOZ quasi-shuffle product · The OOZ map fixes the empty word · The OOZ map on a one-letter word

TheoremThe OOZ map fixes the empty word#✓fully proved

Let \(T\) be the map of the OOZ quasi-shuffle product, which sends words in letters \(z_k\) (\(k\) a natural number) to finite formal \(\mathbb{Q}\)-linear combinations of words. Then \(T\) sends the empty word \(\mathbf{1}\) to itself: \(T(\mathbf{1}) = \mathbf{1}\).

public theorem oozT_nil : oozT [] = Finsupp.single [] 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the OOZ quasi-shuffle product.

Uses 1

Statement usesThe map \(T\) of the OOZ quasi-shuffle product

TheoremThe OOZ map on a one-letter word#✓fully proved

Let \(T\) be the map of the OOZ quasi-shuffle product, which sends words in letters \(z_k\) (\(k\) a natural number) to finite formal \(\mathbb{Q}\)-linear combinations of words. Then \(T\) sends the one-letter word \(z_2\) to \(z_2 - z_1\): \(T(z_2) = z_2 - z_1\).

public theorem oozT_singleton_two : oozT [2] = Finsupp.single [2] 1 - Finsupp.single [1] 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the OOZ quasi-shuffle product.

Uses 1

Statement usesThe map \(T\) of the OOZ quasi-shuffle product

DefinitionStuffle product of formal linear combinations of words#✓fully proved

On words in letters \(z_k\) (\(k\) a natural number), the stuffle product \(\ast\) is the quasi-shuffle product with letter product \(z_m \diamond z_n = z_{m+n}\): \(\mathbf{1} \ast w = w \ast \mathbf{1} = w\) for the empty word \(\mathbf{1}\), and \(z_m u \ast z_n v = z_m (u \ast z_n v) + z_n (z_m u \ast v) + z_{m+n} (u \ast v)\), counted with multiplicity. It is extended \(\mathbb{Q}\)-bilinearly to finite formal \(\mathbb{Q}\)-linear combinations of words: \(A \ast B = \sum_{a, b} A_a B_b \, (a \ast b)\), where \(A_a\) is the coefficient of the word \(a\) in \(A\).

public noncomputable def stuffleComb (A B : List ℕ →₀ ℚ) : List ℕ →₀ ℚ :=
  A.sum fun a x => B.sum fun b y =>
    (x * y) • ((quasiShuffle (fun m n => [m + n]) a b).map fun w => Finsupp.single w (1 : ℚ)).sum

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the stuffle product ∗ on 𝔥¹.

Uses 1 · Used by 2

Statement usesQuasi-shuffle product

Used byOOZ qMZVs respect the OOZ quasi-shuffle product · The empty word is a left unit for the stuffle product

TheoremThe empty word is a left unit for the stuffle product#✓fully proved

For every word \(b\) in letters \(z_k\) (\(k\) a natural number), the stuffle product of the empty word \(\mathbf{1}\) with \(b\) is \(b\): \(\mathbf{1} \ast b = b\), as formal \(\mathbb{Q}\)-linear combinations of words.

public theorem stuffleComb_single_nil (b : List ℕ) :
    stuffleComb (Finsupp.single [] 1) (Finsupp.single b 1) = Finsupp.single b 1

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of the stuffle product ∗ on 𝔥¹.

Uses 3

Statement usesStuffle product of formal linear combinations of words

Proof usesQuasi-shuffle product · The empty word is a left unit for the quasi-shuffle product

TheoremOOZ qMZVs respect the OOZ quasi-shuffle product#●ready to prove

Identify words in letters \(z_k\) with lists \((k_1, \dots, k_r)\) of natural numbers, and call such a word admissible if every \(k_i \ge 1\) and, when \(r \ge 1\), \(k_1 \ge 2\). Let \(T\) send the empty word \(\mathbf{1}\) to \(\mathbf{1}\) and a word \(z_n v\) with first letter \(z_n\) to the formal \(\mathbb{Q}\)-linear combination \(z_n v - z_{n-1} v\) (with \(n - 1\) truncated at \(0\)). Extend \(T\) and the Ohno–Okuda–Zudilin qMZV \(\zeta_q^{\mathrm{OOZ}}\) \(\mathbb{Q}\)-linearly to finite formal \(\mathbb{Q}\)-linear combinations of words, and let \(\ast\) be the stuffle product (the quasi-shuffle product with letter product \(z_m \diamond z_n = z_{m+n}\)) of such combinations. For all admissible words \(u\) and \(v\), there is exactly one finite formal \(\mathbb{Q}\)-linear combination \(w\) of admissible words with \(T(w) = T(u) \ast T(v)\), and every finite formal \(\mathbb{Q}\)-linear combination \(w\) of admissible words with \(T(w) = T(u) \ast T(v)\) satisfies \(\zeta_q^{\mathrm{OOZ}}(w) = \zeta_q^{\mathrm{OOZ}}(u) \, \zeta_q^{\mathrm{OOZ}}(v)\).

Thus the OOZ quasi-shuffle product, defined by \(T(u \ast_{\mathrm{OOZ}} v) = T(u) \ast T(v)\), is well defined, and \(\zeta_q^{\mathrm{OOZ}}\) is multiplicative for it.

public theorem_wanted oozQMZV_mul_eq_of_oozT_eq_stuffleComb (u v : List ℕ)
    (hu : ∀ k ∈ u, 1 ≤ k) (hu₁ : ∀ k₁ ∈ u.head?, 2 ≤ k₁)
    (hv : ∀ k ∈ v, 1 ≤ k) (hv₁ : ∀ k₁ ∈ v.head?, 2 ≤ k₁) :
    (∃! w : List ℕ →₀ ℚ, (∀ x ∈ w.support, (∀ k ∈ x, 1 ≤ k) ∧ ∀ k₁ ∈ x.head?, 2 ≤ k₁) ∧
        (w.sum fun x c => c • oozT x) = stuffleComb (oozT u) (oozT v)) ∧
      ∀ w : List ℕ →₀ ℚ, (∀ x ∈ w.support, (∀ k ∈ x, 1 ≤ k) ∧ ∀ k₁ ∈ x.head?, 2 ≤ k₁) →
        (w.sum fun x c => c • oozT x) = stuffleComb (oozT u) (oozT v) →
        (w.sum fun x c => c • oozQMZV x) = oozQMZV u * oozQMZV v

Sources

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

Uses 3

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · The map \(T\) of the OOZ quasi-shuffle product · Stuffle product of formal linear combinations of words

DefinitionWeighted chain sums#✓fully proved

Let \(o_1, \dots, o_\ell\) be a word of markers, each either a natural number (a weighted position) or a blank (an unweighted position); let \(W\) be the set of weighted positions and \(k_t\) the number at position \(t \in W\). For natural numbers \(M\) and \(R\), the weighted chain sum of the word at bound \(M\) and target \(R\) is the natural number

\[\sum \prod_{t \in W} \binom{j_t}{k_t},\]

the sum running over strictly decreasing chains \(M > a_1 > a_2 > \dots > a_\ell > 0\) of natural numbers and multiplicities \(j_1, \dots, j_\ell \ge 0\) with \(a_1 j_1 + \dots + a_\ell j_\ell = R\). For the empty word (\(\ell = 0\)) the sum has a single empty term, so the value is \(1\) if \(R = 0\) and \(0\) otherwise, whatever \(M\) is.

public def bzChainSum : List (Option ℕ) → ℕ → ℕ → ℕ
  | [], _, R => if R = 0 then 1 else 0
  | o :: os, M, R => ∑ m ∈ Finset.Ioo 0 M, ∑ j ∈ Finset.range (R / m + 1),
      (match o with
        | some k => j.choose k
        | none => 1) * bzChainSum os m (R - m * j)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 1 (the sums over m₁ > n₁ > ⋯ > m_r > ⋯ > 0 with multiplicities j, i ≥ 0).

Used by 2

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

13 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.