Stirling Numbers

This file defines Stirling numbers of the first and second kinds, proves their fundamental recurrence relations, and establishes some of their key properties and identities.

The Stirling numbers of the first kind

The unsigned Stirling numbers of the first kind, represent the number of ways to partition n distinct elements into k non-empty cycles.

The Stirling numbers of the second kind

The Stirling numbers of the second kind, represent the number of ways to partition n distinct elements into k non-empty subsets.

Main definitions

• Nat.stirlingFirst: the number of ways to partition n distinct elements into k non-empty cycles, defined by the recursive relationship it satisfies.
• Nat.stirlingSecond: the number of ways to partition n distinct elements into k non-empty subsets, defined by the recursive relationship it satisfies.

Main results

• Nat.pow_eq_sum_stirlingSecond_mul_descFactorial: every power n ^ k is a linear combination of the descending factorials Nat.descFactorial with the Stirling numbers of the second kind as coefficients.

References

• [Knuth, The Art of Computer Programming, Volume 1, §1.2.6][knuth1997]

def Nat.stirlingFirst : ℕ → ℕ → ℕ

Nat.stirlingFirst n k is the (unsigned) Stirling number of the first kind, counting the number of permutations of n elements with exactly k disjoint cycles.

Equations

• Nat.stirlingFirst 0 0 = 1
• Nat.stirlingFirst 0 n.succ = 0
• n.succ.stirlingFirst 0 = 0
• n.succ.stirlingFirst k.succ = n * n.stirlingFirst (k + 1) + n.stirlingFirst k

@[simp]

theorem Nat.stirlingFirst_zero : stirlingFirst 0 0 = 1

@[simp]

theorem Nat.stirlingFirst_zero_succ (k : ℕ) : stirlingFirst 0 k.succ = 0

@[simp]

theorem Nat.stirlingFirst_succ_zero (n : ℕ) : n.succ.stirlingFirst 0 = 0

theorem Nat.stirlingFirst_succ_left (n k : ℕ) (hk : k ≠ 0) : (n + 1).stirlingFirst k = n * n.stirlingFirst k + n.stirlingFirst (k - 1)

theorem Nat.stirlingFirst_succ_right (n k : ℕ) (hn : n ≠ 0) : n.stirlingFirst (k + 1) = (n - 1) * (n - 1).stirlingFirst (k + 1) + (n - 1).stirlingFirst k

theorem Nat.stirlingFirst_succ_succ (n k : ℕ) : (n + 1).stirlingFirst (k + 1) = n * n.stirlingFirst (k + 1) + n.stirlingFirst k

theorem Nat.stirlingFirst_eq_zero_of_lt {n k : ℕ} : n < k → n.stirlingFirst k = 0

theorem Nat.stirlingFirst_self (n : ℕ) : n.stirlingFirst n = 1

theorem Nat.stirlingFirst_succ_self_left (n : ℕ) : (n + 1).stirlingFirst n = (n + 1).choose 2

theorem Nat.stirlingFirst_one_right (n : ℕ) : (n + 1).stirlingFirst 1 = n.factorial

def Nat.stirlingSecond : ℕ → ℕ → ℕ

Nat.stirlingSecond n k is the Stirling number of the second kind, counting the number of ways to partition a set of n elements into k nonempty subsets.

Equations

• Nat.stirlingSecond 0 0 = 1
• Nat.stirlingSecond 0 n.succ = 0
• n.succ.stirlingSecond 0 = 0
• n.succ.stirlingSecond k.succ = (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k

@[simp]

theorem Nat.stirlingSecond_zero : stirlingSecond 0 0 = 1

@[simp]

theorem Nat.stirlingSecond_zero_succ (k : ℕ) : stirlingSecond 0 k.succ = 0

@[simp]

theorem Nat.stirlingSecond_succ_zero (n : ℕ) : n.succ.stirlingSecond 0 = 0

theorem Nat.stirlingSecond_succ_left (n k : ℕ) (hk : k ≠ 0) : (n + 1).stirlingSecond k = k * n.stirlingSecond k + n.stirlingSecond (k - 1)

theorem Nat.stirlingSecond_succ_right (n k : ℕ) (hn : n ≠ 0) : n.stirlingSecond (k + 1) = (k + 1) * (n - 1).stirlingSecond (k + 1) + (n - 1).stirlingSecond k

theorem Nat.stirlingSecond_succ_succ (n k : ℕ) : (n + 1).stirlingSecond (k + 1) = (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k

theorem Nat.stirlingSecond_eq_zero_of_lt {n k : ℕ} : n < k → n.stirlingSecond k = 0

theorem Nat.stirlingSecond_self (n : ℕ) : n.stirlingSecond n = 1

theorem Nat.stirlingSecond_one_right (n : ℕ) : (n + 1).stirlingSecond 1 = 1

theorem Nat.stirlingSecond_succ_self_left (n : ℕ) : (n + 1).stirlingSecond n = (n + 1).choose 2

theorem Nat.pow_eq_sum_stirlingSecond_mul_descFactorial (n k : ℕ) : n ^ k = ∑ j ∈ Finset.range (k + 1), k.stirlingSecond j * n.descFactorial j

Every power n ^ k is a linear combination of the descending factorials n.descFactorial j with the Stirling numbers of the second kind stirlingSecond k j as coefficients.