General q-multiple zeta values to Sums over partitions are invariant under transposition

DefinitionGeneral q-multiple zeta values#✓fully proved

For natural numbers \(k_1, \dots, k_r\) and polynomials \(Q_1, \dots, Q_r \in \mathbb{Q}[X]\), the general qMZV \(\zeta_q(k_1, \dots, k_r; Q_1, \dots, Q_r)\) is the formal power series in \(q\) over \(\mathbb{Q}\) whose coefficient of \(q^N\), for every \(N\), is the coefficient of \(q^N\) in the finite sum \(\sum_{N \ge m_1 > m_2 > \dots > m_r > 0} \prod_{j=1}^{r} Q_j(q^{m_j}) / (1 - q^{m_j})^{k_j}\) over integers \(m_1, \dots, m_r\), and \(\zeta_q(\varnothing; \varnothing) = 1\).

When \(Q_1(0) = 0\) (the paper's condition \(Q_1 \in X \mathbb{Q}[X]\)), the summands with \(m_1 > N\) have \(q\)-adic order greater than \(N\), so this is the series \(\sum_{m_1 > \dots > m_r > 0} \prod_{j=1}^{r} Q_j(q^{m_j}) / (1 - q^{m_j})^{k_j}\); for other data the value is a junk value.

public noncomputable def qMZV : List (ℕ × Polynomial ℚ) → ℚ⟦X⟧
  | [] => 1
  | (k, Q) :: kQ => PowerSeries.mk fun N => coeff N (∑ m ∈ Finset.Ioo 0 (N + 1),
      Polynomial.aeval (X ^ m : ℚ⟦X⟧) Q * ((1 - X ^ m)⁻¹) ^ k * qMZVPartial kQ m)

Sources

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

Uses 1 · Used by 14

Statement usesPartial sums of general qMZVs

Used byBradley–Zhao q-multiple zeta values · Nonempty general qMZVs have no constant term · The constant series one lies in every space of qMZVs · General qMZV of the empty index · Spaces of general qMZVs · Coefficients of qMZVs as polynomial functions on partitions · Quasi-shuffle relations for general qMZVs · Analytic properties of general qMZVs · Takeyama–Bradley–Zhao qMZVs · Okounkov \(q\)-multiple zeta values · The constant \(1\) lies in \(\mathcal{Z}^\circ_{q,d}\) · The spaces \(\mathcal{Z}^\circ_{q,d}\) · \(\mathcal{Z}^\circ_{q,d}\) is contained in \(\mathcal{Z}_{q,d}\) · The TBZ model extends the BZ model

TheoremGeneral qMZV of the empty index#✓fully proved

The general q-multiple zeta value of the empty data is \(\zeta_q(\varnothing; \varnothing) = 1\).

public theorem qMZV_nil : qMZV [] = 1

Sources

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

Uses 1

Statement usesGeneral q-multiple zeta values

TheoremNonempty general qMZVs have no constant term#✓fully proved

For every nonempty list \((k_1, Q_1), \dots, (k_r, Q_r)\) of natural numbers \(k_j\) and polynomials \(Q_j \in \mathbb{Q}[X]\), the constant coefficient of the general q-multiple zeta value \(\zeta_q(k_1, \dots, k_r; Q_1, \dots, Q_r)\) is \(0\). No condition on \(Q_1(0)\) is assumed.

public theorem coeff_zero_qMZV_cons (k : ℕ) (Q : Polynomial ℚ) (kQ : List (ℕ × Polynomial ℚ)) :
    coeff 0 (qMZV ((k, Q) :: kQ)) = 0

Sources

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

Uses 2 · Used by 1

Statement usesGeneral q-multiple zeta values

Proof usesPartial sums of general qMZVs

Used byNonempty Bradley–Zhao qMZVs have no constant term

DefinitionSpaces of general qMZVs#✓fully proved

For a natural number \(d\), \(\mathcal{Z}_{q,d}\) is the \(\mathbb{Q}\)-subspace of the formal power series \(\mathbb{Q}[[q]]\) spanned by 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]\) with \(\deg Q_j + d \le k_j\) for every \(j\) (the zero polynomial counting as degree \(0\)) and \(Q_1(0) = 0\) when \(r \ge 1\).

