Identities for Bernoulli numbers

TheoremAbel–Bernoulli sum#✓fully proved

Let \(B_k(t)\) denote the \(k\)-th Bernoulli polynomial. For every natural number \(n\) and all complex numbers \(x\) and \(y\) with \(x \neq 0\),

\[\sum_{l=0}^{n} \binom{n}{l} (x + l)^{l-1} B_{n-l}(y + n - l) = \frac{1}{x} B_n(y + x + n),\]

where \((x + l)^{l-1}\) is an integer power, so the term \(l = 0\) contains the factor \(x^{-1}\).

This is the first of the source's two Abel–Bernoulli sums.

theorem abel_bernoulli_sum :
    ∀ (n : ℕ) (x y : ℂ), x ≠ 0 →
      ∑ l ∈ Finset.range (n + 1),
        (Nat.choose n l : ℂ) * (x + (l : ℂ)) ^ ((l : ℤ) - 1) *
          Polynomial.eval₂ (algebraMap ℚ ℂ) (y + (n - l : ℕ))
            (Polynomial.bernoulli (n - l)) =
        (1 / x) * Polynomial.eval₂ (algebraMap ℚ ℂ) (y + x + (n : ℂ))
          (Polynomial.bernoulli n)
Sources
  • Claudio de J. Pita Ruiz V., "Carlitz-Type and Other Bernoulli Identities," Journal of Integer Sequences 19 (2016), Article 16.1.8, Proposition [Abel-Bernoulli sums], equation (5.11), lines 790–794, https://cs.uwaterloo.ca/journals/JIS/VOL19/Pita/pita23.tex

TheoremAbel–Hurwitz–Bernoulli multinomial identity#✓fully proved

Let \(B_k(t)\) denote the \(k\)-th Bernoulli polynomial. Let \(m \ge 2\) and \(n\) be natural numbers, let \(x_1, \dots, x_m\) be rational numbers, and let \(r\) be an index with \(1 \le r \le m\). Then

\[\sum_{l} \binom{n}{l_1, \dots, l_m} B_{l_r}(x_r + l_r) \prod_{j \neq r} (x_j + l_j)^{l_j} = \sum_{k=0}^{n} \binom{n}{k} \frac{(m + k - 2)!}{(m - 2)!} B_{n-k}(x_1 + \dots + x_m + n),\]

where the sum on the left runs over all \(l = (l_1, \dots, l_m) \in \mathbb{N}^m\) with \(l_1 + \dots + l_m = n\), and \(\binom{n}{l_1, \dots, l_m}\) is the multinomial coefficient.

The source states the identity for arbitrary real or complex parameters; this statement records its specialization to rational \(x_1, \dots, x_m\).

theorem abel_hurwitz_bernoulli_multinomial
    (m n : ℕ) (x : Fin m → ℚ) (r : Fin m) (hm : 2 ≤ m) :
    ∑ l ∈ (Fintype.piFinset (fun _ : Fin m => Finset.range (n + 1))).filter
      (fun l => ∑ i, l i = n),
      (Nat.multinomial Finset.univ l : ℚ) *
        (Polynomial.eval (x r + (l r : ℚ)) (Polynomial.bernoulli (l r)) *
        ∏ j ∈ Finset.univ.erase r, (x j + (l j : ℚ)) ^ l j) =
    ∑ l ∈ Finset.range (n + 1),
      (Nat.choose n l : ℚ) *
        ((Nat.factorial (m + l - 2) : ℚ) / (Nat.factorial (m - 2) : ℚ)) *
        Polynomial.eval ((∑ i, x i) + (n : ℚ)) (Polynomial.bernoulli (n - l))
Sources
  • Claudio de J. Pita Ruiz V., "Carlitz-Type and Other Bernoulli Identities," Journal of Integer Sequences 19 (2016), Article 16.1.8, Proposition [Abel-Hurwitz-Bernoulli identity] (a), equation (5.16), lines 821–829, https://cs.uwaterloo.ca/journals/JIS/VOL19/Pita/pita23.tex

TheoremCarlitz's Bernoulli identity#✓fully proved

Let \(B_j\) denote the \(j\)-th Bernoulli number, with \(B_1 = -1/2\). For all natural numbers \(m\) and \(n\),

