Genocchi numbers

DefinitionGenerating function of the Genocchi numbers#✓fully proved

The Genocchi power series is the formal power series \(\frac{2x}{e^x + 1} = 2x \cdot (e^x + 1)^{-1}\) in \(\mathbb{Q}[[x]]\), where \(e^x = \sum_{n \ge 0} x^n / n!\) is the exponential power series and \((e^x + 1)^{-1}\) is the inverse of \(e^x + 1\) among formal power series. It is the exponential generating function of the Genocchi numbers \(G_n\), that is, \(\frac{2x}{e^x + 1} = \sum_{n \ge 0} G_n \frac{x^n}{n!}\).

This retains the standard convention \(\frac{2x}{e^x + 1}\) stated by Chen and used independently by Kida; the sign-changed variant consumes only even-index terms, where the conventions agree.

public noncomputable def genocchiPowerSeries : PowerSeries ℚ :=
  2 * PowerSeries.X * (PowerSeries.exp ℚ + 1)⁻¹

Sources

• Chen, JIS VOL6 (chen50.tex, lines 296-300): https://cs.uwaterloo.ca/journals/JIS/VOL6/Chen/chen50.html
• Kida, JIS VOL16: https://cs.uwaterloo.ca/journals/JIS/VOL16/Kida/kida2.html

Used by 5

Used byDivisibility of the median Genocchi numbers · Genocchi numbers · Genocchi numbers from their generating function · Genocchi numbers in terms of Bernoulli numbers · The Genocchi power series is \(2x/(e^x + 1)\)

DefinitionGenocchi numbers#✓fully proved

For a natural number \(n\), the Genocchi number \(G_n \in \mathbb{Q}\) is \(n!\) times the coefficient of \(x^n\) in the Genocchi power series \(\frac{2x}{e^x + 1} \in \mathbb{Q}[[x]]\), so that \(\frac{2x}{e^x + 1} = \sum_{n \ge 0} G_n \frac{x^n}{n!}\).

public noncomputable def genocchiNumber (n : ℕ) : ℚ :=
  (n.factorial : ℚ) * (PowerSeries.coeff n) genocchiPowerSeries

Sources

• Chen, JIS VOL6 (chen50.tex, lines 296-300): https://cs.uwaterloo.ca/journals/JIS/VOL6/Chen/chen50.html
• Kida, JIS VOL16: https://cs.uwaterloo.ca/journals/JIS/VOL16/Kida/kida2.html

Uses 1 · Used by 10

Statement usesGenerating function of the Genocchi numbers

Used byGarabedian's formula for the Genocchi numbers · Garabedian's formula for the Genocchi numbers, including \(n = 0\) · Divisibility of the median Genocchi numbers · Genocchi–Lucas coefficients · Genocchi numbers via Stirling numbers of the second kind · Genocchi–Lucas sum for powers of the conjugate golden ratio · Genocchi numbers from their generating function · Genocchi numbers in terms of Bernoulli numbers · Explicit formula for Genocchi numbers via Stirling numbers · The two definitions of the Genocchi numbers agree

TheoremThe Genocchi power series is \(2x/(e^x + 1)\)#✓fully proved

The Genocchi power series equals \(2x \cdot (e^x + 1)^{-1}\) in \(\mathbb{Q}[[x]]\), where \(e^x = \sum_{n \ge 0} x^n / n!\) is the exponential power series and \((e^x + 1)^{-1}\) is the inverse of \(e^x + 1\) among formal power series.

public theorem genocchiPowerSeries_eq :
    genocchiPowerSeries = 2 * PowerSeries.X * (PowerSeries.exp ℚ + 1)⁻¹

Uses 1 · Used by 2

Statement usesGenerating function of the Genocchi numbers

Used byDivisibility of the median Genocchi numbers · Genocchi numbers in terms of Bernoulli numbers

TheoremGenocchi numbers from their generating function#✓fully proved