The space \(\mathcal{Z}_q := \mathcal{Z}_{q,0}\) is the space of qMZVs (with \(k_j \ge 0\)); for \(d = 1\) the degree condition forces \(k_j \ge 1\).

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

Sources

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

Uses 1 · Used by 7

Statement usesGeneral q-multiple zeta values

Used byThe constant series one lies in every space of qMZVs · Spanning sets of Ohno–Okuda–Zudilin qMZVs · Spanning set of Bradley–Zhao qMZVs · Spanning set of Schlesinger–Zudilin qMZVs · Polynomial functions on partitions characterize \(\mathcal{Z}_q\) · \(\mathcal{Z}^\circ_{q,d}\) is contained in \(\mathcal{Z}_{q,d}\) · The Takeyama–Bradley–Zhao model spans \(\mathcal{Z}_q\)

TheoremThe constant series one lies in every space of qMZVs#✓fully proved

For every natural number \(d\), the constant power series \(1\) lies in the \(\mathbb{Q}\)-span \(\mathcal{Z}_{q,d}\) of the general q-multiple zeta values \(\zeta_q(k_1, \dots, k_r; Q_1, \dots, Q_r)\) with \(Q_1(0) = 0\) and \(\deg Q_j + d \le k_j\) for all \(j\), where the zero polynomial is given degree \(0\); it is the qMZV of the empty index.

public theorem one_mem_qMZVSpace (d : ℕ) : (1 : ℚ⟦X⟧) ∈ qMZVSpace d

Sources

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

Uses 2

Statement usesSpaces of general qMZVs

Proof usesGeneral q-multiple zeta values

DefinitionBradley–Zhao q-multiple zeta values#✓fully proved

For an index \(k = (k_1, \dots, k_r)\) of natural numbers, the Bradley–Zhao q-multiple zeta value is the general qMZV \(\zeta_q^{BZ}(k) = \zeta_q(k_1, \dots, k_r; X^{k_1 - 1}, \dots, X^{k_r - 1})\), a formal power series in \(q\) over \(\mathbb{Q}\), where \(k_j - 1\) is truncated at \(0\). For an admissible index (\(k_1 \ge 2\) and all \(k_i \ge 1\)) it equals

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

for other indices the value has no intended meaning.

public noncomputable def bzQMZV (k : List ℕ) : ℚ⟦X⟧ :=
  qMZV (k.map fun k => (k, Polynomial.X ^ (k - 1)))

Sources

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

Uses 1 · Used by 9

Statement usesGeneral q-multiple zeta values

Used byBradley–Zhao duality for q-multiple zeta values · Bradley–Zhao qMZV of the empty index · Nonempty Bradley–Zhao qMZVs have no constant term · Spanning set of Bradley–Zhao qMZVs · q-Ohno relations for Bradley–Zhao qMZVs · Quasi-shuffle relations for Bradley–Zhao qMZVs · The TBZ model extends the BZ model · Brackets, Okounkov qMZVs and Bradley–Zhao qMZVs span \(\mathcal{Z}^\circ_{q,1}\) · OOZ-qMZVs of admissible indices via BZ-qMZVs

TheoremBradley–Zhao qMZV of the empty index#✓fully proved

The Bradley–Zhao q-multiple zeta value of the empty index is \(\zeta_q^{BZ}(\varnothing) = 1\).

public theorem bzQMZV_nil : bzQMZV [] = 1

Sources

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

Uses 1

Statement usesBradley–Zhao q-multiple zeta values

TheoremNonempty Bradley–Zhao qMZVs have no constant term#✓fully proved

For every nonempty index \((k_1, \dots, k_r)\) of natural numbers, the constant coefficient of the Bradley–Zhao q-multiple zeta value \(\zeta_q^{BZ}(k_1, \dots, k_r)\) is \(0\).

