Reversing multiple-zeta summation conventions

DefinitionReversed index#✓fully proved

The reverse of an index \((k_0, \dots, k_{d-1})\) is the index \((k_{d-1}, \dots, k_0)\) with the same entries in the opposite order.

def Index.reverse (index : Index) : Index :=
  match index with
  | ⟨n, composition⟩ => ⟨n, composition.reverse⟩

Uses 1 · Used by 5

Statement usesMultiple-zeta index

Used byReversal of strictly increasing tuples · Reversal preserves each summand · Increasing values agree with strict values of the reverse · Increasing admissibility is admissibility of the reverse · Entries of the reversed index

AbbreviationStrictly increasing tuples#✓fully proved

For a natural number \(d\), a strictly increasing tuple of length \(d\) is a tuple \((m_0, \dots, m_{d-1})\) of positive natural numbers with \(m_0 < m_1 < \cdots < m_{d-1}\). These are the summation variables of the increasing multiple-zeta convention.

abbrev StrictIncreasingTuple (depth : ℕ) :=
  {m : Fin depth → PNat // StrictMono m}

Used by 5

Used byReversal of strictly increasing tuples · Summand of the increasing multiple-zeta series · Reversal preserves each summand · Multiple zeta value in the increasing convention · Increasing values agree with strict values of the reverse

DefinitionAdmissibility in the increasing convention#✓fully proved

An index \((k_0, \dots, k_{d-1})\) is admissible in the increasing convention when its list of entries read in reverse order, \((k_{d-1}, \dots, k_0)\), is admissible: it is nonempty, its first element \(k_{d-1}\) is at least two, and its other elements are positive. Since the entries of an index are positive, this says that the index is nonempty and its last entry is at least two.

This is the convention in arXiv:2304.08722 and arXiv:2608.10675.

def Index.IsIncreasingAdmissible (index : Index) : Prop :=
  MetaMathlibExt.MultipleZeta.IsAdmissible index.entries.reverse

Uses 3 · Used by 3

Statement usesMultiple-zeta index · Entries of an index · Admissible list

Used byMultiple zeta value in the increasing convention · Increasing values agree with strict values of the reverse · Increasing admissibility is admissibility of the reverse

TheoremIncreasing admissibility is admissibility of the reverse#✓fully proved

An index is admissible in the increasing convention (nonempty with last entry at least two) if and only if its reverse is admissible (nonempty with first entry at least two).

theorem Index.isIncreasingAdmissible_iff_reverse_isAdmissible (index : Index) :
    index.IsIncreasingAdmissible ↔ index.reverse.IsAdmissible

Uses 7 · Used by 1

Statement usesMultiple-zeta index · Admissible index · Admissibility in the increasing convention · Reversed index

Proof usesEntries of an index · Admissibility of an index via its entries · Admissible list

Used byIncreasing values agree with strict values of the reverse

TheoremEntries of the reversed index#✓fully proved

Let \(k = (k_0, \dots, k_{d-1})\) be an index of depth \(d\); its reverse also has depth \(d\). For every \(i < d\), the \(i\)-th entry of the reverse of \(k\) is \(k_{d-1-i}\).

theorem Index.reverse_entry (index : Index)
    (i : Fin index.reverse.depth) :
    index.reverse.entry i =
      index.entry (Fin.rev (Fin.castOrderIso index.reverse_depth i))

Uses 4 · Used by 1

Statement usesMultiple-zeta index · Depth of an index · Entry of a multiple-zeta index · Reversed index

Used byReversal preserves each summand

DefinitionSummand of the increasing multiple-zeta series#✓fully proved

Let \(k = (k_0, \dots, k_{d-1})\) be an index of depth \(d\). To a strictly increasing tuple \(m = (m_0, \dots, m_{d-1})\) of positive natural numbers it attaches the real number

\[\Bigl(\prod_{i=0}^{d-1} m_i^{k_i}\Bigr)^{-1}.\]

This is the convention in arXiv:2304.08722 and arXiv:2608.10675.

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

Uses 4 · Used by 3

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

Used byReversal preserves each summand · Multiple zeta value in the increasing convention · Increasing values agree with strict values of the reverse

DefinitionMultiple zeta value in the increasing convention#✓fully proved

Let \(k = (k_0, \dots, k_{d-1})\) be an index of depth \(d\) that is admissible in the increasing convention. Its value in the increasing convention is the real number

\[\sum_{0 < m_0 < \cdots < m_{d-1}} \prod_{i=0}^{d-1} m_i^{-k_i},\]

the unconditional sum over all strictly increasing tuples of positive natural numbers (taken to be \(0\) if the family is not summable).

This is the convention in arXiv:2304.08722 and arXiv:2608.10675.

@[nolint unusedArguments]
noncomputable def increasingValue (index : Index)
    (_h : index.IsIncreasingAdmissible) : ℝ :=
  ∑' m : StrictIncreasingTuple index.depth, increasingSummand index m

Uses 5 · Used by 1

Statement usesMultiple-zeta index · Admissibility in the increasing convention · Depth of an index · Strictly increasing tuples · Summand of the increasing multiple-zeta series

Used byIncreasing values agree with strict values of the reverse

DefinitionReversal of strictly increasing tuples#✓fully proved

Let \(k\) be an index of depth \(d\); its reverse also has depth \(d\). Sending a strictly increasing tuple \((m_0, \dots, m_{d-1})\) of positive natural numbers to the reversed tuple \((m_{d-1}, \dots, m_0)\) is a bijection from the strictly increasing tuples of length \(d\) onto the strictly decreasing tuples of length \(d\), whose inverse again reverses the order of the coordinates.

MetaMathlibExt.MultipleZeta.increasingEquivDecreasing · 25 lines

def increasingEquivDecreasing (index : Index) :
    StrictIncreasingTuple index.depth ≃
      StrictDecreasingTuple index.reverse.depth where
  toFun m :=
    ⟨fun i => m.1 (Fin.rev (Fin.castOrderIso index.reverse_depth i)), by
      intro i j hij
      have hcast :
          Fin.castOrderIso index.reverse_depth i <
            Fin.castOrderIso index.reverse_depth j := by
        simpa using hij
      exact m.2 (Fin.rev_lt_rev.mpr hcast)⟩
  invFun m :=
    ⟨fun i => m.1 (Fin.castOrderIso index.reverse_depth.symm (Fin.rev i)), by
      intro i j hij
      have hcast :
          Fin.castOrderIso index.reverse_depth.symm (Fin.rev j) <
            Fin.castOrderIso index.reverse_depth.symm (Fin.rev i) := by
        simpa using Fin.rev_lt_rev.mpr hij
      exact m.2 hcast⟩
  left_inv m := by
    ext i
    simp
  right_inv m := by
    ext i
    simp

Uses 5 · Used by 2

Statement usesMultiple-zeta index · Depth of an index · Reversed index · Strictly decreasing tuples · Strictly increasing tuples

Used byReversal preserves each summand · Increasing values agree with strict values of the reverse

TheoremReversal preserves each summand#✓fully proved

Let \(k = (k_0, \dots, k_{d-1})\) be an index of depth \(d\) and let \(m = (m_0, \dots, m_{d-1})\) be a strictly increasing tuple of positive natural numbers. Then the summand of the increasing multiple-zeta series of \(k\) at \(m\) equals the summand of the strict multiple-zeta series of the reversed index \((k_{d-1}, \dots, k_0)\) at the strictly decreasing tuple \((m_{d-1}, \dots, m_0)\).

theorem increasingSummand_eq_strictSummand_reverse (index : Index)
    (m : StrictIncreasingTuple index.depth) :
    increasingSummand index m =
      strictSummand index.reverse (increasingEquivDecreasing index m)

Uses 10 · Used by 1

Statement usesMultiple-zeta index · Depth of an index · Reversed index · Strictly decreasing tuples · Strictly increasing tuples · Reversal of strictly increasing tuples · Summand of the increasing multiple-zeta series · Multiple zeta summand

Proof usesEntry of a multiple-zeta index · Entries of the reversed index

Used byIncreasing values agree with strict values of the reverse

TheoremIncreasing values agree with strict values of the reverse#✓fully proved

Let \(k = (k_0, \dots, k_{d-1})\) be an index of depth \(d\) that is admissible in the increasing convention, so that its reverse \((k_{d-1}, \dots, k_0)\) is admissible. Then the value of \(k\) in the increasing convention equals the strict multiple zeta value of the reverse of \(k\):

\[\sum_{0 < m_0 < \cdots < m_{d-1}} \prod_{i=0}^{d-1} m_i^{-k_i} = \sum_{n_0 > \cdots > n_{d-1} > 0} \prod_{i=0}^{d-1} n_i^{-k_{d-1-i}},\]

where both sides are unconditional sums of real numbers (taken to be \(0\) for a non-summable family).

theorem increasingValue_eq_strictValue_reverse (index : Index)
    (h : index.IsIncreasingAdmissible) :
    increasingValue index h =
      strictValue index.reverse
        (Or.inl (index.isIncreasingAdmissible_iff_reverse_isAdmissible.mp h))

Uses 14

Statement usesMultiple-zeta index · Admissible index · Admissibility in the increasing convention · Depth of an index · Increasing admissibility is admissibility of the reverse · Reversed index · Multiple zeta value in the increasing convention · Multiple zeta value

Proof usesStrictly decreasing tuples · Strictly increasing tuples · Reversal of strictly increasing tuples · Summand of the increasing multiple-zeta series · Reversal preserves each summand · Multiple zeta summand

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.