Higher-order Bernoulli numbers

DefinitionHigher-order Bernoulli numbers#✓fully proved

For a complex number \(\alpha\) and a natural number \(n\), the higher-order Bernoulli number \(B_n^{(\alpha)}\) is \(n!\) times the coefficient of \(t^n\) in the formal power series \(\left(t / (e^t - 1)\right)^{\alpha}\). Here \(t / (e^t - 1)\) is the Bernoulli generating series \(\sum_{k \ge 0} B_k t^k / k!\) (with \(B_1 = -1/2\)), and its \(\alpha\)-th power is the binomial series \((1 + u)^{\alpha} = \sum_{j \ge 0} \binom{\alpha}{j} u^j\) with \(u = t / (e^t - 1) - 1\) substituted.

Equivalently, \(B_n^{(\alpha)} = B_n^{(\alpha)}(0)\), where the generalized Bernoulli polynomials \(B_n^{(\alpha)}(x)\) are given by the exponential generating function \(\sum_{n \ge 0} B_n^{(\alpha)}(x) t^n / n! = \left(t / (e^t - 1)\right)^{\alpha} e^{tx}\).

public noncomputable def higherOrderBernoulliNumber (α : ℂ) (n : ℕ) : ℂ :=
  (n.factorial : ℂ) * PowerSeries.coeff n
    (PowerSeries.subst (bernoulliPowerSeries ℂ - 1) (PowerSeries.binomialSeries ℂ α))

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL23/Chellal/chellal7.tex, lines 99-112.

Used by 3

Used byHigher-order Bernoulli numbers of natural order · Higher-order Bernoulli numbers of order one · Neto's identity for higher-order Bernoulli numbers

TheoremHigher-order Bernoulli numbers of natural order#✓fully proved

Let \(B_k\) denote the Bernoulli numbers, with \(B_1 = -1/2\). For natural numbers \(d\) and \(n\), the higher-order Bernoulli number \(B_n^{(d)}\) equals \(n!\) times the coefficient of \(t^n\) in the \(d\)-th power of the Bernoulli generating series \(\sum_{k \ge 0} B_k t^k / k!\).

public theorem higherOrderBernoulliNumber_nat (d n : ℕ) :
    higherOrderBernoulliNumber (d : ℂ) n =
      (n.factorial : ℂ) * PowerSeries.coeff n (bernoulliPowerSeries ℂ ^ d)

Uses 1 · Used by 2

Statement usesHigher-order Bernoulli numbers

Used byHigher-order Bernoulli numbers of order one · Neto's identity for higher-order Bernoulli numbers

TheoremHigher-order Bernoulli numbers of order one#✓fully proved

For every natural number \(n\), the higher-order Bernoulli number \(B_n^{(1)}\) equals the Bernoulli number \(B_n\), with the convention \(B_1 = -1/2\).

public theorem higherOrderBernoulliNumber_one (n : ℕ) :
    higherOrderBernoulliNumber 1 n = (bernoulli n : ℂ)

Uses 2

Statement usesHigher-order Bernoulli numbers

Proof usesHigher-order Bernoulli numbers of natural order

TheoremNeto's identity for higher-order Bernoulli numbers#✓fully proved

For every complex number \(x\) and all natural numbers \(n\) and \(\ell\),

\[\sum_{k=0}^{n} \binom{n}{k} x^{n-k} B_{\ell+k}^{(x)} = (-1)^{n+\ell} \sum_{k=0}^{\ell} \binom{\ell}{k} x^{\ell-k} B_{n+k}^{(x)},\]

where \(B_m^{(x)}\) is the higher-order Bernoulli number of order \(x\).

Proof: The substitution coefficient formula makes both sides polynomial in the order. For natural orders, the cited Bernoulli EGF gives the reflection identity, formal differentiation proves Neto's formula, and equality on all natural complex points finishes the polynomial argument.

public theorem neto_higher_order_bernoulli_identity (x : ℂ) (n ℓ : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      x ^ (n - k) * (Nat.choose n k : ℂ) * higherOrderBernoulliNumber x (ℓ + k)) =
    (-1 : ℂ) ^ (n + ℓ) *
      ∑ k ∈ Finset.range (ℓ + 1),
        x ^ (ℓ - k) * (Nat.choose ℓ k : ℂ) * higherOrderBernoulliNumber x (n + k)

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL23/Chellal/chellal7.tex, lines 662-670.

Uses 2

Statement usesHigher-order Bernoulli numbers

Proof usesHigher-order Bernoulli numbers of natural order

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.