\[(-1)^m \sum_{k=0}^{m} \binom{m}{k} B_{n+k} = (-1)^n \sum_{k=0}^{n} \binom{n}{k} B_{m+k}.\]
theorem carlitz_bernoulli_sum_symm (m n : ℕ) :
    (-1 : ℚ) ^ m * (Finset.range (m + 1)).sum
      (fun k => (Nat.choose m k : ℚ) * bernoulli (n + k)) =
    (-1 : ℚ) ^ n * (Finset.range (n + 1)).sum
      (fun k => (Nat.choose n k : ℚ) * bernoulli (m + k))
Sources
  • Pita Ruiz, “Carlitz-Type and Other Bernoulli Identities”; original L. Carlitz, Problem 795, Mathematics Magazine 44 (1971), p. 107.

TheoremEuler's convolution identity for Bernoulli numbers#✓fully proved

Let \(B_j\) denote the \(j\)-th Bernoulli number, with \(B_1 = -1/2\). For every natural number \(n \ge 1\),

\[\sum_{i=0}^{n} \binom{n}{i} B_i B_{n-i} = -n B_{n-1} - (n-1) B_n.\]
theorem euler_bernoulli_convolution (n : ℕ) (hn : 1 ≤ n) :
    ∑ i ∈ Finset.range (n + 1), (n.choose i : ℚ) * bernoulli i * bernoulli (n - i) =
      -(n : ℚ) * bernoulli (n - 1) - ((n : ℚ) - 1) * bernoulli n
Sources

TheoremGessel's Bernoulli-number identity#✓fully proved

Let \(B_j\) denote the \(j\)-th Bernoulli number, with \(B_1 = -1/2\). For all natural numbers \(n\), \(r\) and \(m\) with \(r\) odd and \(m \ge 1\),

\[\sum_{k=0}^{n+r} m^{n+r-k} \binom{n+r}{k} \binom{n+k+r}{r} B_{n+k} = \frac{r+1}{2} \sum_{k=1}^{m-1} \sum_{j=0}^{r+1} \binom{n+r}{j} \binom{n+r}{r+1-j} k^{j+n-1} (k-m)^{n+r-j}.\]

The powers on the right have integer exponents and nonzero rational bases: for \(n = 0\) the terms \(j = 0\) and \(j = r + 1\) have exponent \(-1\).

theorem gessel_bernoulli_number_identity (n r m : ℕ) (hr : Odd r) (hm : 1 ≤ m) :
    Finset.sum (Finset.range (n + r + 1)) (fun k =>
      (m : ℚ) ^ (n + r - k) * (Nat.choose (n + r) k : ℚ) *
        (Nat.choose (n + k + r) r : ℚ) * bernoulli (n + k)) =
    (((r : ℚ) + 1) / 2) * Finset.sum (Finset.Ico 1 m) (fun k =>
      Finset.sum (Finset.range (r + 2)) (fun j =>
        (Nat.choose (n + r) j : ℚ) * (Nat.choose (n + r) (r + 1 - j) : ℚ) *
          (k : ℚ) ^ ((j : ℤ) + (n : ℤ) - 1) *
            (((k : ℚ) - (m : ℚ)) ^ ((n : ℤ) + (r : ℤ) - (j : ℤ)))))
Sources
  • Redha Chellal and Farid Bencherif, An Identity for Generalized Bernoulli Polynomials, Journal of Integer Sequences 23 (2020), Article 20.11.2, formula t5 (the special case ℓ = n with r odd), lines 142–149, https://cs.uwaterloo.ca/journals/JIS/VOL23/Chellal/chellal7.tex. Quoted there from H. Belbachir and M. Rahmani, On Gessel-Kaneko's identity for Bernoulli numbers, Appl. Anal. Discrete Math. 7 (2013), 1–10. Original: I. M. Gessel, Applications of the classical umbral calculus, Algebra Universalis 49 (2003), 397–434.

TheoremGould's alternating identity for Bernoulli polynomials#✓fully proved

Let \(B_i\) denote the \(i\)-th Bernoulli number, with \(B_1 = -1/2\), and let \(B_j(x) = \sum_{i=0}^{j} \binom{j}{i} B_i x^{j-i}\) be the \(j\)-th Bernoulli polynomial. For every natural number \(n\) and every rational number \(x\),

