Multiple-zeta and multiple-zeta-star series

DefinitionEmpty multiple-zeta index#✓fully proved

The empty multiple-zeta index, which has no entries and weight zero.

def Index.empty : Index :=
  ⟨0, ⟨[], by simp, by simp⟩⟩

Sources

• arXiv:2307.09867, empty-index convention.

Uses 1 · Used by 1

Statement usesMultiple-zeta index

Used byMultiple-zeta-star value of the empty index

DefinitionEntry of a multiple-zeta index#✓fully proved

For a multiple-zeta index \(k = (k_0, \dots, k_{d-1})\) of depth \(d\) and \(0 \le i < d\), the entry of \(k\) at \(i\) is the positive natural number \(k_i\).

def Index.entry : (index : Index) → Fin index.depth → PNat
  | ⟨_, composition⟩ => fun i =>
    ⟨composition.blocksFun i, composition.blocks_pos (composition.blocksFun_mem_blocks i)⟩

Uses 2 · Used by 10

Statement usesMultiple-zeta index · Depth of an index

Used byCyclic sum formula for multiple zeta-star values · Cyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Multiple-zeta-star summand · Multiple-zeta-star value of the empty index · Multiple zeta summand · Summand of the increasing multiple-zeta series · Reversal preserves each summand · Entries of the reversed index · Convergence of multiple zeta series

AbbreviationStrictly decreasing tuples#✓fully proved

For a natural number \(r\), a strictly decreasing \(r\)-tuple is a tuple \((m_0, \dots, m_{r-1})\) of positive integers with \(m_0 > m_1 > \dots > m_{r-1}\).

