Bernoulli numbers of the second kind

DefinitionGenerating function of the Bernoulli numbers of the second kind#✓fully proved

Let \(G(t)\) be the inverse, in the ring \(\mathbb{Q}[[t]]\) of formal power series, of the series \(\sum_{n \ge 0} \frac{(-1)^n}{n + 1} t^n\), which is invertible because its constant coefficient is \(1\).

Analytically this series is \(\log(1 + t) / t\), so \(G(t) = t / \log(1 + t)\); the logarithm itself is not invertible, having zero constant coefficient.

public noncomputable def bernoulliSecondPowerSeries : PowerSeries ℚ :=
  (PowerSeries.mk fun n => (-1 : ℚ) ^ n / (n + 1))⁻¹
Used by 6
Used byBernoulli numbers of the second kind · Recurrence for the Bernoulli numbers of the second kind · Bernoulli numbers of the second kind as scaled coefficients · Generating function of the Bernoulli numbers of the second kind as an inverse · Defining identity of the generating function of the Bernoulli numbers of the second kind · Coefficient identity for the generating function of the Bernoulli numbers of the second kind

DefinitionBernoulli numbers of the second kind#✓fully proved

For a natural number \(n\), the Bernoulli number of the second kind \(B_n^*\) is the rational number \(n!\) times the coefficient of \(t^n\) in \(G(t) \in \mathbb{Q}[[t]]\), the inverse of the formal power series \(\sum_{k \ge 0} \frac{(-1)^k}{k + 1} t^k\). Thus \(G(t) = \sum_{n \ge 0} B_n^* t^n / n!\).

Analytically \(G(t) = t / \log(1 + t)\); this is Roman's normalization, with \(B_0^* = 1\), \(B_1^* = 1/2\) and \(B_2^* = -1/6\).

public noncomputable def bernoulliSecond (n : ℕ) : ℚ :=
  (n.factorial : ℚ) * (PowerSeries.coeff n) bernoulliSecondPowerSeries
Uses 1 · Used by 9
Statement usesGenerating function of the Bernoulli numbers of the second kind
Used byBernoulli numbers in terms of Bernoulli numbers of the second kind · Recurrence for the Bernoulli numbers of the second kind · Bernoulli numbers of the second kind as scaled coefficients · Bernoulli numbers of the second kind in terms of Bernoulli numbers · Bernoulli numbers of the second kind via Stirling numbers of the first kind · Falling factorials in the Bernoulli polynomial basis · Sums of signed Stirling numbers of the first kind with shifted reciprocal weights · Shifted Stirling convolution as a Bernoulli number of the second kind · Stirling convolution as a sum of Bernoulli numbers of the second kind

TheoremGenerating function of the Bernoulli numbers of the second kind as an inverse#✓fully proved

The generating function \(G(t)\) of the Bernoulli numbers of the second kind equals the inverse, in the ring \(\mathbb{Q}[[t]]\) of formal power series, of the series \(\sum_{n \ge 0} \frac{(-1)^n}{n + 1} t^n\).

public theorem bernoulliSecondPowerSeries_eq :
    bernoulliSecondPowerSeries =
      (PowerSeries.mk fun n => (-1 : ℚ) ^ n / (n + 1))⁻¹
Uses 1
Statement usesGenerating function of the Bernoulli numbers of the second kind

TheoremBernoulli numbers of the second kind as scaled coefficients#✓fully proved

For every natural number \(n\), the Bernoulli number of the second kind \(B_n^*\) equals \(n!\) times the coefficient of \(t^n\) in the generating function \(G(t) \in \mathbb{Q}[[t]]\) of the Bernoulli numbers of the second kind.

public theorem bernoulliSecond_eq (n : ℕ) :
    bernoulliSecond n =
      (n.factorial : ℚ) * (PowerSeries.coeff n) bernoulliSecondPowerSeries
Uses 2 · Used by 1
Statement usesBernoulli numbers of the second kind · Generating function of the Bernoulli numbers of the second kind
Used byRecurrence for the Bernoulli numbers of the second kind

TheoremDefining identity of the generating function of the Bernoulli numbers of the second kind#✓fully proved

Defining identity of the generating function of the Bernoulli numbers of the second kind. In the ring \(\mathbb{Q}[[t]]\) of formal power series, the generating function \(G(t)\) of the Bernoulli numbers of the second kind satisfies \(G(t) \cdot \sum_{n \ge 0} \frac{(-1)^n}{n + 1} t^n = 1\).

Analytically, \(\sum_{n \ge 0} \frac{(-1)^n}{n + 1} t^n = \log(1 + t) / t\).

