Cyclic sum formula

DefinitionThe index of a list of positive integers#✓fully proved

A list \((l_1, \dots, l_r)\) of positive integers determines the multiple-zeta index whose entries are \(l_1, \dots, l_r\) in this order; its weight is \(l_1 + \cdots + l_r\).

noncomputable def toIndex (l : List ℕ) (hpos : ∀ x ∈ l, 0 < x) :
    MultipleZeta.Index :=
  ⟨l.sum, ⟨l, fun {x} hx => hpos x hx, rfl⟩⟩
Uses 1 · Used by 6
Statement usesMultiple-zeta index
Used byCyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Left-hand indices of the cyclic sum formula · Left-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula · Right-hand indices of the cyclic sum formula are admissible or empty

DefinitionLeft-hand indices of the cyclic sum formula#✓fully proved

Let \(k = (k_1, \dots, k_l)\) be a list of positive integers, with subscripts read modulo \(l\). For \(1 \le j \le l\) and a natural number \(i\), the left-hand index of \(k\) at \((j, i)\) is the index \((k_j - i + 1, k_{j+1}, \dots, k_{j+l-1}, i)\) when \(1 \le i \le k_j - 1\), and the index \((2)\) otherwise. The run \(k_{j+1}, \dots, k_{j+l-1}\) is empty when \(l = 1\).

