Bernoulli, Euler and Genocchi numbers

Combinatorial formulas for Bernoulli, Euler, tangent and Genocchi numbers (Garabedian's formulas, median Euler and Genocchi numbers, Euler–Seidel matrices, Carlitz q-Bernoulli polynomials), their divisibility, and sums of powers via Faulhaber coefficients.

• Carlitz q-Bernoulli polynomials
• Euler–Seidel matrices
• Faulhaber coefficients and sums of powers
• Garabedian's formulas for Bernoulli and Genocchi numbers
• Median Euler numbers
• Median Genocchi numbers

TheoremTangent numbers: 2-adic divisibility and a congruence mod 6#✓fully proved

Let \(T \colon \mathbb{N} \to \mathbb{Z}\) satisfy \(T(0) = 0\) and, for every \(m \in \mathbb{N}\),

\[T(m+1) = [m = 0] - \sum_{k=0}^{m} \binom{m}{k} T(k)\, T(m-k),\]

where \([m = 0]\) is \(1\) if \(m = 0\) and \(0\) otherwise. Then for every \(n \ge 1\), \(2^n\) divides \(T(2n+1)\) and \(T(2n+1)/2^n \equiv (-1)^n 4^{n-1} \pmod 6\).

These conditions determine \(T\): its values are the coefficients of the exponential generating function of \(\tanh x\), the signed tangent numbers (unsigned, OEIS A009006). The source defines the tangent numbers through \(1 + \tanh x\), which agrees with this recurrence at odd indices.

theorem tangentNumber_two_adic_divisibility_mod_six
    (T : ℕ → ℤ)
    (hT_zero : T 0 = 0)
    (hT_succ : ∀ m : ℕ,
      T (m + 1) =
        (if m = 0 then 1 else 0) -
          ∑ k ∈ Finset.range (m + 1), (m.choose k : ℤ) * T k * T (m - k))
    (n : ℕ) (hn : 1 ≤ n) :
    ((2 : ℤ) ^ n ∣ T (2 * n + 1)) ∧
      Int.ModEq 6 (T (2 * n + 1) / (2 : ℤ) ^ n)
        ((-1 : ℤ) ^ n * 4 ^ (n - 1))

Sources

• Kwang-Wu Chen, "An Interesting Lemma for Regular C-fractions," Journal of Integer Sequences 6 (2003), Article 03.4.8, Theorem, equation, lines 362–369 (tangent numbers defined at lines 351–360), https://cs.uwaterloo.ca/journals/JIS/VOL6/Chen/chen53.tex

DefinitionWeighted affine power sum#✓fully proved

Let \(R\) be a ring, \(a, b\) integers, \(u \in R\) and \(n, p\) natural numbers. The weighted affine power sum is

\[S_p(a, b; u, n + 1) = \sum_{k=0}^{n} u^k (ak + b)^p,\]

computed in \(R\) with \(a\), \(b\) and \(k\) mapped into \(R\).

Unlike later generating-function identities in the source, this finite definition does not require \(u\) to be nonzero.

public def weightedAffinePowerSum {R : Type*} [Ring R]
    (a b : ℤ) (u : R) (n p : ℕ) : R :=
  ∑ k ∈ Finset.range (n + 1), u ^ k * ((a : R) * (k : R) + (b : R)) ^ p

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.