public theorem coeff_zero_bzQMZV_cons (k : ℕ) (ks : List ℕ) :
    coeff 0 (bzQMZV (k :: ks)) = 0

Sources

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

Uses 2

Statement usesBradley–Zhao q-multiple zeta values

Proof usesNonempty general qMZVs have no constant term

DefinitionBlock index of a list of pairs#✓fully proved

The block index of a list \([(a_1, b_1), \dots, (a_r, b_r)]\) of pairs of natural numbers is the index \((a_1 + 1, \{1\}^{b_1 - 1}, \dots, a_r + 1, \{1\}^{b_r - 1})\), where \(\{1\}^n\) stands for \(n\) consecutive entries equal to \(1\) and \(b_j - 1\) is truncated at \(0\).

When all \(a_j, b_j \ge 1\) this is an admissible index; it corresponds to the word \(x^{a_1} y^{b_1} \cdots x^{a_r} y^{b_r}\) of the space \(\mathfrak{h}^0\) of admissible words in the letters \(x, y\), and the duality \(\tau\), the anti-automorphism of \(\mathbb{Q}\langle x, y \rangle\) exchanging \(x\) and \(y\), maps this word to the word of the block index of \([(b_r, a_r), \dots, (b_1, a_1)]\).

public def bzBlockIndex (ab : List (ℕ × ℕ)) : List ℕ :=
  (ab.map fun p => (p.1 + 1) :: List.replicate (p.2 - 1) 1).flatten

Sources

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

Used by 3

Used byBlock index of a prepended pair · Bradley–Zhao duality for q-multiple zeta values · q-Ohno relations for Bradley–Zhao qMZVs

TheoremBlock index of a prepended pair#✓fully proved

For natural numbers \(a, b\) and a list \(L\) of pairs of natural numbers, the block index of the list obtained by prepending \((a, b)\) to \(L\) consists of the entry \(a + 1\), followed by \(b - 1\) entries equal to \(1\) (none when \(b = 0\)), followed by the block index of \(L\).

public theorem bzBlockIndex_cons (a b : ℕ) (ab : List (ℕ × ℕ)) :
    bzBlockIndex ((a, b) :: ab) = (a + 1) :: (List.replicate (b - 1) 1 ++ bzBlockIndex ab)

Sources

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

Uses 1

Statement usesBlock index of a list of pairs

TheoremSpanning set of Schlesinger–Zudilin qMZVs#●ready to prove

Let \(\mathcal{Z}_q\) be the space \(\mathcal{Z}_{q,d}\) of general qMZVs for \(d = 0\). Then \(\mathcal{Z}_q\) is the \(\mathbb{Q}\)-span of the Schlesinger–Zudilin qMZVs \(\zeta_q^{\mathrm{SZ}}(k_1, \dots, k_r)\) over all indices of natural numbers with \(k_1 \ge 1\) when \(r \ge 1\) (including the empty index, with \(\zeta_q^{\mathrm{SZ}}(\varnothing) = 1\)). Moreover, \(\mathcal{Z}_q\) is closed under the operator \(q \frac{d}{dq}\): for every \(f \in \mathcal{Z}_q\), the series \(q f'\) lies in \(\mathcal{Z}_q\), where \(f'\) is the formal derivative of \(f\).

public theorem_wanted qMZVSpace_zero_eq_span_szQMZV :
    qMZVSpace 0 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ k₁ ∈ k.head?, 1 ≤ k₁) ∧ f = szQMZV k} ∧
      ∀ f ∈ qMZVSpace 0, X * derivative f ∈ qMZVSpace 0

Sources

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

Uses 2

Statement usesSpaces of general qMZVs · Schlesinger–Zudilin qMZVs

TheoremSpanning set of Bradley–Zhao qMZVs#●ready to prove

