Multiple-zeta indices

DefinitionMultiple-zeta index#✓fully proved

An index is a finite sequence \((k_1, \ldots, k_r)\) of positive integers with \(r \ge 0\), so the empty sequence is allowed. It is represented as a natural number \(n\) together with a composition of \(n\), that is, a sequence of positive integers with sum \(n\).

def Index : Type :=
  Σ _n : Nat, Composition _n

Sources

• clause D1 (2608.10675:D01, 2307.09867:D01).

Used by 39

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 · Left-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula · The index of a list of positive integers · Hoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · The type of empty or admissible indices · Empty or admissible indices · Entries of an index as positive integers · Hoffman monomial of an index · Hoffman word of an index · Empty multiple-zeta index · Entry of a multiple-zeta index · Admissible or empty index · Repeated index · Multiple-zeta-star summand · Star and strict summands agree on strictly decreasing tuples · Multiple zeta-star value · Multiple zeta summand · Multiple zeta value · Depth of an index · Entries of an index · Height of an index · Admissible index · Admissibility of an index via its entries · Weight of an index · Reversal 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 · Admissibility in the increasing convention · Increasing admissibility is admissibility of the reverse · Reversed index · Entries of the reversed index · Convergence of multiple zeta series

DefinitionEntries of an index#✓fully proved

The entries of an index \((k_1, \ldots, k_r)\) form the list \([k_1, \ldots, k_r]\) of its terms, in order.

def Index.entries : Index → List Nat
  | ⟨_, c⟩ => c.blocks

Sources

• clause D2 (2608.10675:D01, 2307.09867:D01).

Uses 1 · Used by 9

Statement usesMultiple-zeta index

Used byCyclic sum formula for multiple zeta-star values · Left-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula are admissible or empty · Hoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Empty or admissible indices · Admissibility of an index via its entries · Admissibility in the increasing convention · Increasing admissibility is admissibility of the reverse

DefinitionWeight of an index#✓fully proved

The weight of an index \((k_1, \ldots, k_r)\) is the sum \(k_1 + \cdots + k_r\) of its entries.

def Index.weight : Index → Nat
  | ⟨n, _⟩ => n

Sources

• clause D3 (2307.09867:D01).

Uses 1

Statement usesMultiple-zeta index

DefinitionDepth of an index#✓fully proved

The depth of an index \((k_1, \ldots, k_r)\) is its number of entries \(r\).

def Index.depth : Index → Nat
  | ⟨_, c⟩ => Composition.length c

Sources

• clause D4 (2608.10675:D01, 2307.09867:D01).

Uses 1 · Used by 21

Statement usesMultiple-zeta 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 · Entry of a multiple-zeta index · Admissible or empty index · Repeated indices with entry at least two are admissible or empty · Multiple-zeta-star summand · Star and strict summands agree on strictly decreasing tuples · Multiple zeta-star value · Multiple-zeta-star value of the empty index · Multiple zeta summand · Multiple zeta value · Reversal 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 · Entries of the reversed index · Convergence of multiple zeta series

DefinitionHeight of an index#✓fully proved

The height of an index \((k_1, \ldots, k_r)\) is the number of positions \(i\) with \(1 \le i \le r\) and \(k_i \ge 2\).

def Index.height : Index → Nat
  | ⟨_, c⟩ => (c.blocks.filter (· ≥ 2)).length

Sources

• clause D5 (2307.09867:D01).

Uses 1

Statement usesMultiple-zeta index

DefinitionAdmissible index#✓fully proved

An index \((k_1, \ldots, k_r)\) is admissible when it is nonempty (\(r \ge 1\)) and its first entry satisfies \(k_1 \ge 2\).

def Index.IsAdmissible : Index → Prop
  | ⟨_, c⟩ =>
    match c.blocks with
    | [] => False
    | h :: _ => 2 ≤ h

Sources

• clause D6 (2307.09867:D01).

Uses 1 · Used by 11

Statement usesMultiple-zeta index

Used byCyclic 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 · Hoffman monomial basis of \(\mathfrak{H}^0\) · Empty or admissible indices · Admissible or empty index · Repeated indices with entry at least two are admissible or empty · Admissibility of an index via its entries · Increasing values agree with strict values of the reverse · Increasing admissibility is admissibility of the reverse · Convergence of multiple zeta series

DefinitionAdmissible list#✓fully proved

A list \([k_1, \ldots, k_r]\) of natural numbers is admissible when it is nonempty (\(r \ge 1\)), \(k_1 \ge 2\), and \(k_i > 0\) for every \(i\) with \(2 \le i \le r\).

This is the admissibility condition for multiple-zeta indices in decreasing summation order.

def IsAdmissible : List ℕ → Prop
  | [] => False
  | h :: t => 2 ≤ h ∧ ∀ x ∈ t, 0 < x

Sources

• 2307.09867:D01.

Used by 6

Used byLeft-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula are admissible or empty · Hoffman monomial basis of \(\mathfrak{H}^0\) · Admissibility of an index via its entries · Admissibility in the increasing convention · Increasing admissibility is admissibility of the reverse

TheoremAdmissibility of an index via its entries#✓fully proved

An index is admissible if and only if the list of its entries is an admissible list.

theorem Index.isAdmissible_iff (index : Index) :
    index.IsAdmissible ↔ MetaMathlibExt.MultipleZeta.IsAdmissible index.entries

Uses 4 · Used by 4

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

Used byLeft-hand indices of the cyclic sum formula are admissible or empty · Right-hand indices of the cyclic sum formula are admissible or empty · Hoffman monomial basis of \(\mathfrak{H}^0\) · Increasing admissibility is admissibility of the reverse

DefinitionHoffman block#✓fully proved

For a positive integer \(k\), the Hoffman block \(z_k = x^{k-1} y\) is the word in the free monoid on two letters \(x\) and \(y\) consisting of \(k - 1\) copies of \(x\) followed by one \(y\).

The free monoid is taken on the booleans, with false standing for \(x\) and true for \(y\).

def hoffmanBlock (k : PNat) : FreeMonoid Bool :=
  FreeMonoid.ofList (List.replicate (k.val - 1) false ++ [true])

Sources

• 2307.09867:D05.

Used by 4

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Hoffman word of a list of positive integers · Hoffman block as a list

TheoremHoffman block as a list#✓fully proved

For every positive integer \(k\), the list of letters of the Hoffman block \(z_k\) consists of \(k - 1\) copies of \(x\) (false) followed by one \(y\) (true).

@[simp]
theorem toList_hoffmanBlock (k : PNat) :
    FreeMonoid.toList (hoffmanBlock k) =
      List.replicate (k.val - 1) false ++ [true]

Uses 1 · Used by 2

Statement usesHoffman block

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\)

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.