## Stream: Is there code for X?

### Topic: Multinomial Theorem

#### Marco David (Dec 06 2022 at 10:49):

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

#### Manuel Eberl (Dec 06 2022 at 10:58):

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

Alright, thanks.

#### Manuel Eberl (Dec 06 2022 at 11:03):

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)"
``````

#### Manuel Eberl (Dec 06 2022 at 11:03):

A direct proof is probably also possible by constructing a bijection

#### Yong Kiam (Jun 22 2023 at 02:52):

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
next
case (Cons k ks)
then show ?case
apply auto
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
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}"
have 2:"ys ∈ (#) y ` {ks. length ks = x ∧ sum_list ks = sum_list ys - y}"
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 (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)
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: Dec 07 2023 at 16:21 UTC