Let \(\mathcal{Z}_{q,1}\) be the space \(\mathcal{Z}_{q,d}\) of general qMZVs for \(d = 1\). Then \(\mathcal{Z}_{q,1}\) is the \(\mathbb{Q}\)-span of the Bradley–Zhao qMZVs \(\zeta_q^{\mathrm{BZ}}(k_1, \dots, k_r)\) over all admissible indices, that is, all indices of natural numbers with \(k_i \ge 1\) for every \(i\) and \(k_1 \ge 2\) when \(r \ge 1\) (including the empty index, with \(\zeta_q^{\mathrm{BZ}}(\varnothing) = 1\)).

public theorem_wanted qMZVSpace_one_eq_span_bzQMZV :
    qMZVSpace 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 1 ≤ kᵢ) ∧ (∀ k₁ ∈ k.head?, 2 ≤ k₁) ∧ f = bzQMZV k}

Sources

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

Uses 2

Statement usesBradley–Zhao q-multiple zeta values · Spaces of general qMZVs

TheoremSpanning sets of Ohno–Okuda–Zudilin qMZVs#●ready to prove

Let \(\mathcal{Z}_{q,1}\) and \(\mathcal{Z}_q\) be the spaces \(\mathcal{Z}_{q,d}\) of general qMZVs for \(d = 1\) and \(d = 0\). Then (i) \(\mathcal{Z}_{q,1}\) is the \(\mathbb{Q}\)-span of the Ohno–Okuda–Zudilin qMZVs \(\zeta_q^{\mathrm{OOZ}}(k_1, \dots, k_r)\) over all indices of natural numbers with \(k_i \ge 1\) for every \(i\) and \(k_1 \ge 2\) when \(r \ge 1\); and (ii) \(\mathcal{Z}_q\) is the \(\mathbb{Q}\)-span of the \(\zeta_q^{\mathrm{OOZ}}(k_1, \dots, k_r)\) over all indices of natural numbers with \(k_1 \ge 1\) when \(r \ge 1\). Both spanning sets contain the empty index, with \(\zeta_q^{\mathrm{OOZ}}(\varnothing) = 1\).

public theorem_wanted qMZVSpace_eq_span_oozQMZV :
    qMZVSpace 1 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ kᵢ ∈ k, 1 ≤ kᵢ) ∧ (∀ k₁ ∈ k.head?, 2 ≤ k₁) ∧ f = oozQMZV k} ∧
      qMZVSpace 0 = Submodule.span ℚ {f | ∃ k : List ℕ,
        (∀ k₁ ∈ k.head?, 1 ≤ k₁) ∧ f = oozQMZV k}

Sources

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

Uses 2

Statement usesOhno–Okuda–Zudilin q-multiple zeta values · Spaces of general qMZVs

TheoremBradley–Zhao duality for q-multiple zeta values#●ready to prove

For every \(r \ge 0\) and all natural numbers \(a_1, b_1, \dots, a_r, b_r \ge 1\), the Bradley–Zhao q-multiple zeta values satisfy

\[\zeta_q^{BZ}(a_1 + 1, \{1\}^{b_1 - 1}, \dots, a_r + 1, \{1\}^{b_r - 1}) = \zeta_q^{BZ}(b_r + 1, \{1\}^{a_r - 1}, \dots, b_1 + 1, \{1\}^{a_1 - 1}),\]

where \(\{1\}^n\) stands for \(n\) consecutive entries equal to \(1\).

In terms of words this is \(\zeta_q^{BZ} \circ \tau = \zeta_q^{BZ}\) on the space \(\mathfrak{h}^0\) of admissible words, where \(\tau\) is the anti-automorphism of \(\mathbb{Q}\langle x, y \rangle\) exchanging \(x\) and \(y\).

public theorem_wanted bzQMZV_bzBlockIndex_dual (ab : List (ℕ × ℕ))
    (hab : ∀ p ∈ ab, 1 ≤ p.1 ∧ 1 ≤ p.2) :
    bzQMZV (bzBlockIndex ab) = bzQMZV (bzBlockIndex (ab.reverse.map Prod.swap))

