Stirling expansions of the Akiyama–Tanigawa algorithm

TheoremChen's Stirling expansion#✓fully proved

Let \(a(m, s)\), for natural numbers \(m\) and \(s\), be real numbers satisfying \(a(m, s + 1) = m \, a(m, s) - (m + 1) \, a(m + 1, s)\) for all \(m\) and \(s\). Then for every natural number \(t\),

\[a(0, t) = \sum_{m=0}^{t} (-1)^m \, m! \, S(t, m) \, a(m, 0),\]

where \(S(t, m)\) is the Stirling number of the second kind.

This recurrence is a variant of the Akiyama–Tanigawa algorithm.

public theorem chen_stirlingSecond_expansion (t : ℕ) :
    ∀ (a : ℕ → ℕ → ℝ),
      (∀ (m s : ℕ),
        a m (s + 1) = (m : ℝ) * a m s - ((m : ℝ) + 1) * a (m + 1) s) →
      a 0 t = ∑ m ∈ Finset.range (t + 1),
        (-1 : ℝ) ^ m * (Nat.factorial m : ℝ) *
          (Nat.stirlingSecond t m : ℝ) * a m 0

Sources

• K.-W. Chen, "Algorithms for Bernoulli numbers and Euler numbers," Journal of Integer Sequences 4 (2001), Article 01.1.6, as stated in Dil, Kurt, and Cenkci (2007), Proposition 4. It is the x = 0 case of poly_initial_expansion.

Used by 1

Used byExpansion by generalized Stirling numbers of the second kind

TheoremExpansion by generalized Stirling numbers of the second kind#✓fully proved

For every natural number \(n\), every real number \(x\) and all real numbers \(a(m, t)\), indexed by natural numbers \(m\) and \(t\), such that \(a(m, t + 1) = m\,a(m, t) - (m + 1)\,a(m + 1, t)\) for all \(m\) and \(t\), writing \({n \brace m}_x\) for the generalized Stirling numbers of the second kind,

\[\sum_{k=0}^{n} \binom{n}{k} x^k a(0, n - k) = \sum_{m=0}^{n} (-1)^m m! {n \brace m}_x a(m, 0).\]

public theorem poly_initial_expansion : ∀ (n : ℕ) (x : ℝ) (a : ℕ → ℕ → ℝ)
    (hrec : ∀ (m t : ℕ),
      a m (t + 1) = (m : ℝ) * a m t - ((m : ℝ) + 1) * a (m + 1) t),
    ∑ k ∈ Finset.range (n + 1), (Nat.choose n k : ℝ) * x ^ k * a 0 (n - k) =
      ∑ m ∈ Finset.range (n + 1), (-1 : ℝ) ^ m * (Nat.factorial m : ℝ) *
        (generalizedStirlingSecond n m x) * a m 0

Sources

• Ayhan Dil, Veli Kurt, and Mehmet Cenkci, "Algorithms for Bernoulli and Related Polynomials," Journal of Integer Sequences 10 (2007), Article 07.5.4, Proposition 5, lines 661–671, https://cs.uwaterloo.ca/journals/JIS/VOL10/Dil/dil11.tex

Uses 2

Statement usesGeneralized Stirling numbers of the second kind

Proof usesChen's Stirling expansion

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.