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)
def twoAssocStirlingSecond (n k : ℕ) : ℤ :=
∑ j ∈ Finset.range (k + 1), ((-1 : ℤ) ^ j) * (Nat.choose n j : ℤ) *
(Nat.stirlingSecond (n - j) (k - j) : ℤ)
MathlibExt/Combinatorics/AssociatedStirlingSecond.lean:30
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
def twoAssocStirlingSecond (n k : ℕ) : ℤ :=
∑ j ∈ Finset.range (k + 1), ((-1 : ℤ) ^ j) * (Nat.choose n j : ℤ) *
(Nat.stirlingSecond (n - j) (k - j) : ℤ)
MathlibExt/Combinatorics/AssociatedStirlingSecond.lean:30
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.