public theorem bernoulliSecondPowerSeries_mul_mk :
    bernoulliSecondPowerSeries *
        (PowerSeries.mk fun n => (-1 : ℚ) ^ n / (n + 1)) = 1
Uses 1 · Used by 1
Statement usesGenerating function of the Bernoulli numbers of the second kind
Used byCoefficient identity for the generating function of the Bernoulli numbers of the second kind

TheoremCoefficient identity for the generating function of the Bernoulli numbers of the second kind#✓fully proved

Coefficient identity for the generating function of the Bernoulli numbers of the second kind. Let \(g_i\) be the coefficient of \(t^i\) in the generating function \(G(t) \in \mathbb{Q}[[t]]\) of the Bernoulli numbers of the second kind. For every natural number \(n\), the sum of \(g_i \cdot (-1)^j / (j + 1)\) over all pairs \((i, j)\) of natural numbers with \(i + j = n\) equals \(1\) if \(n = 0\) and \(0\) if \(n \ge 1\).

public theorem sum_antidiagonal_bernoulliSecondPowerSeries_coeff (n : ℕ) :
    (∑ x ∈ Finset.antidiagonal n,
      (PowerSeries.coeff x.1) bernoulliSecondPowerSeries *
        ((-1 : ℚ) ^ x.2 / (x.2 + 1))) = if n = 0 then 1 else 0
Uses 2 · Used by 1
Statement usesGenerating function of the Bernoulli numbers of the second kind
Proof usesDefining identity of the generating function of the Bernoulli numbers of the second kind
Used byRecurrence for the Bernoulli numbers of the second kind

TheoremRecurrence for the Bernoulli numbers of the second kind#✓fully proved

For every natural number \(n \ge 1\), the Bernoulli numbers of the second kind \(B_k^*\) satisfy \(B_n^* / n! = -\sum_{k=0}^{n-1} (B_k^* / k!) \cdot (-1)^{n-k} / (n - k + 1)\).

public theorem bernoulliSecond_div_factorial_eq (n : ℕ) (hn : 1 ≤ n) :
    bernoulliSecond n / (n.factorial : ℚ) =
      -∑ k ∈ Finset.range n, (bernoulliSecond k / (k.factorial : ℚ)) *
        ((-1 : ℚ) ^ (n - k) / (n - k + 1))
Uses 4
Statement usesBernoulli numbers of the second kind
Proof usesGenerating function of the Bernoulli numbers of the second kind · Bernoulli numbers of the second kind as scaled coefficients · Coefficient identity for the generating function of the Bernoulli numbers of the second kind

TheoremAsymptotic expansion of the Bernoulli numbers of the second kind#✓fully proved

For a natural number \(n\) let \(b_n = \frac{1}{n!} \int_0^1 x (x - 1) \cdots (x - n + 1) dx\), and for a natural number \(k\) let \(\beta_k\) be \((-1)^k\) times the \((k + 1)\)-th derivative of \(1 / \Gamma\) at \(0\). Then for every natural number \(m\), as \(n \to \infty\),

\[b_n - \frac{(-1)^{n+1}}{n (\log n)^2} \sum_{k=0}^{m} \frac{\beta_k}{(\log n)^k} = o\left(\frac{1}{n (\log n)^{m+2}}\right).\]

The main term \((-1)^{n+1} / (n (\log n)^2)\) is Steffensen's approximation, as noted in the source.

theorem bernoulli_second_kind_asymptotic (b : ℕ → ℝ) (β : ℕ → ℝ)
  (hb : ∀ n : ℕ, b n = (∫ x in (0 : ℝ)..1, ∏ j ∈ Finset.range n, (x - (j : ℝ))) /
    (Nat.factorial n : ℝ))
  (hβ : ∀ k : ℕ, β k = (-1 : ℝ) ^ k * iteratedDeriv (k + 1) (fun s : ℝ => (Real.Gamma s)⁻¹)
    (0 : ℝ)) :
  ∀ m : ℕ, Asymptotics.IsLittleO Filter.atTop
    (fun n : ℕ => b n -
    (((-1 : ℝ) ^ (n + 1) / ((n : ℝ) * (Real.log (n : ℝ)) ^ 2)) * ∑ k ∈ Finset.range (m + 1), β k /
    (Real.log (n : ℝ)) ^ k)) (fun n : ℕ => 1 / ((n : ℝ) * (Real.log (n : ℝ)) ^ (m + 2)))
Sources
  • Gergő Nemes, "An Asymptotic Expansion for the Bernoulli Numbers of the Second Kind," Journal of Integer Sequences 14 (2011), Article 11.4.8, Theorem, equations, lines 124–133, https://cs.uwaterloo.ca/journals/JIS/VOL14/Nemes/nemes4.tex