Sources

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

Uses 2

Statement usesBlock index of a list of pairs · Bradley–Zhao q-multiple zeta values

Theoremq-Ohno relations for Bradley–Zhao qMZVs#●ready to prove

Let \((a_1, b_1), \dots, (a_r, b_r)\) be pairs of positive integers, write \(\{1\}^{n}\) for \(n\) repetitions of \(1\), let \(\mathbf{k} = (a_1 + 1, \{1\}^{b_1 - 1}, \dots, a_r + 1, \{1\}^{b_r - 1})\) be the admissible index they determine, of depth \(\ell\), and let \(\mathbf{k}^\vee = (b_r + 1, \{1\}^{a_r - 1}, \dots, b_1 + 1, \{1\}^{a_1 - 1})\) be its dual, of depth \(\ell^\vee\). Then for every natural number \(c\), \(\sum_{\mathbf{c}} \zeta_q^{\mathrm{BZ}}(\mathbf{k} + \mathbf{c}) = \sum_{\mathbf{c}'} \zeta_q^{\mathrm{BZ}}(\mathbf{k}^\vee + \mathbf{c}')\), where \(\mathbf{c}\) runs over the tuples in \(\mathbb{N}^{\ell}\) and \(\mathbf{c}'\) over the tuples in \(\mathbb{N}^{\ell^\vee}\) whose entries sum to \(c\), and indices are added componentwise.

public theorem_wanted sum_bzQMZV_add_eq_sum_bzQMZV_dual_add (ab : List (ℕ × ℕ))
    (hab : ∀ p ∈ ab, 1 ≤ p.1 ∧ 1 ≤ p.2) (c : ℕ) :
    ∑ cs ∈ Finset.Nat.antidiagonalTuple (bzBlockIndex ab).length c,
        bzQMZV (List.zipWith (· + ·) (bzBlockIndex ab) (List.ofFn cs)) =
      ∑ cs ∈ Finset.Nat.antidiagonalTuple
          (bzBlockIndex (ab.reverse.map Prod.swap)).length c,
        bzQMZV (List.zipWith (· + ·) (bzBlockIndex (ab.reverse.map Prod.swap)) (List.ofFn cs))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Theorem 8 (q-Ohno relations, Okuda–Takeyama).

Uses 2

Statement usesBlock index of a list of pairs · Bradley–Zhao q-multiple zeta values

DefinitionPartitions in Stanley coordinates#✓fully proved

For natural numbers \(r\) and \(N\), \(\mathcal{P}_r(N)\) is the finite set of partitions of \(N\) of length \(r\) in Stanley coordinates: the pairs of tuples \(((m_1, \dots, m_r), (n_1, \dots, n_r))\) of positive integers with \(m_1 > m_2 > \dots > m_r\) and \(m_1 n_1 + \dots + m_r n_r = N\).

All coordinates of such a pair are then at most \(N\).

public def stanleyPartitions (r N : ℕ) : Finset ((Fin r → ℕ) × (Fin r → ℕ)) :=
  ((Fintype.piFinset fun _ : Fin r => Finset.Icc 1 N) ×ˢ
      (Fintype.piFinset fun _ : Fin r => Finset.Icc 1 N)).filter
    fun p => (∀ i j : Fin r, i < j → p.1 j < p.1 i) ∧ ∑ j, p.1 j * p.2 j = N

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of Stanley coordinates and of 𝒫_r(N) (Section 4).

Used by 4

Used byMembership criterion for partitions in Stanley coordinates · Sums over partitions are invariant under transposition · Coefficients of qMZVs as polynomial functions on partitions · Polynomial functions on partitions characterize \(\mathcal{Z}_q\)

TheoremMembership criterion for partitions in Stanley coordinates#✓fully proved

For natural numbers \(r\) and \(N\), a pair \(((m_1, \dots, m_r), (n_1, \dots, n_r))\) of \(r\)-tuples of natural numbers lies in the set \(\mathcal{P}_r(N)\) of partitions of \(N\) of length \(r\) in Stanley coordinates if and only if \(m_1 > m_2 > \dots > m_r\), every \(m_j\) and every \(n_j\) is positive, and \(m_1 n_1 + \dots + m_r n_r = N\).

public theorem mem_stanleyPartitions {r N : ℕ} {p : (Fin r → ℕ) × (Fin r → ℕ)} :
    p ∈ stanleyPartitions r N ↔
      (∀ i j : Fin r, i < j → p.1 j < p.1 i) ∧ (∀ j, 0 < p.1 j) ∧ (∀ j, 0 < p.2 j) ∧
        ∑ j, p.1 j * p.2 j = N

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Definition of 𝒫_r(N) (Section 4).

Uses 1

Statement usesPartitions in Stanley coordinates

DefinitionTransposed partition in Stanley coordinates#✓fully proved

For tuples \(\mathbf{m} = (m_1, \dots, m_r)\) and \(\mathbf{n} = (n_1, \dots, n_r)\) of natural numbers, the transpose \(\rho(\mathbf{m}, \mathbf{n})\) is the pair of tuples \(((n_1 + \dots + n_r, \dots, n_1 + n_2, n_1), (m_r, m_{r-1} - m_r, \dots, m_1 - m_2))\): for \(1 \le j \le r\), the \(j\)-th entry of the first tuple is \(n_1 + \dots + n_{r+1-j}\) and the \(j\)-th entry of the second tuple is \(m_{r+1-j} - m_{r+2-j}\), where \(m_{r+1} := 0\) and subtraction of natural numbers is truncated at \(0\).

On a partition with \(m_1 > \dots > m_r\) this reflects its Young diagram in the main diagonal.

public def stanleyTranspose {r : ℕ} (p : (Fin r → ℕ) × (Fin r → ℕ)) :
    (Fin r → ℕ) × (Fin r → ℕ) :=
  (fun j => ∑ i : Fin r with i.val + j.val < r, p.2 i,
    fun j => p.1 (Fin.rev j) -
      (if h : (Fin.rev j).val + 1 < r then p.1 ⟨(Fin.rev j).val + 1, h⟩ else 0))

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Section 4, transposed partition in Stanley coordinates.

Used by 2

Used byTranspose of a one-part partition · Sums over partitions are invariant under transposition

TheoremTranspose of a one-part partition#✓fully proved

For all natural numbers \(m\) and \(n\), the transpose \(\rho\) in Stanley coordinates sends the pair of one-entry tuples \(((m), (n))\) to \(((n), (m))\).

public theorem stanleyTranspose_fin_one (m n : Fin 1 → ℕ) :
    stanleyTranspose (m, n) = (n, m)

Sources

• Benjamin Brindle, A Unified Approach to qMZVs, INTEGERS 24 (2024), Article A6, Section 4, transposed partition in Stanley coordinates.

Uses 1

Statement usesTransposed partition in Stanley coordinates

TheoremSums over partitions are invariant under transposition#●ready to prove

For all natural numbers \(r\) and \(N\) and every function \(a\) from pairs of \(r\)-tuples of natural numbers to \(\mathbb{Q}\), \(\sum_{p \in \mathcal{P}_r(N)} a(p) = \sum_{p \in \mathcal{P}_r(N)} a(\rho(p))\), where \(\mathcal{P}_r(N)\) is the set of partitions of \(N\) of length \(r\) in Stanley coordinates and \(\rho\) is the transpose map.

public theorem_wanted sum_stanleyPartitions_comp_stanleyTranspose (r N : ℕ)
    (a : (Fin r → ℕ) × (Fin r → ℕ) → ℚ) :
    ∑ p ∈ stanleyPartitions r N, a p = ∑ p ∈ stanleyPartitions r N, a (stanleyTranspose p)

Sources

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

Uses 2

Statement usesPartitions in Stanley coordinates · Transposed partition in Stanley coordinates

14 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.