Documentation

FormalConjectures.Paper.ZagierMZV

Zagier's Conjecture on Multiple Zeta Values #

References:

source
noncomputable def ZagierMZV.multiZeta :
List ℕ → ℝ

The multiple zeta value $\zeta(s_1, s_2, \ldots, s_k)$, defined as $$\zeta(s_1, \ldots, s_k) = \sum_{n_1 > n_2 > \cdots > n_k > 0} \frac{1}{n_1^{s_1} n_2^{s_2} \cdots n_k^{s_k}}.$$ The argument is a list of positive natural numbers. The value is well-defined (i.e. the series converges) when the first entry is at least 2, but we define it for all inputs. For the empty list, multiZeta [] = 1 (the empty product convention).

Equations
Instances For
    source
    noncomputable def ZagierMZV.multiZeta.aux :
    List ℕ → ℕ → ℝ

    Auxiliary function for multiZeta: computes the inner sum $\sum_{n_2 > \cdots > n_k > 0, n_2 < \text{bound}} \frac{1}{n_2^{s_2} \cdots n_k^{s_k}}$.

    Equations
    Instances For
      source
      def ZagierMZV.weight (s : List ℕ) :
      ℕ

      The weight of an MZV index $(s_1, \ldots, s_k)$ is $s_1 + \cdots + s_k$.

      Equations
      Instances For
        source
        def ZagierMZV.AdmissibleIndex :
        List ℕ → Prop

        An MZV index is admissible if it is either empty or if the first entry is at least 2 and all entries are positive. The empty list convention ensures $\mathcal{Z}_0 = \mathbb{Q}$.

        Equations
        Instances For
          source
          def ZagierMZV.mzvSetOfWeight (n : ℕ) :
          Set ℝ

          The set of all MZV values of weight $n$.

          Equations
          Instances For
            source
            noncomputable def ZagierMZV.mzvSpanOfWeight (n : ℕ) :
            Submodule ℚ ℝ

            The $\mathbb{Q}$-submodule of $\mathbb{R}$ spanned by all MZVs of weight $n$.

            Equations
            Instances For
              source
              def ZagierMZV.zagierDim :
              ℕ → ℕ

              The conjectured Zagier dimension sequence $d_n$, defined by $d_0 = 1$, $d_1 = 0$, $d_2 = 1$, and $d_n = d_{n-2} + d_{n-3}$ for $n \geq 3$.

              Equations
              Instances For
                source
                theorem ZagierMZV.zagier_conjecture :
                True ↔ ∀ (n : ℕ), Module.finrank ℚ ↥(mzvSpanOfWeight n) = zagierDim n

                Zagier's conjecture

                The $\mathbb{Q}$-dimension of the vector space spanned by all multiple zeta values of weight $n$ equals $d_n$, where $d_n$ is the Zagier dimension sequence satisfying $d_0 = 1$, $d_1 = 0$, $d_2 = 1$, and $d_n = d_{n-2} + d_{n-3}$ for $n \geq 3$.

                source
                theorem ZagierMZV.zagier_upper_bound (n : ℕ) :
                Module.finrank ℚ ↥(mzvSpanOfWeight n) ≤ zagierDim n

                Upper bound [Te02, DG05]

                The dimension of the $\mathbb{Q}$-vector space of MZVs of weight $n$ is at most $d_n$.

                source
                theorem ZagierMZV.zagierDim_first_values :
                [zagierDim 0, zagierDim 1, zagierDim 2, zagierDim 3, zagierDim 4, zagierDim 5, zagierDim 6, zagierDim 7, zagierDim 8, zagierDim 9] = [1, 0, 1, 1, 1, 2, 2, 3, 4, 5]

                The first few values of $d_n$ are $1, 0, 1, 1, 1, 2, 2, 3, 4, 5, 7, 9, \ldots$

                source
                theorem ZagierMZV.no_admissible_weight_one (s : List ℕ) (h : AdmissibleIndex s) :
                weight s ≠ 1

                There is no admissible index of weight 1 (since $s_1 \geq 2$ is required).

                source
                theorem ZagierMZV.dim_mzv_weight_zero :
                Module.finrank ℚ ↥(mzvSpanOfWeight 0) = 1

                $\mathcal{Z}_0 = \mathbb{Q}$, so $\dim_\mathbb{Q}(\mathcal{Z}_0) = 1$.

                source
                theorem ZagierMZV.dim_mzv_weight_one :
                Module.finrank ℚ ↥(mzvSpanOfWeight 1) = 0

                $\mathcal{Z}_1 = \emptyset$, so $\dim_\mathbb{Q}(\mathcal{Z}_1) = 0$.

                source
                theorem ZagierMZV.multiZeta_empty :
                multiZeta [] = 1
                source
                theorem ZagierMZV.multiZeta_two :
                multiZeta [2] = Real.pi ^ 2 / 6

                Euler's identity: $\zeta(2) = \pi^2/6$.

                source
                theorem ZagierMZV.multiZeta_four :
                multiZeta [4] = Real.pi ^ 4 / 90

                Euler's identity for $\zeta(4) = \pi^4/90$.