Have multinomial coefficients and the multinomial theorem been formalized in Isabelle/HOL?

I don't think so, but it should be very easy. Just an induction using the binomial theorem in each step.

Alright, thanks.

Most natural way to state it would probably be like this (using `HOL-Library.FuncSet`

):

```
lemma multinomial:
"card {f∈A →⇩E B. ∀x∈B. card (f -` {x} ∩ A) = h x} * (∏x∈B. fact (h x)) =
fact (card A)"
```

A direct proof is probably also possible by constructing a bijection

in case it's helpful for anyone in the future, here's my version of it (sorry for the lateness as I just joined this Zulip chat)

```
lemma finite_card_fixed_length_lists:
assumes "finite X"
shows
"finite {ls. length ls = n ∧ set ls ⊆ X}"
"card {ls. length ls = n ∧ set ls ⊆ X} = card X ^ n"
proof -
obtain xs where "X = set xs"
using assms finite_list by blast
show "finite {ls. length ls = n ∧ set ls ⊆ X}"
by (smt (verit) Collect_mono_iff assms finite_lists_length_eq rev_finite_subset)
show "card {ls. length ls = n ∧ set ls ⊆ X} = card X ^ n"
by (metis (no_types, lifting) Collect_cong assms card_lists_length_eq)
qed
(* Multinomial coefficient:
this definition makes it slightly easier to prove the
multinomial theorem
*)
definition multinomial :: "nat ⇒ nat list ⇒ nat" (infixl "mchoose" 65)
where "n mchoose ks =
fact n div prod_list (map fact ks)"
lemma prod_list_dvd_fact_sum_list:
shows "prod_list (map fact ks) dvd fact (sum_list ks)"
proof (induction ks)
case Nil
then show ?case
by (auto simp add: dvd_def)
next
case (Cons k ks)
then show ?case
apply auto
by (smt (verit) add_diff_cancel_left' binomial_fact_lemma dvd_def le_add1 mult.assoc of_nat_fact of_nat_mult)
qed
lemma multinomial_dvd:
assumes "sum_list ks ≤ n"
shows "prod_list (map fact ks) dvd fact n"
by (metis assms binomial_fact_lemma dvd_def mult.assoc of_nat_fact of_nat_mult prod_list_dvd_fact_sum_list)
lemma finite_sum_list_eq:
"finite {ks. length ks = x ∧ sum_list ks = (y::nat)}"
proof -
have *: "{ks. length ks = x ∧ sum_list ks = (y::nat)} ⊆
{ks. length ks = x ∧ set ks ⊆ {0..y}}"
apply auto
by (simp add: member_le_sum_list)
have "finite {ks. length ks = x ∧ set ks ⊆ {0..y}}"
using finite_card_fixed_length_lists
by blast
thus ?thesis using *
by (meson rev_finite_subset)
qed
lemma sum_split_k:
shows "sum f {ks. length ks = Suc x ∧ sum_list ks = n} =
(∑k≤n. sum (λks. f ((k::nat) # ks)) {ks. length ks = x ∧ sum_list ks = n - k})"
proof -
have *: "{ks. length ks = Suc x ∧ sum_list ks = n} =
(⋃k≤n.
(λks. k # ks) `
{ks. length ks = x ∧ sum_list ks = n - k})"
apply auto
proof -
fix ys
assume ys: "length ys = Suc x" "n = sum_list ys"
then obtain y yss where y: "ys = y # yss"
by (metis Suc_length_conv)
have "y + sum_list yss = n" using ys y by auto
then have 1:"y ∈ {..sum_list ys}"
by (simp add: ys(2))
have 2:"ys ∈ (#) y ` {ks. length ks = x ∧ sum_list ks = sum_list ys - y}"
apply (auto simp add: image_def)
using y ys(1) by fastforce
thus "∃xb∈{..sum_list ys}.
ys ∈ (#) xb `
{ks.
length ks = x ∧
sum_list ks = sum_list ys - xb}"
using 1 2 by blast
qed
have f: "finite {ks. length ks = x ∧ sum_list ks = (y::nat)}" for y
using finite_sum_list_eq by auto
show ?thesis
unfolding *
apply (subst sum.UNION_disjoint)
apply (auto simp add: f)
apply (subst sum.reindex)
by auto
qed
lemma cross_multiply:
assumes "a dvd c"
assumes "d dvd (a::nat)"
shows "a div d * c div a = c div d"
using assms(1) assms(2) by fastforce
lemma mchoose_cons:
assumes "sum_list (k # ks) ≤ n"
shows "(n mchoose (k # ks)) =
(n-k mchoose ks) * (n choose k)"
proof -
have *: "fact n div fact k = fact (n - k) * (n choose k)"
by (metis (no_types, lifting) assms binomial_fact_lemma fact_nonzero le_add1 le_eq_less_or_eq mult.assoc nonzero_mult_div_cancel_left order_le_less_trans sum_list_simps(2))
have "n mchoose (k # ks) =
fact n div prod_list (map fact (k # ks))"
unfolding multinomial_def by auto
moreover have "... = (fact n div fact k) div prod_list (map fact ks)"
apply simp
by (metis div_mult2_eq)
moreover have "... = (fact (n - k) * (n choose k)) div prod_list (map fact ks)"
using * by auto
moreover have "... = (fact (n - k) div prod_list (map fact ks)) * (n choose k)"
by (metis add_le_cancel_left assms binomial_eq_0 bits_div_0 div_mult_swap le_add_diff_inverse linorder_not_less mult.commute mult_zero_left multinomial_dvd sum_list.Cons)
ultimately show ?thesis
using multinomial_def by presburger
qed
theorem multinomial_theorem:
shows "(sum_list (xs::nat list)) ^ n =
sum (λks. (n mchoose ks) * prod_list (map2 (^) xs ks))
{ks. length ks = length xs ∧ sum_list ks = n}"
proof (induction xs arbitrary: n)
case Nil
have *: "{ks. ks = [] ∧ (∀n∈set ks. n = 0)} = {[]}"
by auto
show ?case
apply (cases n)
by (auto simp add:multinomial_def *)
next
case (Cons x xs)
(* rhs *)
have "(∑ks | length ks = Suc (length xs) ∧
sum_list ks = n.
(n mchoose ks) *
prod_list (map2 (^) (x # xs) ks)) =
(∑k≤n.
∑ks | length ks = length xs ∧
sum_list ks = n - k.
(n mchoose (k # ks)) *
prod_list (map2 (^) (x # xs) (k # ks)))"
unfolding sum_split_k by auto
moreover have "... =
(∑k≤n.
sum (λks.
((n-k mchoose ks) * (n choose k)) *
(x ^ k * prod_list (map2 (^) xs ks)))
{ks. length ks = length xs ∧ sum_list ks = n - k})"
by (auto intro!: sum.cong simp add: mchoose_cons)
moreover have "... =
(∑k≤n.
(n choose k) * x ^ k *
sum (λks.
(n-k mchoose ks) *
prod_list (map2 (^) xs ks))
{ks. length ks = length xs ∧ sum_list ks = n - k})"
by (smt (z3) mult.assoc mult.left_commute sum.cong sum_distrib_left)
moreover have "... =
(∑k≤n.
of_nat (n choose k) * x ^ k *
sum_list xs ^ (n - k))"
using Cons
using of_nat_id by presburger
moreover
have "... = (x + sum_list xs) ^ n "
unfolding binomial by auto
ultimately show ?case
by auto
qed
```

Last updated: Feb 27 2024 at 08:17 UTC