Associated Stirling numbers of the second kind

Definition2-associated Stirling numbers of the second kind#✓fully proved

For natural numbers \(n\) and \(k\), the 2-associated Stirling number of the second kind is the integer \(S_2(n, k) = \sum_{j=0}^{k} (-1)^j \binom{n}{j} S(n - j, k - j)\), where \(S\) denotes the Stirling numbers of the second kind.

By inclusion and exclusion over singleton blocks, \(S_2(n, k)\) is the number of partitions of an \(n\)-element set into \(k\) blocks, each containing at least two elements.

def twoAssocStirlingSecond (n k : ℕ) : ℤ :=
  ∑ j ∈ Finset.range (k + 1), ((-1 : ℤ) ^ j) * (Nat.choose n j : ℤ) *
      (Nat.stirlingSecond (n - j) (k - j) : ℤ)
Used by 8

TheoremRecurrence for 2-associated Stirling numbers of the second kind#✓fully proved

Write \(S_2(n, k)\) for the 2-associated Stirling number of the second kind. For natural numbers \(m\) and \(k\) with \(1 \le k \le m\), we have \(S_2(m + 2, k) = k \, S_2(m + 1, k) + (m + 1) \, S_2(m, k - 1)\).

theorem twoAssocStirlingSecond_recurrence (m k : ℕ) (hk : 1 ≤ k) (hkm : k ≤ m) :
    twoAssocStirlingSecond (m + 2) k =
      (k : ℤ) * twoAssocStirlingSecond (m + 1) k +
        (m + 1 : ℤ) * twoAssocStirlingSecond m (k - 1)
Uses 1 · Used by 1

TheoremVanishing of 2-associated Stirling numbers of the second kind#✓fully proved

For natural numbers \(n\) and \(k\) with \(n < 2k\), the 2-associated Stirling number of the second kind \(S_2(n, k)\) equals \(0\).

theorem twoAssocStirlingSecond_eq_zero_of_lt_two_mul (n k : ℕ) (hnk : n < 2 * k) :
    twoAssocStirlingSecond n k = 0
Uses 2 · Used by 1
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.