For every natural number \(n\), the Genocchi number \(G_n\) equals \(n!\) times the coefficient of \(x^n\) in the Genocchi power series \(\frac{2x}{e^x + 1} \in \mathbb{Q}[[x]]\).

public theorem genocchiNumber_eq (n : ℕ) :
    genocchiNumber n = (n.factorial : ℚ) * (PowerSeries.coeff n) genocchiPowerSeries

Uses 2 · Used by 2

Statement usesGenocchi numbers · Generating function of the Genocchi numbers

Used byDivisibility of the median Genocchi numbers · Genocchi numbers in terms of Bernoulli numbers

TheoremGenocchi numbers in terms of Bernoulli numbers#✓fully proved

For every natural number \(n\), the Genocchi number \(G_n\), defined by \(\frac{2x}{e^x + 1} = \sum_{m \ge 0} G_m \frac{x^m}{m!}\), satisfies \(G_n = 2(1 - 2^n) B_n\), where \(B_n\) is the \(n\)-th Bernoulli number with the convention \(B_1 = -\tfrac{1}{2}\).

theorem genocchiNumber_eq_bernoulli (n : ℕ) :
    genocchiNumber n = 2 * (1 - (2 : ℚ) ^ n) * bernoulli n

Uses 4 · Used by 2

Statement usesGenocchi numbers

Proof usesGenocchi numbers from their generating function · Generating function of the Genocchi numbers · The Genocchi power series is \(2x/(e^x + 1)\)

Used byGarabedian's formula for the Genocchi numbers, including \(n = 0\) · The two definitions of the Genocchi numbers agree

TheoremThe two definitions of the Genocchi numbers agree#✓fully proved

For every natural number \(n\), the rational number \(2(1 - 2^n) B_n\), where \(B_n\) is the \(n\)-th Bernoulli number with the convention \(B_1 = -\tfrac{1}{2}\), equals the Genocchi number \(G_n\) defined by the exponential generating function \(\frac{2x}{e^x + 1} = \sum_{m \ge 0} G_m \frac{x^m}{m!}\).

theorem genocchiNumberViaBernoulli_eq_genocchiNumber (n : ℕ) :
    genocchiNumberViaBernoulli n = genocchiNumber n

Uses 3 · Used by 1

Statement usesGenocchi numbers · Genocchi numbers via Bernoulli numbers

Proof usesGenocchi numbers in terms of Bernoulli numbers

Used byDivisibility of the median Genocchi numbers

DefinitionIterated forward differences of a power on \(\mathbb{Q}\)#✓fully proved

For a rational number \(x\) and natural numbers \(k\) and \(n\), \(\Delta^k x^n\) denotes the value at \(x\) of the \(k\)-th iterate of the forward difference operator applied to the function \(y \mapsto y^n\) on \(\mathbb{Q}\), where the forward difference of \(f \colon \mathbb{Q} \to \mathbb{Q}\) is the function \(y \mapsto f(y + 1) - f(y)\).

noncomputable def diffPowEval (x : ℚ) (k n : ℕ) : ℚ :=
  ((fun f : ℚ → ℚ => fun y => f (y + 1) - f y)^[k]
    (fun y => y ^ n)) x

Used by 2

Used byBernoulli numbers via forward differences at \(1\) · Bernoulli numbers via forward differences at \(0\)

DefinitionThe Zerroukhat–Khaldi sum \(U(m, k)\)#✓fully proved

For natural numbers \(m\) and \(k\), define the rational number

\[U(m, k) = \sum_{j=0}^{m} (-1)^{k+j+m} \frac{(k+j-1)!}{2^{k+j-1}} S(m, j),\]

where \(S(m, j)\) is the Stirling number of the second kind and, in the term with \(k = j = 0\), \(k + j - 1\) is read as \(0\), so that this term is \((-1)^m S(m, 0)\).