abbrev StrictDecreasingTuple (depth : ℕ) :=
  {m : Fin depth → PNat // StrictAnti m}

Sources

• arXiv:2307.09867, lines 60–63, and arXiv:2309.07569, lines 76–80.

Used by 13

Used byCyclic sum formula for multiple zeta-star values · Cyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Strictly nested sums of reciprocal odd squares · Empty strictly decreasing tuple · Star and strict summands agree on strictly decreasing tuples · Multiple zeta summand · Multiple zeta value · Strictly decreasing tuples as weakly decreasing tuples · Reversal of strictly increasing tuples · Reversal preserves each summand · Increasing values agree with strict values of the reverse · Convergence of multiple zeta series

DefinitionEmpty strictly decreasing tuple#✓fully proved

The unique strictly decreasing tuple of positive natural numbers of length zero, namely the empty tuple.

def StrictDecreasingTuple.empty : StrictDecreasingTuple 0 :=
  ⟨fun i => Fin.elim0 i, fun i => Fin.elim0 i⟩

Uses 1

Statement usesStrictly decreasing tuples

DefinitionMultiple zeta summand#✓fully proved

Let \(\mathbf{k} = (k_0, \dots, k_{r-1})\) be an index of depth \(r\) and let \((m_0, \dots, m_{r-1})\) be a strictly decreasing \(r\)-tuple of positive integers. The summand attached to \(\mathbf{k}\) and this tuple is the real number \(\left(\prod_{i=0}^{r-1} m_i^{k_i}\right)^{-1}\).

noncomputable def strictSummand (index : Index)
    (m : StrictDecreasingTuple index.depth) : ℝ :=
  (∏ i : Fin index.depth, ((m.1 i : ℕ) : ℝ) ^ (index.entry i : ℕ))⁻¹

Sources

• arXiv:2307.09867, lines 60–63, and arXiv:2309.07569, lines 76–80.

Uses 4 · Used by 8

Statement usesMultiple-zeta index · Depth of an index · Entry of a multiple-zeta index · Strictly decreasing tuples

Used byCyclic sum formula for multiple zeta-star values · Cyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Star and strict summands agree on strictly decreasing tuples · Multiple zeta value · Reversal preserves each summand · Increasing values agree with strict values of the reverse · Convergence of multiple zeta series

DefinitionAdmissible or empty index#✓fully proved

A multiple-zeta index is admissible or empty when it is admissible (nonempty with first entry at least two) or has depth zero, that is, has no entries.

The strict multiple-zeta value and the multiple-zeta-star value are defined on these indices.

def Index.IsAdmissibleOrEmpty (index : Index) : Prop :=
  index.IsAdmissible ∨ index.depth = 0

Uses 3 · Used by 10

Statement usesMultiple-zeta index · Admissible index · Depth of an index

Used byCyclic sum formula for multiple zeta-star values · Cyclic 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 · Right-hand indices of the cyclic sum formula are admissible or empty · Nested sums of reciprocal squares · Repeated indices with entry at least two are admissible or empty · Multiple zeta-star value · Multiple-zeta-star value of the empty index · Multiple zeta value

DefinitionMultiple zeta value#✓fully proved

Let \(\mathbf{k} = (k_0, \dots, k_{r-1})\) be an index of depth \(r\) that is admissible (\(r \ge 1\) and \(k_0 \ge 2\)) or empty. Its multiple zeta value is the real number

\[\zeta(\mathbf{k}) = \sum_{m_0 > m_1 > \dots > m_{r-1} \ge 1} \prod_{i=0}^{r-1} m_i^{-k_i}\]

where the sum runs over all strictly decreasing \(r\)-tuples \((m_0, \dots, m_{r-1})\) of positive integers. The sum is unconditional, with value \(0\) by convention when the family is not summable.

@[nolint unusedArguments]
noncomputable def strictValue (index : Index) (_h : index.IsAdmissibleOrEmpty) : ℝ :=
  ∑' m : StrictDecreasingTuple index.depth, strictSummand index m

Sources

• arXiv:2307.09867, lines 60–63, and arXiv:2309.07569, lines 76–80.

Uses 5 · Used by 4

Statement usesMultiple-zeta index · Admissible or empty index · Depth of an index · Strictly decreasing tuples · Multiple zeta summand

Used byCyclic sum formula for multiple zeta-star values · Cyclic sum formula (Hoffman–Ohno) · Cyclic sum formula for strict multiple zeta values of indices · Increasing values agree with strict values of the reverse

AbbreviationWeakly decreasing tuples#✓fully proved

For a natural number \(r\), a weakly decreasing \(r\)-tuple is a tuple \((m_0, \dots, m_{r-1})\) of positive integers with \(m_0 \ge m_1 \ge \dots \ge m_{r-1}\).

abbrev WeaklyDecreasingTuple (depth : ℕ) :=
  {m : Fin depth → PNat // Antitone m}

Sources

• arXiv:2307.09867, lines 61–65, and arXiv:2309.07569v2, lines 84–87.

Used by 7

Used byCyclic sum formula for multiple zeta-star values · Nested sums of reciprocal odd squares · Empty weakly decreasing tuple · Multiple-zeta-star summand · Multiple zeta-star value · Multiple-zeta-star value of the empty index · Strictly decreasing tuples as weakly decreasing tuples

DefinitionEmpty weakly decreasing tuple#✓fully proved

The unique weakly decreasing tuple of positive natural numbers of length zero, namely the empty tuple.

def WeaklyDecreasingTuple.empty : WeaklyDecreasingTuple 0 :=
  ⟨fun i => Fin.elim0 i, fun i => Fin.elim0 i⟩

Uses 1 · Used by 1

Statement usesWeakly decreasing tuples

Used byMultiple-zeta-star value of the empty index

DefinitionStrictly decreasing tuples as weakly decreasing tuples#✓fully proved

For a natural number \(r\), every strictly decreasing \(r\)-tuple \((m_0, \dots, m_{r-1})\) of positive integers is weakly decreasing; this map sends it to the same tuple, regarded as a weakly decreasing \(r\)-tuple.

def StrictDecreasingTuple.toWeaklyDecreasing {depth : ℕ}
    (m : StrictDecreasingTuple depth) : WeaklyDecreasingTuple depth :=
  ⟨m.1, m.2.antitone⟩

Uses 2 · Used by 1

Statement usesStrictly decreasing tuples · Weakly decreasing tuples

Used byStar and strict summands agree on strictly decreasing tuples

DefinitionMultiple-zeta-star summand#✓fully proved

For a multiple-zeta index \(k = (k_0, \dots, k_{d-1})\) of depth \(d\) and a weakly decreasing tuple \(m = (m_0, \dots, m_{d-1})\) of positive natural numbers, the star summand of \(k\) at \(m\) is the real number \(\left(\prod_{i\lt d} m_i^{k_i}\right)^{-1}\).

noncomputable def starSummand (index : Index)
    (m : WeaklyDecreasingTuple index.depth) : ℝ :=
  (∏ i : Fin index.depth, ((m.1 i : ℕ) : ℝ) ^ (index.entry i : ℕ))⁻¹

Sources

• arXiv:2307.09867, lines 61–65, and arXiv:2309.07569v2, lines 84–87.

Uses 4 · Used by 4

Statement usesMultiple-zeta index · Depth of an index · Entry of a multiple-zeta index · Weakly decreasing tuples

Used byCyclic sum formula for multiple zeta-star values · Star and strict summands agree on strictly decreasing tuples · Multiple zeta-star value · Multiple-zeta-star value of the empty index

TheoremStar and strict summands agree on strictly decreasing tuples#✓fully proved

For a multiple-zeta index \(k\) of depth \(d\) and a strictly decreasing tuple \(m\) of \(d\) positive natural numbers, the star summand of \(k\) at \(m\), with \(m\) regarded as a weakly decreasing tuple, equals the strict summand of \(k\) at \(m\).

@[simp]
theorem starSummand_toWeaklyDecreasing
    (index : Index) (m : StrictDecreasingTuple index.depth) :
    starSummand index m.toWeaklyDecreasing = strictSummand index m

Uses 6

Statement usesMultiple-zeta index · Depth of an index · Strictly decreasing tuples · Strictly decreasing tuples as weakly decreasing tuples · Multiple-zeta-star summand · Multiple zeta summand

DefinitionMultiple zeta-star value#✓fully proved

Let \(\mathbf{k} = (k_0, \dots, k_{r-1})\) be an index of depth \(r\) that is admissible (\(r \ge 1\) and \(k_0 \ge 2\)) or empty. Its multiple zeta-star value is the real number

\[\zeta^\star(\mathbf{k}) = \sum_{m_0 \ge \dots \ge m_{r-1} \ge 1} \prod_{i=0}^{r-1} m_i^{-k_i}\]

where the sum runs over all weakly decreasing \(r\)-tuples \((m_0, \dots, m_{r-1})\) of positive integers. The sum is unconditional, with value \(0\) by convention when the family is not summable.

@[nolint unusedArguments]
noncomputable def starValue (index : Index) (_h : index.IsAdmissibleOrEmpty) : ℝ :=
  ∑' m : WeaklyDecreasingTuple index.depth, starSummand index m

Sources

• arXiv:2307.09867, lines 61–65, and arXiv:2309.07569v2, lines 84–87.

Uses 5 · Used by 3

Statement usesMultiple-zeta index · Admissible or empty index · Depth of an index · Weakly decreasing tuples · Multiple-zeta-star summand

Used byCyclic sum formula for multiple zeta-star values · Nested sums of reciprocal squares · Multiple-zeta-star value of the empty index

TheoremMultiple-zeta-star value of the empty index#✓fully proved

The multiple-zeta-star value of the empty index is \(1\).

@[simp]
theorem starValue_empty (h : Index.empty.IsAdmissibleOrEmpty) :
    starValue Index.empty h = 1

Sources

• arXiv:2307.09867, lines 166–167.

Uses 8

Statement usesAdmissible or empty index · Empty multiple-zeta index · Multiple zeta-star value

Proof usesDepth of an index · Entry of a multiple-zeta index · Weakly decreasing tuples · Empty weakly decreasing tuple · Multiple-zeta-star summand

DefinitionRepeated index#✓fully proved

For a natural number \(k\) and a positive natural number \(e\), the index \(\{e\}^k = (e, \dots, e)\) consisting of \(k\) entries all equal to \(e\), so of weight \(ke\).

For \(e = 2\) its multiple-zeta-star value is \(\zeta^\star(\{2\}^k)\).

def Index.replicate (k : ℕ) (e : PNat) : Index :=
  ⟨k * e, ⟨List.replicate k (e : ℕ), fun h => by
      rw [List.eq_of_mem_replicate h]
      exact e.pos, by simp⟩⟩

Sources

• Serge Iovleff, About Some Nested Sums of Reciprocal Squared Numbers, INTEGERS 26 (2026), Article A114, Section 1 (notation ζ*({2}^k) and ζ({2}^k)).

Uses 1 · Used by 2

Statement usesMultiple-zeta index

Used byNested sums of reciprocal squares · Repeated indices with entry at least two are admissible or empty

TheoremRepeated indices with entry at least two are admissible or empty#✓fully proved

For every natural number \(k\) and every positive natural number \(e \ge 2\), the index \(\{e\}^k\) consisting of \(k\) entries all equal to \(e\) is admissible or empty.

theorem Index.replicate_isAdmissibleOrEmpty (k : ℕ) {e : PNat} (he : 2 ≤ (e : ℕ)) :
    (Index.replicate k e).IsAdmissibleOrEmpty

Sources

• Iovleff, INTEGERS 26 (2026), Article A114, Section 1 (ζ*({2}^k)).

Uses 4 · Used by 1

Statement usesAdmissible or empty index · Repeated index

Proof usesAdmissible index · Depth of an index

Used byNested sums of reciprocal squares

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.