Spivey's Bell number formula

TheoremSpivey's Bell number formula#✓fully proved

For all natural numbers \(m\) and \(n\),

\[B_{n+m} = \sum_{j=0}^{m} \sum_{k=0}^{n} j^{n-k} \, S(m, j) \binom{n}{k} B_k,\]

where \(B_k\) is the \(k\)-th Bell number, \(S(m, j)\) is the Stirling number of the second kind, and \(0^0 = 1\).

theorem spivey_bell_number_add (m n : ℕ) : (n + m).bell = ∑ j ∈ Finset.range (m + 1), ∑ k ∈
  Finset.range (n + 1), j ^ (n - k) * m.stirlingSecond j * n.choose k * k.bell
Sources
Used by 1
Used bySpivey's recurrence for Bell numbers

TheoremSpivey's recurrence for Bell numbers#✓fully proved

For all natural numbers \(n\) and \(m\),

\[B_{n+m} = \sum_{k=0}^{n} \sum_{j=0}^{m} j^{n-k} \, S(m, j) \binom{n}{k} B_k,\]

where \(B_k\) is the \(k\)-th Bell number, \(S(m, j)\) is the Stirling number of the second kind, and \(0^0 = 1\). This is Spivey's Bell number formula with the two finite sums interchanged.

theorem spivey_bell_recurrence (n m : ℕ) :
    Nat.bell (n + m) =
      ∑ k ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (m + 1),
        j ^ (n - k) * Nat.stirlingSecond m j * Nat.choose n k * Nat.bell k
Sources
  • Jacob Katriel, "On a Generalized Recurrence for Bell Numbers", Journal of Integer Sequences 11 (2008), Article 08.3.8, equation (Spivey), lines 77–81, https://cs.uwaterloo.ca/journals/JIS/VOL11/Katriel/katriel6.tex (quoting Michael Z. Spivey, "A generalized recurrence for Bell numbers", Journal of Integer Sequences 11 (2008), Article 08.2.5).
Uses 1
Proof usesSpivey's Bell number formula

TheoremThe (p, q)-deformed Spivey formula#✓fully proved

Let \(p\) and \(q\) be real numbers with \(0 < q < p \le 1\), and for \(k \in \mathbb{N}\) put \([k] = (p^k - q^k)/(p - q)\). Define real numbers \(S(n, k)\) for \(n, k \in \mathbb{N}\) by \(S(0, 0) = 1\), \(S(0, k) = 0\) for \(k \ge 1\), \(S(n + 1, 0) = 0\), and, for \(k \ge 1\), \(S(n + 1, k) = p^{n + 1 - k} q^{k - 1} S(n, k - 1) + [k] \, S(n, k)\), where the exponent \(n + 1 - k\) is read as \(0\) when \(k > n + 1\). Put \(\tilde S(n, k) = p^{\binom{k}{2}} S(n, k)\) and \(\tilde B_n(x) = \sum_{k=0}^{n} \tilde S(n, k) \, x^k\) for real \(x\). Then for all \(m, n \in \mathbb{N}\),

\[\tilde B_{n+m}(1) = \sum_{k=0}^{m} \sum_{j=0}^{n} \binom{n}{j} \tilde S(m, k) \, [k]^{n-j} \, q^{jk} \, \tilde B_j\bigl(p^{n+m-j}\bigr),\]

with \(0^0 = 1\).

Proof: We formalize the operator proof around equations eq1, eq2', eq4, meq, pqexpn, and lasteq in Oussi's paper, using formal power series in place of convergent series.

public theorem spivey_pq_bell :
  ∀ (p q : ℝ) (hq0 : 0 < q) (hqp : q < p) (hp1 : p ≤ 1),
    let bracket : ℕ → ℝ := fun k => (p ^ k - q ^ k) / (p - q);
    let rec S : ℕ → ℕ → ℝ
Sources
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.