Euler–Seidel matrices

DefinitionEuler–Seidel matrix#✓fully proved

Let \(M\) be a type with an addition and let \((a_n)_{n \ge 0}\) be a sequence in \(M\). The Euler–Seidel matrix of \(a\) is the array \((a_n^k)_{n, k \ge 0}\), with entry \(a_n^k\) in position \((n, k)\), defined by \(a_n^0 = a_n\) and \(a_n^k = a_n^{k-1} + a_{n+1}^{k-1}\) for \(k \ge 1\).

def eulerSeidelMatrix {M : Type*} [Add M] (a : ℕ → M) : ℕ → ℕ → M
  | n, 0 => a n
  | n, k + 1 => eulerSeidelMatrix a n k + eulerSeidelMatrix a (n + 1) k

Used by 4

Used byClosed form of the Euler–Seidel matrix · Median Euler numbers · Median Euler numbers modulo three and five · Divisibility of the median Genocchi numbers

TheoremClosed form of the Euler–Seidel matrix#✓fully proved

Let \(M\) be an additive commutative monoid and let \((a_n)_{n \ge 0}\) be a sequence in \(M\). For all \(n, k \ge 0\), the entry \(a_n^k\) of the Euler–Seidel matrix of \(a\) equals \(\sum_{i=0}^{k} \binom{k}{i} a_{n+i}\).

public theorem eulerSeidelMatrix_eq_sum {M : Type*} [AddCommMonoid M] (a : ℕ → M)
    (n k : ℕ) :
    eulerSeidelMatrix a n k = ∑ i ∈ Finset.range (k + 1), k.choose i • a (n + i)

Uses 1 · Used by 2

Statement usesEuler–Seidel matrix

Used byMedian Euler numbers modulo three and five · Divisibility of the median Genocchi numbers

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.