def zerroU (m k : ℕ) : ℚ :=
  ∑ j ∈ Finset.range (m + 1),
    (-1 : ℚ) ^ (k + j + m) * ((k + j - 1).factorial : ℚ) /
      2 ^ (k + j - 1) * (Nat.stirlingSecond m j : ℚ)

Used by 2

Used byThe Zerroukhat–Khaldi sum \(H_{n,m}\) · Recurrence for the Zerroukhat–Khaldi sums \(U\)

DefinitionThe Zerroukhat–Khaldi sum \(H_{n,m}\)#✓fully proved

For natural numbers \(n\) and \(m\), define the rational number

\[H_{n,m} = (-1)^n \, n \sum_{k=1}^{n-m} U(m+1, k) \, S(n-m, k),\]

where \(U(m+1, k)\) is the Zerroukhat–Khaldi sum \(U\), \(S(n-m, k)\) is the Stirling number of the second kind, and \(n - m\) is truncated at \(0\), so that \(H_{n,m} = 0\) when \(m \ge n\).

def zerroH (n m : ℕ) : ℚ :=
  (-1 : ℚ) ^ n * (n : ℚ) *
    ∑ k ∈ Finset.Icc 1 (n - m), zerroU (m + 1) k *
      (Nat.stirlingSecond (n - m) k : ℚ)

Uses 1 · Used by 1

Statement usesThe Zerroukhat–Khaldi sum \(U(m, k)\)

Used byA step identity for the Zerroukhat–Khaldi sums \(H_{n,m}\)

TheoremExplicit formula for Genocchi numbers via Stirling numbers#●ready to prove

Let \(n\) and \(r\) be positive integers with \(n \ge r + 1\), let \(G_n\) be the \(n\)-th Genocchi number and let \(S(a, b)\) denote the Stirling numbers of the second kind. For \(k \ge 1\) write \(c_k = \sum_{j=0}^{r} (-1)^{k+j+r} \frac{(k+j-1)!}{2^{k+j-1}} S(r, j)\). Then \(G_n = (-1)^n \, n \sum_{k=1}^{n-r} c_k \, S(n-r, k)\).

theorem_wanted genocchiNumber_eq_sum (n r : ℕ) (hn : 1 ≤ n)
    (hr : 1 ≤ r) (hnr : r + 1 ≤ n) :
    MetaMathlibExt.genocchiNumber n =
      (-1 : ℚ) ^ n * (n : ℚ) *
        ∑ k ∈ Finset.Icc 1 (n - r),
          (∑ j ∈ Finset.range (r + 1),
            (-1 : ℚ) ^ (k + j + r) *
              ((k + j - 1).factorial : ℚ) / 2 ^ (k + j - 1) *
              (Nat.stirlingSecond r j : ℚ)) *
          (Nat.stirlingSecond (n - r) k : ℚ)

Sources

• Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers", Theorem 1.

Uses 1

Statement usesGenocchi numbers

TheoremBernoulli numbers via forward differences at \(0\)#●ready to prove

Let \(n\) and \(r\) be positive integers with \(n \ge r + 1\), let \(B_n\) be the \(n\)-th Bernoulli number, let \(S(a, b)\) denote the Stirling numbers of the second kind and let \(\Delta^k 0^m\) be the \(k\)-th forward difference of \(y \mapsto y^m\) at \(0\). For \(k \ge 1\) write \(d_k = \sum_{j=0}^{r} (-1)^{k+j+r+1} \, 2^{r-j} \, \frac{(k+j-1)!}{k!} \, S(r, j)\). Then \((-1)^n B_n = \frac{n}{2^n - 1} \sum_{k=1}^{n-r} d_k \, \frac{\Delta^k 0^{n-r}}{2^{k+r}}\).

