Stirling numbers of the second kind

TheoremAddition formula for Stirling numbers of the second kind#✓fully proved

Write \(S(n,k)\) for the Stirling numbers of the second kind. For all natural numbers \(u\), \(v\) and \(k\) with \(u > 0\),

\[S(u+v,k) = \sum_{n=1}^{k} S(u,n) \sum_{m=k-n}^{v} \binom{v}{m} S(m,k-n)\, n^{v-m},\]

where an inner sum with \(k - n > v\) is empty.

The source does not state the hypothesis \(u > 0\), but the formula needs it: for \(u = 0\) and \(v = k = 1\) the left side is \(S(1,1) = 1\), while every term on the right has the factor \(S(0,1) = 0\).

theorem stirlingSecond_addition
    (u v k : ℕ) (hu : 0 < u) :
    Nat.stirlingSecond (u + v) k =
      ∑ n ∈ Finset.Icc 1 k, Nat.stirlingSecond u n *
        ∑ m ∈ Finset.Icc (k - n) v,
          Nat.choose v m * Nat.stirlingSecond m (k - n) * n ^ (v - m)

Sources

• Grzegorz Rządkowski, "Two Formulas for Successive Derivatives and Their Applications," Journal of Integer Sequences 12 (2009), Article 09.8.2, Theorem, equation (ex33), lines 198–204, https://cs.uwaterloo.ca/journals/JIS/VOL12/Rzadkowski/rzadkowski3.tex

TheoremExplicit formula for Stirling numbers of the second kind#✓fully proved

Write \(S(t,k)\) for the Stirling numbers of the second kind. For all natural numbers \(t\) and \(k\),

\[k!\, S(t,k) = \sum_{j=0}^{k} (-1)^{k-j} \binom{k}{j}\, j^t,\]

with the convention \(0^0 = 1\).

public theorem stirlingSecond_mul_factorial_eq_sum (t k : ℕ) :
    (Nat.stirlingSecond t k : ℝ) * (k.factorial : ℝ) =
      ∑ j ∈ Finset.range (k + 1),
        (-1 : ℝ) ^ (k - j) * (Nat.choose k j : ℝ) * (j : ℝ) ^ t

Sources

• R. L. Graham, D. E. Knuth, and O. Patashnik, Concrete Mathematics, 2nd ed., Section 6.1.

Used by 4

Used byStirling numbers of the second kind with three blocks · Hankel determinants of the shifted Eulerian polynomials · Laguerre–Stirling–Bell connection pair · Exponential generating function of a shifted Stirling column

TheoremExponential generating function of a shifted Stirling column#✓fully proved

Write \(S(n,k)\) for the Stirling numbers of the second kind. For every natural number \(j\) and every real number \(x\), the series

\[\sum_{n=0}^{\infty} S(n+1,j+1)\, \frac{x^n}{n!}\]

converges unconditionally to \(e^x (e^x - 1)^j / j!\).

public theorem hasSum_stirlingSecond_succ_egf (j : ℕ) (x : ℝ) :
    HasSum
      (fun n : ℕ =>
        (Nat.stirlingSecond (n + 1) (j + 1) : ℝ) * (x ^ n / n.factorial))
      (Real.exp x * (Real.exp x - 1) ^ j / j.factorial)

Sources

• R. L. Graham, D. E. Knuth, and O. Patashnik, Concrete Mathematics, 2nd ed., Section 7.6 (the column generating function (e^x - 1)^(j+1)/(j+1)!, differentiated).

Uses 1 · Used by 1

Proof usesExplicit formula for Stirling numbers of the second kind

Used byGenerating function of negative-index poly-Bernoulli numbers

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.