Zagier's matrix and Bernoulli numbers

DefinitionZagier's matrix#✓fully proved

For a natural number \(K\), Zagier's matrix \(A_K\) is the rational matrix with rows and columns indexed by \(1 \le i, j \le K - 1\) (empty when \(K \le 1\)) whose \((i, j)\) entry is

\[(A_K)_{ij} = \binom{2K - 2j}{2i - 1} + \binom{2K - 2j}{2K - 2i},\]

where \(\binom{m}{k} = 0\) for \(k > m\).

public def zagierMatrix (K : ℕ) : Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ := fun i j =>
  (Nat.choose (2 * K - 2 * (j.val + 1)) (2 * (i.val + 1) - 1) : ℚ)
    + (Nat.choose (2 * K - 2 * (j.val + 1)) (2 * K - 2 * (i.val + 1)) : ℚ)
Used by 3
Used byLeft inverse of Zagier's matrix · Zagier's matrix conjecture · Right inverse of Zagier's matrix

DefinitionFirst Bernoulli formula for the inverse of Zagier's matrix#✓fully proved

For a natural number \(K\), \(P_K\) is the rational matrix with rows and columns indexed by \(1 \le i, j \le K - 1\) (empty when \(K \le 1\)) whose \((i, j)\) entry is

\[(P_K)_{ij} = \frac{2}{2i-1} \sum_{n=0}^{2K-2i} \binom{2j-1}{2K-2i-n+1} \binom{n+2i-2}{n} B_n,\]

where \(B_n\) is the \(n\)-th Bernoulli number with \(B_1 = -\frac{1}{2}\) and \(\binom{m}{k} = 0\) for \(k > m\).

public def zagierInverseP (K : ℕ) : Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ := fun i j =>
  (2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1)
    * ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
      (Nat.choose (2 * (j.val + 1) - 1) (2 * K - 2 * (i.val + 1) - n + 1) : ℚ)
        * (Nat.choose (n + 2 * (i.val + 1) - 2) n : ℚ) * bernoulli n
Used by 4
Used byThe two Bernoulli formulas for the inverse of Zagier's matrix agree · Left inverse of Zagier's matrix · Zagier's matrix conjecture · Right inverse of Zagier's matrix

DefinitionSecond Bernoulli formula for the inverse of Zagier's matrix#✓fully proved

For a natural number \(K\), \(Q_K\) is the rational matrix with rows and columns indexed by \(1 \le i, j \le K - 1\) (empty when \(K \le 1\)) whose \((i, j)\) entry is

\[(Q_K)_{ij} = -\frac{2}{2i-1} \sum_{n=0}^{2K-2i} \binom{2K-2j}{2K-2i-n+1} \binom{n+2i-2}{n} B_n,\]

where \(B_n\) is the \(n\)-th Bernoulli number with \(B_1 = -\frac{1}{2}\) and \(\binom{m}{k} = 0\) for \(k > m\).

public def zagierInverseQ (K : ℕ) : Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ := fun i j =>
  (-2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1)
    * ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
      (Nat.choose (2 * K - 2 * (j.val + 1)) (2 * K - 2 * (i.val + 1) - n + 1) : ℚ)
        * (Nat.choose (n + 2 * (i.val + 1) - 2) n : ℚ) * bernoulli n
Used by 3
Used byThe two Bernoulli formulas for the inverse of Zagier's matrix agree · Left inverse of Zagier's matrix · Zagier's matrix conjecture

LemmaThe two Bernoulli formulas for the inverse of Zagier's matrix agree#✓fully proved

For every natural number \(K\), the matrices \(P_K\) and \(Q_K\) given by the first and second Bernoulli formulas for the inverse of Zagier's matrix are equal: \(P_K = Q_K\).

public lemma zagierInverseP_eq_zagierInverseQ (K : ℕ) :
    zagierInverseP K = zagierInverseQ K
Uses 2 · Used by 2
Statement usesFirst Bernoulli formula for the inverse of Zagier's matrix · Second Bernoulli formula for the inverse of Zagier's matrix
Used byLeft inverse of Zagier's matrix · Zagier's matrix conjecture

LemmaLeft inverse of Zagier's matrix#✓fully proved

For every natural number \(K\), the matrix \(P_K\) given by the first Bernoulli formula is a left inverse of Zagier's matrix \(A_K\): \(P_K A_K = I\), where \(I\) is the \((K - 1) \times (K - 1)\) identity matrix.

public lemma zagierInverseP_mul_zagierMatrix (K : ℕ) :
    zagierInverseP K * zagierMatrix K = 1
Uses 4 · Used by 2
Statement usesFirst Bernoulli formula for the inverse of Zagier's matrix · Zagier's matrix
Proof usesThe two Bernoulli formulas for the inverse of Zagier's matrix agree · Second Bernoulli formula for the inverse of Zagier's matrix
Used byZagier's matrix conjecture · Right inverse of Zagier's matrix

LemmaRight inverse of Zagier's matrix#✓fully proved