theorem_wanted neg_one_pow_mul_bernoulli_eq_sum_zero
    (n r : ℕ) (hn : 1 ≤ n) (hr : 1 ≤ r) (hnr : r + 1 ≤ n) :
    (-1 : ℚ) ^ n * bernoulli n =
      (n : ℚ) / (2 ^ n - 1) *
        ∑ k ∈ Finset.Icc 1 (n - r),
          (∑ j ∈ Finset.range (r + 1),
            (-1 : ℚ) ^ (k + j + r + 1) * 2 ^ (r - j) *
              ((k + j - 1).factorial : ℚ) / k.factorial *
              (Nat.stirlingSecond r j : ℚ)) *
          (diffPowEval 0 k (n - r) / 2 ^ (k + r))

Sources

• Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers", Corollary 2.

Uses 1

Statement usesIterated forward differences of a power on \(\mathbb{Q}\)

TheoremBernoulli numbers via forward differences at \(1\)#●ready to prove

Let \(n\) and \(r\) be positive integers with \(n \ge r + 1\), let \(B_n\) be the \(n\)-th Bernoulli number, let \(S(a, b)\) denote the Stirling numbers of the second kind and let \(\Delta^k 1^m\) be the \(k\)-th forward difference of \(y \mapsto y^m\) at \(1\). For \(k \ge 0\) write \(e_k = \sum_{j=0}^{r} (-1)^{k+j+r} \, 2^{r-j} \, \frac{(k+j)!}{k!} \, S(r, j)\). Then \((-1)^n B_n = \frac{n}{2^n - 1} \sum_{k=0}^{n-1-r} e_k \, \frac{\Delta^k 1^{n-1-r}}{2^{k+1+r}}\).

theorem_wanted neg_one_pow_mul_bernoulli_eq_sum_one
    (n r : ℕ) (hn : 1 ≤ n) (hr : 1 ≤ r) (hnr : r + 1 ≤ n) :
    (-1 : ℚ) ^ n * bernoulli n =
      (n : ℚ) / (2 ^ n - 1) *
        ∑ k ∈ Finset.range (n - r),
          (∑ j ∈ Finset.range (r + 1),
            (-1 : ℚ) ^ (k + j + r) * 2 ^ (r - j) *
              ((k + j).factorial : ℚ) / k.factorial *
              (Nat.stirlingSecond r j : ℚ)) *
          (diffPowEval 1 k (n - 1 - r) / 2 ^ (k + 1 + r))

Sources

• Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers", Corollary 2.

Uses 1

Statement usesIterated forward differences of a power on \(\mathbb{Q}\)

TheoremRecurrence for the Zerroukhat–Khaldi sums \(U\)#●ready to prove

Let \(U(m, k)\) be the Zerroukhat–Khaldi sum. For all natural numbers \(r\) and \(k\) with \(k \ge 1\), \(U(r+1, k) = U(r, k+1) + k \, U(r, k)\).

theorem_wanted zerroU_succ (r k : ℕ) (hk : 1 ≤ k) :
    zerroU (r + 1) k = zerroU r (k + 1) + (k : ℚ) * zerroU r k

Sources

• Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers", Lemma 3.

Uses 1

Statement usesThe Zerroukhat–Khaldi sum \(U(m, k)\)

TheoremA step identity for the Zerroukhat–Khaldi sums \(H_{n,m}\)#●ready to prove

Let \(H_{n,m}\) denote the Zerroukhat–Khaldi sum. For all natural numbers \(n\) and \(r\) with \(r \ge 1\) and \(n \ge r + 1\), \(H_{n,r} = H_{n,r-1}\).

theorem_wanted zerroH_eq (n r : ℕ) (hr : 1 ≤ r)
    (hnr : r + 1 ≤ n) :
    zerroH n r = zerroH n (r - 1)

Sources

• Schehrazade Zerroukhat and Laala Khaldi, "A Note on Explicit Formulas for Bernoulli and Genocchi Numbers", Lemma 3.

Uses 1

Statement usesThe Zerroukhat–Khaldi sum \(H_{n,m}\)

9 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.