Garabedian's formulas for Bernoulli and Genocchi numbers

TheoremGarabedian's formula for the Bernoulli numbers, including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[2(1 - 2^n) B_n = n \sum_{k=1}^{n} \frac{(-1)^{n-k} (k-1)!\, S(n, k)}{2^{k-1}},\]

where \(B_n\) is the \(n\)-th Bernoulli number, with \(B_1 = -\frac{1}{2}\), and \(S(n, k)\) is the Stirling number of the second kind. At \(n = 0\) both sides are \(0\).

theorem garabedian_genocchi_formula_general (n : ℕ) :
    2 * (1 - (2 : ℚ) ^ n) * bernoulli n =
      n * ∑ k ∈ Finset.Icc 1 n,
        ((-1 : ℚ) ^ (n - k) * (Nat.factorial (k - 1) : ℚ) *
          Nat.stirlingSecond n k) / (2 : ℚ) ^ (k - 1)
Used by 2
Used byGarabedian's formula for the Bernoulli numbers · Garabedian's formula for the Genocchi numbers, including \(n = 0\)

TheoremGarabedian's formula for the Bernoulli numbers#✓fully proved

For every natural number \(n \ge 1\),

\[2(1 - 2^n) B_n = n \sum_{k=1}^{n} \frac{(-1)^{n-k} (k-1)!\, S(n, k)}{2^{k-1}},\]

where \(B_n\) is the \(n\)-th Bernoulli number, with \(B_1 = -\frac{1}{2}\), and \(S(n, k)\) is the Stirling number of the second kind.

The identity also holds for \(n = 0\), where both sides are \(0\).

@[nolint unusedArguments]
theorem garabedian_genocchi_formula (n : ℕ) (hn : 1 ≤ n) :
    2 * (1 - (2 : ℚ) ^ n) * bernoulli n =
      n * ∑ k ∈ Finset.Icc 1 n,
        ((-1 : ℚ) ^ (n - k) * (Nat.factorial (k - 1) : ℚ) *
          Nat.stirlingSecond n k) / (2 : ℚ) ^ (k - 1)
Sources
  • Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers," Journal of Integer Sequences 28 (2025), Article 25.6.7, equation (g19), lines 188–191 of the official TeX, https://cs.uwaterloo.ca/journals/JIS/VOL28/Zerroukhat/zerrou3.tex, which displays 2(1-2^n)B_n = G_n = n ∑ ... and notes Garabedian's formula is equivalent to it; this article states the outer (Bernoulli-to-sum) equality. Original: H. L. Garabedian, "A new formula for the Bernoulli numbers," Bull. Amer. Math. Soc. 46 (1940), 531–533.
Uses 1
Proof usesGarabedian's formula for the Bernoulli numbers, including \(n = 0\)

TheoremGarabedian's formula for the Genocchi numbers, including \(n = 0\)#✓fully proved

For every natural number \(n\), the Genocchi number \(G_n\), defined by \(\sum_{m \ge 0} G_m x^m / m! = 2x/(e^x + 1)\), satisfies

\[G_n = n \sum_{k=1}^{n} \frac{(-1)^{n-k} (k-1)!\, S(n, k)}{2^{k-1}},\]

where \(S(n, k)\) is the Stirling number of the second kind. At \(n = 0\) both sides are \(0\).

theorem genocchiNumber_eq_stirlingSecond_sum_general (n : ℕ) :
    genocchiNumber n =
      (n : ℚ) * ∑ k ∈ Finset.Icc 1 n,
        (-1 : ℚ) ^ (n - k) * (Nat.factorial (k - 1) : ℚ) * (Nat.stirlingSecond n k : ℚ) /
          (2 : ℚ) ^ (k - 1)
Uses 3 · Used by 1
Statement usesGenocchi numbers
Proof usesGarabedian's formula for the Bernoulli numbers, including \(n = 0\) · Genocchi numbers in terms of Bernoulli numbers
Used byGarabedian's formula for the Genocchi numbers

TheoremGarabedian's formula for the Genocchi numbers#✓fully proved

For every natural number \(n \ge 1\), the Genocchi number \(G_n\), defined by \(\sum_{m \ge 0} G_m x^m / m! = 2x/(e^x + 1)\), satisfies

\[G_n = n \sum_{k=1}^{n} \frac{(-1)^{n-k} (k-1)!\, S(n, k)}{2^{k-1}},\]

where \(S(n, k)\) is the Stirling number of the second kind.

The identity also holds for \(n = 0\), where both sides are \(0\).

The formula is due to H. L. Garabedian, "A new formula for the Bernoulli numbers," Bulletin of the American Mathematical Society 46 (1940), 531–533, DOI 10.1090/S0002-9904-1940-07255-6.

@[nolint unusedArguments]
theorem genocchiNumber_eq_stirlingSecond_sum (n : ℕ)
    (hn : 1 ≤ n) :
    genocchiNumber n =
      (n : ℚ) * ∑ k ∈ Finset.Icc 1 n,
        (-1 : ℚ) ^ (n - k) * (Nat.factorial (k - 1) : ℚ) * (Nat.stirlingSecond n k : ℚ) /
          (2 : ℚ) ^ (k - 1)
Sources
Uses 2
Statement usesGenocchi numbers
Proof usesGarabedian's formula for the Genocchi numbers, including \(n = 0\)
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.