For every natural number \(K\), the matrix \(P_K\) given by the first Bernoulli formula is a right inverse of Zagier's matrix \(A_K\): \(A_K P_K = I\), where \(I\) is the \((K - 1) \times (K - 1)\) identity matrix.

public lemma zagierMatrix_mul_zagierInverseP (K : ℕ) :
    zagierMatrix K * zagierInverseP K = 1
Uses 3 · Used by 1
Statement usesFirst Bernoulli formula for the inverse of Zagier's matrix · Zagier's matrix
Proof usesLeft inverse of Zagier's matrix
Used byZagier's matrix conjecture

TheoremZagier's matrix conjecture#✓fully proved

Let \(K\) be a natural number, let \(B_n\) be the \(n\)-th Bernoulli number with \(B_1 = -\frac{1}{2}\), and let \(\binom{m}{k} = 0\) for \(k > m\). Let \(A\), \(P\) and \(Q\) be the \((K - 1) \times (K - 1)\) rational matrices, with rows and columns indexed by \(1 \le i, j \le K - 1\), whose entries are

\[A_{ij} = \binom{2K - 2j}{2i - 1} + \binom{2K - 2j}{2K - 2i},\]
\[P_{ij} = \frac{2}{2i-1} \sum_{n=0}^{2K-2i} \binom{2j-1}{2K-2i-n+1} \binom{n+2i-2}{n} B_n,\]
\[Q_{ij} = -\frac{2}{2i-1} \sum_{n=0}^{2K-2i} \binom{2K-2j}{2K-2i-n+1} \binom{n+2i-2}{n} B_n.\]

Then \(P = Q\), \(AP = I\) and \(PA = I\), where \(I\) is the identity matrix; that is, the two Bernoulli formulas agree and give the two-sided inverse of \(A\).

The source assumes \(K \ge 2\). The assumption is not needed: for \(K \le 1\) the matrices are empty.

MetaMathlibExt.zagier_matrix_inverse · 40 lines 
public theorem zagier_matrix_inverse (K : ℕ) :
    (Matrix.of (fun i j : Fin (K - 1) =>
        (2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1) *
          ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
            (↑(Nat.choose (2 * (j.val + 1) - 1)
              (2 * K - 2 * (i.val + 1) - n + 1)) : ℚ) *
              (↑(Nat.choose (n + 2 * (i.val + 1) - 2) n) : ℚ) * bernoulli n) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    =
    (Matrix.of (fun i j : Fin (K - 1) =>
        (-2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1) *
          ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
            (↑(Nat.choose (2 * K - 2 * (j.val + 1))
              (2 * K - 2 * (i.val + 1) - n + 1)) : ℚ) *
              (↑(Nat.choose (n + 2 * (i.val + 1) - 2) n) : ℚ) * bernoulli n) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    ∧ (Matrix.of (fun i j : Fin (K - 1) =>
        (↑(Nat.choose (2 * K - 2 * (j.val + 1)) (2 * (i.val + 1) - 1)) : ℚ) +
          (↑(Nat.choose (2 * K - 2 * (j.val + 1)) (2 * K - 2 * (i.val + 1))) : ℚ)) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    * (Matrix.of (fun i j : Fin (K - 1) =>
        (2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1) *
          ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
            (↑(Nat.choose (2 * (j.val + 1) - 1)
              (2 * K - 2 * (i.val + 1) - n + 1)) : ℚ) *
              (↑(Nat.choose (n + 2 * (i.val + 1) - 2) n) : ℚ) * bernoulli n) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    = 1
    ∧ (Matrix.of (fun i j : Fin (K - 1) =>
        (2 : ℚ) / (2 * (↑(i.val + 1) : ℚ) - 1) *
          ∑ n ∈ Finset.range (2 * K - 2 * (i.val + 1) + 1),
            (↑(Nat.choose (2 * (j.val + 1) - 1)
              (2 * K - 2 * (i.val + 1) - n + 1)) : ℚ) *
              (↑(Nat.choose (n + 2 * (i.val + 1) - 2) n) : ℚ) * bernoulli n) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    * (Matrix.of (fun i j : Fin (K - 1) =>
        (↑(Nat.choose (2 * K - 2 * (j.val + 1)) (2 * (i.val + 1) - 1)) : ℚ) +
          (↑(Nat.choose (2 * K - 2 * (j.val + 1)) (2 * K - 2 * (i.val + 1))) : ℚ)) :
      Matrix (Fin (K - 1)) (Fin (K - 1)) ℚ)
    = 1
Sources
  • Yawen Ma and Lee-Peng Teo, "Another Proof of Zagier's Matrix Conjecture," Journal of Integer Sequences 25 (2022), Article 22.6.4, Theorem [Zagier's conjecture], equations (eq12) and (eq13), lines 279–285, https://cs.uwaterloo.ca/journals/JIS/VOL25/Teo/teo4.tex
Uses 6
Proof usesFirst Bernoulli formula for the inverse of Zagier's matrix · The two Bernoulli formulas for the inverse of Zagier's matrix agree · Left inverse of Zagier's matrix · Second Bernoulli formula for the inverse of Zagier's matrix · Zagier's matrix · Right inverse of Zagier's matrix
7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.