MetaMathlibExt.CyclicSumFormula.leftIndex · 19 lines 
noncomputable def leftIndex (k : List ℕ) (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (j : Fin k.length) (i : ℕ) : MultipleZeta.Index :=
  if hmem : i ∈ Finset.Icc 1 (k.get j - 1) then
    toIndex ((k.get j - i + 1) :: ((k.rotate j.1).tail ++ [i])) (by
      have hi1 : 1 ≤ i := (Finset.mem_Icc.mp hmem).1
      intro x hx
      rw [List.mem_cons] at hx
      rcases hx with rfl | hx
      · omega
      · rw [List.mem_append] at hx
        rcases hx with hx | hx
        · have hxR : x ∈ k.rotate j.1 := List.mem_of_mem_tail hx
          rw [List.mem_rotate] at hxR
          have h1 := hk_pos x hxR
          omega
        · rw [List.mem_singleton] at hx
          omega)
  else
    toIndex [2] (fun x hx => by rw [List.mem_singleton] at hx; omega)
Uses 2 · Used by 3
Statement usesThe index of a list of positive integers · Multiple-zeta index
Used byCyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Left-hand indices of the cyclic sum formula are admissible or empty

DefinitionRight-hand indices of the cyclic sum formula#✓fully proved

Let \(k = (k_1, \dots, k_l)\) be a list of positive integers, with subscripts read modulo \(l\). For \(1 \le j \le l\), the right-hand index of \(k\) at \(j\) is the index \((k_j + 1, k_{j+1}, \dots, k_{j+l-1})\), where the run \(k_{j+1}, \dots, k_{j+l-1}\) is empty when \(l = 1\).

noncomputable def rightIndex (k : List ℕ) (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (j : Fin k.length) : MultipleZeta.Index :=
  toIndex ((k.get j + 1) :: (k.rotate j.1).tail) (by
    intro x hx
    rw [List.mem_cons] at hx
    rcases hx with rfl | hx
    · omega
    · have hxR : x ∈ k.rotate j.1 := List.mem_of_mem_tail hx
      rw [List.mem_rotate] at hxR
      have h1 := hk_pos x hxR
      omega)
Uses 2 · Used by 3
Statement usesThe index of a list of positive integers · Multiple-zeta index
Used byCyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Right-hand indices of the cyclic sum formula are admissible or empty

TheoremLeft-hand indices of the cyclic sum formula are admissible or empty#✓fully proved

For every list \(k = (k_1, \dots, k_l)\) of positive integers, every \(1 \le j \le l\) and every natural number \(i\), the left-hand index of the cyclic sum formula of \(k\) at \((j, i)\) is admissible or empty.

theorem leftIndex_isAdmissibleOrEmpty (k : List ℕ) (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (j : Fin k.length) (i : ℕ) :
    (leftIndex k hk_pos j i).IsAdmissibleOrEmpty
Uses 9 · Used by 2
Statement usesLeft-hand indices of the cyclic sum formula · Admissible or empty index
Proof usesThe index of a list of positive integers · Multiple-zeta index · Admissible index · Depth of an index · Entries of an index · Admissibility of an index via its entries · Admissible list
Used byCyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices

TheoremRight-hand indices of the cyclic sum formula are admissible or empty#✓fully proved

For every list \(k = (k_1, \dots, k_l)\) of positive integers and every \(1 \le j \le l\), the right-hand index of the cyclic sum formula of \(k\) at \(j\) is admissible or empty.

theorem rightIndex_isAdmissibleOrEmpty (k : List ℕ) (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (j : Fin k.length) :
    (rightIndex k hk_pos j).IsAdmissibleOrEmpty
Uses 8 · Used by 2
Statement usesRight-hand indices of the cyclic sum formula · Admissible or empty index
Proof usesThe index of a list of positive integers · Admissible index · Depth of an index · Entries of an index · Admissibility of an index via its entries · Admissible list
Used byCyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices

TheoremCyclic sum formula for strict multiple zeta values of indices#✓fully proved

Let \(k = (k_1, \dots, k_l)\) be a nonempty list of positive integers, not all equal to \(1\), with subscripts read modulo \(l\), and write \(\zeta\) for the strict multiple zeta value. For \(1 \le j \le l\) and \(1 \le i \le k_j - 1\) the left-hand index of the cyclic sum formula of \(k\) at \((j, i)\) is \((k_j - i + 1, k_{j+1}, \dots, k_{j+l-1}, i)\), and its right-hand index at \(j\) is \((k_j + 1, k_{j+1}, \dots, k_{j+l-1})\); the run \(k_{j+1}, \dots, k_{j+l-1}\) is empty when \(l = 1\). Then

\[ \sum_{j=1}^{l} \sum_{i=1}^{k_j - 1} \zeta(k_j - i + 1, k_{j+1}, \dots, k_{j+l-1}, i) = \sum_{j=1}^{l} \zeta(k_j + 1, k_{j+1}, \dots, k_{j+l-1}), \]

where the inner sum is empty when \(k_j = 1\).

theorem hoffman_ohno_cyclic_sum_formula_strict
    (k : List ℕ)
    (hk_nonempty : k ≠ [])
    (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (hk_not_all_one : ∃ n ∈ k, n ≠ 1) :
    ∑ j : Fin k.length,
        ∑ i ∈ Finset.Icc 1 (k.get j - 1),
          MultipleZeta.strictValue (CyclicSumFormula.leftIndex k hk_pos j i)
            (CyclicSumFormula.leftIndex_isAdmissibleOrEmpty k hk_pos j i) =
      ∑ j : Fin k.length,
        MultipleZeta.strictValue (CyclicSumFormula.rightIndex k hk_pos j)
          (CyclicSumFormula.rightIndex_isAdmissibleOrEmpty k hk_pos j)
Uses 14 · Used by 1
Statement usesLeft-hand indices of the cyclic sum formula · Left-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula · Right-hand indices of the cyclic sum formula are admissible or empty · Multiple zeta value
Proof usesThe index of a list of positive integers · Multiple-zeta index · Admissible index · Admissible or empty index · Depth of an index · Entry of a multiple-zeta index · Strictly decreasing tuples · Multiple zeta summand · Convergence of multiple zeta series
Used byCyclic sum formula (Hoffman–Ohno)

TheoremCyclic sum formula (Hoffman–Ohno)#✓fully proved

For a finite list \((n_1, \dots, n_r)\) of natural numbers let \(\zeta(n_1, \dots, n_r)\) be the sum of \((m_1^{n_1} \cdots m_r^{n_r})^{-1}\) over all integers \(m_1 > m_2 > \cdots > m_r > 0\), taken to be \(0\) when this family is not summable. Let \(k = (k_1, \dots, k_l)\) be a nonempty list of positive integers, not all equal to \(1\), with subscripts read modulo \(l\). Then

\[ \sum_{j=1}^{l} \sum_{i=1}^{k_j - 1} \zeta(k_j - i + 1, k_{j+1}, \dots, k_{j+l-1}, i) = \sum_{j=1}^{l} \zeta(k_j + 1, k_{j+1}, \dots, k_{j+l-1}), \]

where the inner sum is empty when \(k_j = 1\) and the run \(k_{j+1}, \dots, k_{j+l-1}\) is empty when \(l = 1\).

theorem hoffman_ohno_cyclic_sum_formula
    (k : List ℕ)
    (hk_nonempty : k ≠ [])
    (hk_pos : ∀ n ∈ k, 1 ≤ n)
    (hk_not_all_one : ∃ n ∈ k, n ≠ 1) :
    ∑ j : Fin k.length,
        ∑ i ∈ Finset.Icc 1 (k.get j - 1),
          multipleZetaValue
            ((k.get j - i + 1) :: ((k.rotate j.1).tail ++ [i])) =
      ∑ j : Fin k.length,
        multipleZetaValue ((k.get j + 1) :: (k.rotate j.1).tail)
Sources
  • Shingo Saito, Tatsushi Tanaka, and Noriko Wakabayashi, "Combinatorial Remarks on the Cyclic Sum Formula for Multiple Zeta Values," Journal of Integer Sequences 14 (2011), Article 11.2.4, Theorem thm:CSF ("Cyclic sum formula," first proved by Hoffman-Ohno), lines 242–248; index set check{I}^1 at lines 150–166, https://cs.uwaterloo.ca/journals/JIS/VOL14/Saito/saito22.tex.
Uses 13
Proof usesLeft-hand indices of the cyclic sum formula · Left-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula · Right-hand indices of the cyclic sum formula are admissible or empty · The index of a list of positive integers · Multiple-zeta index · Admissible or empty index · Depth of an index · Entry of a multiple-zeta index · Strictly decreasing tuples · Multiple zeta summand · Multiple zeta value · Cyclic sum formula for strict multiple zeta values of indices

TheoremCyclic sum formula for multiple zeta-star values#✓fully proved

Let \(l \ge 1\) and let \(k_0, \dots, k_{l-1}\) be positive integers, not all equal to \(1\), with subscripts read modulo \(l\), and put \(K = k_0 + \cdots + k_{l-1}\). Write \(\zeta^\star\) for the multiple zeta-star value and \(\zeta\) for the strict multiple zeta value. Suppose that for each \(0 \le j \le l - 1\) and each natural number \(i\) an index \(\mathbf{c}_{j,i}\) is given that is admissible or empty, and that for \(1 \le i \le k_j - 1\) its entries are \((k_j - i + 1, k_{j+1}, \dots, k_{j+l-1}, i)\), the run \(k_{j+1}, \dots, k_{j+l-1}\) being empty when \(l = 1\). Let \(\mathbf{t}\) be an index, admissible or empty, whose only entry is \(K + 1\). Then

\[ \sum_{j=0}^{l-1} \sum_{i=1}^{k_j - 1} \zeta^\star(\mathbf{c}_{j,i}) = K \, \zeta(\mathbf{t}). \]
MetaMathlibExt.cyclic_sum_formula_multiple_zeta_star_values · 19 lines 
theorem cyclic_sum_formula_multiple_zeta_star_values
    (l : ℕ) (hl : 0 < l)
    (k : Fin l → ℕ)
    (hk : ∀ j, 0 < k j)
    (hne : ∃ j, k j ≠ 1)
    (cyclicIndex : Fin l → ℕ → MultipleZeta.Index)
    (hcyclicEntries : ∀ j i, i ∈ Finset.Icc 1 (k j - 1) →
      (cyclicIndex j i).entries = List.ofFn (fun t : Fin (l + 1) =>
        if t.val = 0 then k j - i + 1
        else if t.val = l then i
        else k ⟨(j.val + t.val) % l, Nat.mod_lt _ hl⟩))
    (hcyclicAdmissible : ∀ j i, (cyclicIndex j i).IsAdmissibleOrEmpty)
    (totalIndex : MultipleZeta.Index)
    (htotalEntries : totalIndex.entries = [(∑ j : Fin l, k j) + 1])
    (htotalAdmissible : totalIndex.IsAdmissibleOrEmpty) :
    ∑ j : Fin l, ∑ i ∈ Finset.Icc 1 (k j - 1),
      MultipleZeta.starValue (cyclicIndex j i) (hcyclicAdmissible j i) =
      ((∑ j : Fin l, k j : ℕ) : ℝ) *
        MultipleZeta.strictValue totalIndex htotalAdmissible
Sources
Uses 11
Statement usesMultiple-zeta index · Admissible or empty index · Entries of an index · Multiple zeta-star value · Multiple zeta value
Proof usesDepth of an index · Entry of a multiple-zeta index · Strictly decreasing tuples · Weakly decreasing tuples · Multiple-zeta-star summand · Multiple zeta summand
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.