\[\sum_{k=0}^{n} (-1)^k \binom{n}{k} B_{n+1}(x - k) = \frac{(n+1)!}{2} (2x - n - 1).\]
theorem gould_bernoulli_identity (n : ℕ) (x : ℚ) :
    ∑ k ∈ Finset.range (n + 1),
        (-1 : ℚ) ^ k * (Nat.choose n k : ℚ) *
          (Polynomial.bernoulli (n + 1)).eval (x - k) =
      (Nat.factorial (n + 1) : ℚ) / 2 * (2 * x - n - 1)
Sources

TheoremKaneko's Stirling-number formula for the Bernoulli numbers#✓fully proved

Let \(B_n\) denote the \(n\)-th Bernoulli number, with \(B_1 = -1/2\), and let \(S(n, j)\) denote the Stirling numbers of the second kind. For every natural number \(n\),

\[B_n = \sum_{m=1}^{n+1} \frac{(-1)^{m-1} (m-1)!\, S(n, m-1)}{m}.\]

This is Kaneko's explicit formula for the poly-Bernoulli numbers \(B_n^{(k)}\) at \(k = 1\). That formula carries a factor \((-1)^n\), which cancels against \(B_n^{(1)} = (-1)^n B_n\) (the numbers \(B_n^{(1)}\) come from the generating series \(t/(1 - e^{-t})\)).

theorem kaneko_bernoulli_stirling_sum
    (n : ℕ) :
    bernoulli n = ∑ m ∈ Finset.Icc 1 (n + 1),
      (-1 : ℚ) ^ (m - 1) * (Nat.factorial (m - 1) : ℚ) *
        (Nat.stirlingSecond n (m - 1) : ℚ) / (m : ℚ)
Sources
  • Y. Hamahata and H. Masubuchi, "Special Multi-Poly-Bernoulli Numbers," Journal of Integer Sequences 10 (2007), Article 07.4.1, Theorem [Kaneko1], lines 144–152, https://cs.uwaterloo.ca/journals/JIS/VOL10/Hamahata/hamahata3.tex citing M. Kaneko, "Poly-Bernoulli numbers," Journal de Théorie des Nombres de Bordeaux 9 (1997), 221–228.

TheoremTuenter's power-sum identity for Bernoulli numbers#✓fully proved

Let \(a\) and \(b\) be nonzero complex numbers and let \(n \ge 1\) be a natural number with \(b^n \ne a^n\). Let \(\sigma_x(i) \in \mathbb{C}\), for \(x \in \mathbb{C}\) and \(i \in \mathbb{N}\), satisfy \((i+1)\,\sigma_x(i) = B_{i+1}(x+1) - B_{i+1}\) for all \(x\) and \(i\), where \(B_m(t)\) denotes the Bernoulli polynomial and \(B_m\) the Bernoulli number, with \(B_1 = -\tfrac{1}{2}\). Then

\[B_n = \frac{1}{b^n - a^n} \sum_{i=1}^{n} \binom{n}{i} B_{n-i} \left( a^{n-1-i} \, b^i \, \sigma_{a-1}(i) - a^i \, b^{n-1-i} \, \sigma_{b-1}(i) \right),\]

where the exponents \(n - 1 - i\) are integers, equal to \(-1\) when \(i = n\).

For a natural number \(x\) and \(i \ge 1\) the relation gives \(\sigma_x(i) = 1^i + 2^i + \dots + x^i\).

MetaMathlibExt.tuenter_bernoulli_power_sum_identity · 15 lines 
theorem tuenter_bernoulli_power_sum_identity
    (a b : ℂ) (n : ℕ) (hn : 0 < n)
    (ha : a ≠ 0) (hb : b ≠ 0)
    (sigma : ℂ → ℕ → ℂ)
    (hsigma : ∀ x i,
      ((i + 1 : ℕ) : ℂ) * sigma x i =
        (Polynomial.bernoulli (i + 1)).eval₂ (algebraMap ℚ ℂ) (x + 1) -
          (bernoulli (i + 1) : ℂ))
    (hden : b ^ n - a ^ n ≠ 0) :
    (bernoulli n : ℂ) =
      1 / (b ^ n - a ^ n) *
        ∑ i ∈ Finset.Icc 1 n,
          (n.choose i : ℂ) * (bernoulli (n - i) : ℂ) *
            (a ^ ((n : ℤ) - 1 - (i : ℤ)) * b ^ i * sigma (a - 1) i -
              a ^ i * b ^ ((n : ℤ) - 1 - (i : ℤ)) * sigma (b - 1) i)
Sources
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.