Uses 1
Proof usesWatson's lemma for Laplace integrals

TheoremBernoulli polynomials in the falling-factorial basis#●ready to prove

Let \(B_m\) be the Bernoulli numbers (with \(B_1 = -1/2\)), \(B_n(X) = \sum_{i=0}^{n} \binom{n}{i} B_i X^{n-i}\) the Bernoulli polynomials over \(\mathbb{Q}\), \(S(m, j)\) the Stirling numbers of the second kind and \(X^{\underline{k}} = X(X-1)\cdots(X-k+1)\) the falling factorial. For every natural number \(n\), in \(\mathbb{Q}[X]\),

\[B_n(X) = B_n + \sum_{k=1}^{n} \frac{n}{k} \, S(n-1, k-1) \, X^{\underline{k}}.\]
theorem_wanted bernoulli_poly_eq (n : ℕ) :
    Polynomial.bernoulli n =
      Polynomial.C (bernoulli n) +
        ∑ k ∈ Finset.Icc 1 n, Polynomial.C
          ((n : ℚ) / k * (Nat.stirlingSecond (n - 1) (k - 1) : ℚ)) *
          descPochhammer ℚ k
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 1.

TheoremBernoulli numbers in terms of Bernoulli numbers of the second kind#●ready to prove

Let \(B_m\) be the Bernoulli numbers (with \(B_1 = -1/2\)), \(B_m^*\) the Bernoulli numbers of the second kind and \(S(m, j)\) the Stirling numbers of the second kind. For every natural number \(n \ge 1\),

\[B_n = -\sum_{k=1}^{n} \frac{n}{k} \, S(n-1, k-1) \, B_k^*.\]
theorem_wanted bernoulli_eq_neg_sum (n : ℕ) (hn : 1 ≤ n) :
    bernoulli n =
      -∑ k ∈ Finset.Icc 1 n, (n : ℚ) / k *
        (Nat.stirlingSecond (n - 1) (k - 1) : ℚ) *
        MetaMathlibExt.bernoulliSecond k
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Corollary 2.
Uses 1
Statement usesBernoulli numbers of the second kind

TheoremStirling inversion#●ready to prove

Let \(s(m, j)\) be the signed Stirling numbers of the first kind and \(S(m, j)\) the Stirling numbers of the second kind. For all sequences \((u_n)_{n \ge 0}\) and \((v_n)_{n \ge 0}\) of rational numbers, \(u_n = \sum_{k=0}^{n} s(n, k) \, v_k\) for every natural number \(n\) if and only if \(v_n = \sum_{k=0}^{n} S(n, k) \, u_k\) for every natural number \(n\).

The paper states this for sequences of complex numbers.

theorem_wanted stirling_inversion_iff (u v : ℕ → ℚ) :
    (∀ n, u n = ∑ k ∈ Finset.range (n + 1),
      (MetaMathlibExt.signedStirlingFirst n k : ℚ) * v k) ↔
    (∀ n, v n = ∑ k ∈ Finset.range (n + 1),
      (Nat.stirlingSecond n k : ℚ) * u k)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Lemma 3.
Uses 1
Statement usesSigned Stirling numbers of the first kind

TheoremBernoulli numbers of the second kind in terms of Bernoulli numbers#●ready to prove

Let \(B_m\) be the Bernoulli numbers (with \(B_1 = -1/2\)), \(B_m^*\) the Bernoulli numbers of the second kind and \(s(m, j)\) the signed Stirling numbers of the first kind. For every natural number \(n \ge 1\),

\[B_n^* = -\sum_{k=1}^{n} \frac{n}{k} \, s(n-1, k-1) \, B_k.\]
theorem_wanted bernoulliSecond_eq_neg_sum (n : ℕ)
    (hn : 1 ≤ n) :
    MetaMathlibExt.bernoulliSecond n =
      -∑ k ∈ Finset.Icc 1 n, (n : ℚ) / k *
        (MetaMathlibExt.signedStirlingFirst (n - 1) (k - 1) : ℚ) * bernoulli k
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 4.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind

TheoremFalling factorials in the Bernoulli polynomial basis#●ready to prove

Let \(B_m^*\) be the Bernoulli numbers of the second kind, \(B_k(X)\) the Bernoulli polynomials over \(\mathbb{Q}\) (so that \(B_1(X) = X - 1/2\)), \(s(m, j)\) the signed Stirling numbers of the first kind and \(X^{\underline{n}} = X(X-1)\cdots(X-n+1)\) the falling factorial. For every natural number \(n\), in \(\mathbb{Q}[X]\),

