Bell numbers for multisets

For n : ℕ, the nth Bell number is the number of partitions of a set of cardinality n. Here, we define a refinement of these numbers, that count, for any m : Multiset ℕ, the number of partitions of a set of cardinality m.sum whose parts have cardinalities given by m.

The definition presents it as a natural number.

• Multiset.bell: number of partitions of a set whose parts have cardinalities a given multiset

• Nat.uniformBell m n : short name for Multiset.bell (replicate m n)

• Multiset.bell_mul_eq shows that m.bell * (m.map (fun j ↦ j !)).prod * Π j ∈ (m.toFinset.erase 0), (m.count j)! = m.sum !

• Nat.uniformBell_mul_eq shows that uniformBell m n * n ! ^ m * m ! = (m * n)!

• Nat.uniformBell_succ_left computes Nat.uniformBell (m + 1) n from Nat.uniformBell m n

TODO

Prove that it actually counts the number of partitions as indicated. (When m contains 0, the result requires to admit repetitions of the empty set as a part.)

def Multiset.bell (m : Multiset ℕ) : ℕ

Number of partitions of a set of cardinality m.sum whose parts have cardinalities given by m

@[simp]

theorem Multiset.bell_zero : bell 0 = 1

theorem Multiset.bell_mul_eq (m : Multiset ℕ) : m.bell * (map (fun (j : ℕ) => j.factorial) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m).factorial = m.sum.factorial

theorem Multiset.bell_eq (m : Multiset ℕ) : m.bell = m.sum.factorial / ((map (fun (j : ℕ) => j.factorial) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m).factorial)

def Nat.uniformBell (m n : ℕ) : ℕ

Number of possibilities of dividing a set with m * n elements into m groups of n-element subsets.

theorem Nat.uniformBell_eq (m n : ℕ) : m.uniformBell n = ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

theorem Nat.uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1

theorem Nat.uniformBell_zero_right (m : ℕ) : m.uniformBell 0 = 1

theorem Nat.uniformBell_succ_left (m n : ℕ) : (m + 1).uniformBell n = (m * n + n - 1).choose (n - 1) * m.uniformBell n

theorem Nat.uniformBell_one_left (n : ℕ) : uniformBell 1 n = 1

theorem Nat.uniformBell_one_right (m : ℕ) : m.uniformBell 1 = 1

theorem Nat.uniformBell_mul_eq (m : ℕ) {n : ℕ} (hn : n ≠ 0) : m.uniformBell n * n.factorial ^ m * m.factorial = (m * n).factorial

theorem Nat.uniformBell_eq_div (m : ℕ) {n : ℕ} (hn : n ≠ 0) : m.uniformBell n = (m * n).factorial / (n.factorial ^ m * m.factorial)