Hankel determinants of Catalan sums

TheoremLayman's Catalan-sum Hankel determinant, including the empty matrix#✓fully proved

Let \(C_m\) denote the \(m\)-th Catalan number and \(F_m\) the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For every natural number \(n\), the determinant of the \(n \times n\) integer matrix whose \((i, j)\) entry is \(C_{i+j+1} + C_{i+j+2}\) for \(0 \le i, j \le n-1\) equals \(F_{2n+2}\). For \(n = 0\) the matrix is empty and both sides equal \(1\).

theorem layman_catalan_sum_hankel_det_unrestricted (n : ℕ) :
    Matrix.det (fun i j : Fin n =>
      ((catalan (i.val + j.val + 1) + catalan (i.val + j.val + 2) : ℕ) : ℤ)) =
      (Nat.fib (2 * n + 2) : ℤ)
Used by 1
Used byLayman's Catalan-sum Hankel determinant

TheoremLayman's Catalan-sum Hankel determinant#✓fully proved

Let \(C_m\) denote the \(m\)-th Catalan number and \(F_m\) the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For every integer \(n \ge 1\), the determinant of the \(n \times n\) integer matrix whose \((i, j)\) entry is \(C_{i+j+1} + C_{i+j+2}\) for \(0 \le i, j \le n-1\) equals \(F_{2n+2}\).

theorem layman_catalan_sum_hankel_det (n : ℕ) (hn : 1 ≤ n) :
    Matrix.det (fun i j : Fin n =>
      ((catalan (i.val + j.val + 1) + catalan (i.val + j.val + 2) : ℕ) : ℤ)) =
      (Nat.fib (2 * n + 2) : ℤ)
Sources
Uses 1
Proof usesLayman's Catalan-sum Hankel determinant, including the empty matrix
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.