\[X^{\underline{n}} = B_n^* + \sum_{k=1}^{n} \frac{n}{k} \, s(n-1, k-1) \, B_k(X).\]
theorem_wanted descPochhammer_eq (n : ℕ) :
    descPochhammer ℚ n =
      Polynomial.C (MetaMathlibExt.bernoulliSecond n) +
        ∑ k ∈ Finset.Icc 1 n, Polynomial.C
          ((n : ℚ) / k * (MetaMathlibExt.signedStirlingFirst (n - 1) (k - 1) : ℚ)) *
          Polynomial.bernoulli k
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 5.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind

TheoremShifted Stirling convolution formula for Bernoulli numbers#●ready to prove

For natural numbers \(k\) and \(n\) with \(1 \le k \le n\), write \(S(m,j)\) for the Stirling numbers of the second kind, \(s(m,j)\) for the signed Stirling numbers of the first kind, and \(B_m\) for the Bernoulli numbers with \(B_1 = -\tfrac12\). Then, in \(\mathbb{Q}\),

\[ \sum_{i=k}^{n} \frac{S(n-1,i-1)\, s(i,k)}{i} = \frac{1}{n} \binom{n}{k} B_{n-k}. \]
theorem_wanted sum_stirlingSecond_signed_div (n k : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∑ i ∈ Finset.Icc k n,
        (Nat.stirlingSecond (n - 1) (i - 1) : ℚ) *
          (MetaMathlibExt.signedStirlingFirst i k : ℚ) / i =
      (1 / (n : ℚ)) * (Nat.choose n k : ℚ) * bernoulli (n - k)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Corollary 7.
Uses 1
Statement usesSigned Stirling numbers of the first kind

TheoremBernoulli numbers via Stirling numbers of the second kind#●ready to prove

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

\[B_n = \sum_{i=0}^{n} (-1)^i \, \frac{i!}{i+1} \, S(n, i).\]
theorem_wanted bernoulli_eq_sum_stirlingSecond (n : ℕ) :
    bernoulli n =
      ∑ i ∈ Finset.range (n + 1), (-1 : ℚ) ^ i *
        ((i.factorial : ℚ) / (i + 1)) *
        (Nat.stirlingSecond n i : ℚ)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Corollary 9.

TheoremUnshifted Stirling convolution formula for Bernoulli numbers#●ready to prove

For natural numbers \(k\) and \(n\) with \(1 \le k \le n\), write \(S(m,j)\) for the Stirling numbers of the second kind, \(s(m,j)\) for the signed Stirling numbers of the first kind, and \(B_m\) for the Bernoulli numbers with \(B_1 = -\tfrac12\). Then, in \(\mathbb{Q}\),

\[ \sum_{i=k}^{n} \frac{S(n,i)\, s(i,k)}{i} = \frac{1}{n} \binom{n}{k} B_{n-k} + \delta_{n-1,k}, \]

where \(\delta_{n-1,k}\) is \(1\) if \(k = n - 1\) and \(0\) otherwise.

theorem_wanted sum_stirlingSecond_signed_div_delta (n k : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∑ i ∈ Finset.Icc k n,
        (Nat.stirlingSecond n i : ℚ) *
          (MetaMathlibExt.signedStirlingFirst i k : ℚ) / i =
      (1 / (n : ℚ)) * (Nat.choose n k : ℚ) * bernoulli (n - k) +
        (if n - 1 = k then 1 else 0)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Corollary 10.
Uses 1
Statement usesSigned Stirling numbers of the first kind

TheoremBernoulli numbers of the second kind via Stirling numbers of the first kind#●ready to prove

Let \(B_m^*\) be the Bernoulli numbers of the second kind and \(s(m, j)\) the signed Stirling numbers of the first kind. For every natural number \(n\),

\[B_n^* = \sum_{i=0}^{n} \frac{s(n, i)}{i+1}.\]
theorem_wanted bernoulliSecond_eq_sum (n : ℕ) :
    MetaMathlibExt.bernoulliSecond n =
      ∑ i ∈ Finset.range (n + 1),
        (MetaMathlibExt.signedStirlingFirst n i : ℚ) / (i + 1)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Proposition 11.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind

TheoremShifted Stirling convolution as a Bernoulli number of the second kind#●ready to prove

Let \(s(m, j)\) be the signed Stirling numbers of the first kind, \(S(m, j)\) the Stirling numbers of the second kind and \(B_m^*\) the Bernoulli numbers of the second kind. For all natural numbers \(n\) and \(k\) with \(1 \le k \le n\),

\[\sum_{i=k}^{n} \frac{s(n-1, i-1) \, S(i, k)}{i} = \frac{1}{n} \binom{n}{k} \, B_{n-k}^*.\]
theorem_wanted sum_signed_stirlingSecond_div (n k : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∑ i ∈ Finset.Icc k n,
        (MetaMathlibExt.signedStirlingFirst (n - 1) (i - 1) : ℚ) *
          (Nat.stirlingSecond i k : ℚ) / i =
      (1 / (n : ℚ)) * (Nat.choose n k : ℚ) *
        MetaMathlibExt.bernoulliSecond (n - k)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 13.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind

TheoremStirling convolution as a sum of Bernoulli numbers of the second kind#●ready to prove

Let \(s(m, j)\) be the signed Stirling numbers of the first kind, \(S(m, j)\) the Stirling numbers of the second kind and \(B_m^*\) the Bernoulli numbers of the second kind. For all natural numbers \(n\) and \(k\) with \(1 \le k \le n\),

\[\sum_{i=k}^{n} \frac{s(n, i) \, S(i, k)}{i} = (-1)^{n-k} \, \frac{(n-1)!}{k!} \sum_{l=0}^{n-k} \frac{(-1)^l}{l!} \, B_l^*.\]
theorem_wanted sum_signed_stirlingSecond_div_eq (n k : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∑ i ∈ Finset.Icc k n,
        (MetaMathlibExt.signedStirlingFirst n i : ℚ) *
          (Nat.stirlingSecond i k : ℚ) / i =
      (-1 : ℚ) ^ (n - k) *
        ((n - 1).factorial : ℚ) / k.factorial *
        ∑ l ∈ Finset.range (n - k + 1),
          ((-1 : ℚ) ^ l / l.factorial) * MetaMathlibExt.bernoulliSecond l
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Corollary 15.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind

TheoremWeighted alternating sums of Stirling numbers of the second kind#●ready to prove

For natural numbers \(r \ge 1\) and \(n\), write \(S(n,k)\) for the Stirling numbers of the second kind, \(c(r,j)\) for the unsigned Stirling numbers of the first kind, and \(B_m\) for the Bernoulli numbers with \(B_1 = -\tfrac12\). Then, in \(\mathbb{Q}\),

\[ \sum_{k=0}^{n} (-1)^k \frac{k!}{k+r} S(n,k) = \frac{1}{(r-1)!} \sum_{k=0}^{r-1} c(r,k+1) B_{n+k}. \]
theorem_wanted sum_stirlingSecond_div_add (r n : ℕ)
    (hr : 1 ≤ r) :
    ∑ k ∈ Finset.range (n + 1), (-1 : ℚ) ^ k *
        ((k.factorial : ℚ) / (k + r)) *
        (Nat.stirlingSecond n k : ℚ) =
      (1 / ((r - 1).factorial : ℚ)) *
        ∑ k ∈ Finset.range r,
          (Nat.stirlingFirst r (k + 1) : ℚ) * bernoulli (n + k)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 17.

TheoremSums of signed Stirling numbers of the first kind with shifted reciprocal weights#●ready to prove

Let \(s(m, j)\) be the signed Stirling numbers of the first kind, \(S(m, j)\) the Stirling numbers of the second kind and \(B_m^*\) the Bernoulli numbers of the second kind. Let \(r \ge 1\) and \(n\) be natural numbers, and for \(0 \le k \le r - 1\) set \(\lambda_{r,n,k} = \sum_{l=0}^{r-1-k} \binom{r-1}{l} \, S(r-1-l, k) \, n^l\) (with \(0^0 = 1\)). Then

\[\sum_{k=0}^{n} \frac{s(n, k)}{k + r} = \sum_{k=0}^{r-1} \lambda_{r,n,k} \, B_{n+k}^*.\]
theorem_wanted sum_signed_div_add (r n : ℕ) (hr : 1 ≤ r) :
    ∑ k ∈ Finset.range (n + 1),
        (MetaMathlibExt.signedStirlingFirst n k : ℚ) / (k + r) =
      ∑ k ∈ Finset.range r,
        (∑ l ∈ Finset.range (r - k), (Nat.choose (r - 1) l : ℚ) *
          (Nat.stirlingSecond (r - 1 - l) k : ℚ) * (n : ℚ) ^ l) *
        MetaMathlibExt.bernoulliSecond (n + k)
Sources
  • Bakir Farhi, "Formulas Involving Bernoulli and Stirling Numbers of Both Kinds", Theorem 19.
Uses 2
Statement usesBernoulli numbers of the second kind · Signed Stirling numbers of the first kind
8 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.