feat(Data/Nat/Choose/Multinomial): multinomial coefficients (leanprover-community#35830)

Define the multinomial coefficients, a variant of `Nat.multinomial`.

- redefine `Multiset.multinomial`.
  Given a multiset `m` of natural numbers, `m.multinomial` is the
  multinomial coefficient defined by (m.sum) ! / ∏ i ∈ m, m i !.

As an example, `Multiset.multinomial {1, 2, 2} = 30`.
This is the exponent of $x y^2 z^2$ in $(x+y+z)^5$. 

This should not be confused with the existing `Multiset.multinomial` which gives a different answer,
for example, `Multiset.multinomial {1, 2, 2} = 3`. This function is renamed as `Multiset.countPerms`.

- `Multiset.multinomial_cons` proves that
  `(x ::ₘ m).multinomial = Nat.choose (x + m.sum) x * m.multinomial`

- `Multiset.multinomial_add` proves that
  `(m + m').multinomial = Nat.choose (m + m').sum m.sum * m.multinomial * m'.multinomial`

co-authored with @mariainesdff

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: 3 people

Mathlib/Data/List/ToFinsupp.lean

@@ -67,6 +67,10 @@ theorem toFinsupp_support :
     l.toFinsupp.support = {i ∈ Finset.range l.length | getD l i 0 ≠ 0} :=
   rfl
 
+lemma toFinsupp_support_subset :
+    l.toFinsupp.support ⊆ Finset.range l.length := by
+  simp [List.toFinsupp_support]
+
 theorem toFinsupp_apply_lt (hn : n < l.length) : l.toFinsupp n = l[n] :=
   getD_eq_getElem _ _ hn
 

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -7,10 +7,10 @@ module
 
 public import Mathlib.Algebra.Order.Antidiag.Pi
 public import Mathlib.Data.Finsupp.Multiset
+public import Mathlib.Data.List.ToFinsupp
 public import Mathlib.Data.Nat.Choose.Sum
 public import Mathlib.Data.Nat.Factorial.BigOperators
 public import Mathlib.Data.Nat.Factorial.DoubleFactorial
-
 /-!
 # Multinomial
 
@@ -27,6 +27,29 @@ This file defines the multinomial coefficients and several small lemmas for mani
 
 - `Finset.sum_pow`: The expansion of `(s.sum x) ^ n` using multinomial coefficients
 
+- `Multiset.multinomial`.
+  Given a multiset `m` of natural numbers, `m.multinomial` is the
+  multinomial coefficient defined by `(m.sum) ! / ∏ i ∈ m, m i !`.
+
+This should not be confused with `m.countPerms` which
+is defined as `m.toFinsupp.multinomial`.
+
+As an example, one has `Multiset.multinomial {1, 2, 2} = 30`,
+while `Multiset.countPerms {1, 2, 2} = 3`.
+
+- `Multiset.multinomial_cons` proves that
+  `(x ::ₘ m).multinomial = Nat.choose (x + m.sum) x * m.multinomial`
+- `Multiset.multinomial_add` proves that
+  `(m + m').multinomial = Nat.choose (m + m').sum m.sum * m.multinomial * m'.multinomial`
+
+## Implementation note for `Multiset.multinomial`.
+
+To avoid the definition of `Multiset.multinomial` as a quotient given above,
+we define it in terms of `Finsupp.multinomial`, via lists:
+If `m : Multiset ℕ` is the multiset associated with a list `l : List ℕ`,
+then `m.multinomial = l.toFinsupp.multinomial`.
+Then we prove its invariance under permutation.
+
 -/
 
 @[expose] public section
@@ -385,3 +408,97 @@ theorem Finsupp.multinomial_of_support_subset {σ : Type*} {d : σ →₀ ℕ} {
   rw [Nat.multinomial, Finsupp.multinomial,
     sum_of_support_subset _ h _ (by simp), prod_of_support_subset _ h _ (by simp)]
   simp
+
+namespace List
+
+open Nat
+
+lemma toFinsupp_sum {α : Type*} [AddCommMonoid α] [DecidableEq α] (l : List α) :
+    l.toFinsupp.sum (fun _ a ↦ a) = l.sum := by
+  match l with
+  | nil => simp
+  | x :: l =>
+    simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]
+    rw [Finsupp.sum_add_index (by simp) (by simp)]
+    simp [Finsupp.sum_embDomain, l.toFinsupp_sum]
+
+/-- The multinomial coefficients given by a list of natural numbers.
+
+See also `Multiset.multinomial` -/
+abbrev multinomial (l : List ℕ) : ℕ := l.toFinsupp.multinomial
+
+theorem multinomial_cons (x : ℕ) (l : List ℕ) :
+    (x :: l).multinomial = Nat.choose (x + l.sum) x * l.multinomial := by
+  simp only [multinomial]
+  rw [Finsupp.multinomial_update 0 (x :: l).toFinsupp]
+  congr 1
+  · congr
+    exact List.toFinsupp_sum (x :: l)
+  let succEmb : ℕ ↪ ℕ :=  { toFun := Nat.succ, inj' := Nat.succ_injective }
+  simp only [toFinsupp_cons_eq_single_add_embDomain, Finsupp.multinomial_eq]
+  have : (Finsupp.single 0 x + l.toFinsupp.embDomain succEmb).update 0 0 =
+    (l.toFinsupp.embDomain succEmb).update 0 0 := by
+    ext i
+    by_cases hi : i = 0
+    · simp [hi]
+    · simp [Finsupp.update_apply, if_neg hi, Finsupp.single_eq_of_ne hi]
+  have h (x) : (l.toFinsupp.embDomain succEmb) (x + 1) = l[x]?.getD 0 := by
+    rw [Finsupp.embDomain_apply, dif_pos ⟨x, by simp [succEmb]⟩]
+    simp [succEmb]
+  simp [succEmb, this, Nat.multinomial, h]
+
+end List
+
+namespace Multiset
+
+/-- The `multinomial` coefficients on `Multiset ℕ`. -/
+def multinomial (m : Multiset ℕ) : ℕ := Quot.liftOn m List.multinomial <| fun l l' h ↦ by
+  induction h with
+  | nil => simp
+  | @cons x l l' hl hl' => simp [List.multinomial_cons, hl', hl.sum_nat]
+  | @swap x y l =>
+    simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]
+    rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]
+    rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]
+    simp [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left]
+  | @trans l l' l'' h h' ih ih' => rw [ih, ih']
+
+theorem multinomial_cons (x : ℕ) (m : Multiset ℕ) :
+    (x ::ₘ m).multinomial = Nat.choose (x + m.sum) x * m.multinomial := by
+  obtain ⟨l, rfl⟩ := Quotient.exists_rep m
+  exact List.multinomial_cons x l
+
+@[simp]
+theorem multinomial_zero : Multiset.multinomial 0 = 1 := rfl
+
+@[simp]
+theorem multinomial_singleton (n : ℕ) :
+    Multiset.multinomial {n} = 1 := by
+  simp [← cons_zero, multinomial_cons]
+
+theorem multinomial_add (m m' : Multiset ℕ) :
+    (m + m').multinomial = Nat.choose (m + m').sum m.sum * m.multinomial * m'.multinomial := by
+  induction m using Multiset.induction_on with
+  | empty => simp
+  | cons x m hind =>
+    simp only [cons_add, sum_cons, sum_add, multinomial_cons, hind, ← mul_assoc]
+    congr 2
+    rw [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left, eq_comm,
+      Nat.choose_mul (Nat.le_add_right _ _), ← Nat.choose_symm (Nat.le_add_right x _)]
+    simp [add_tsub_cancel_left]
+
+theorem multinomial_nsmul (k : ℕ) (m : Multiset ℕ) :
+    (k • m).multinomial = Nat.multinomial (Finset.range k) (fun _ ↦ m.sum) * m.multinomial ^ k := by
+  induction k with
+  | zero => simp
+  | succ k hk =>
+    rw [succ_nsmul', multinomial_add, hk, Finset.range_add_one,
+      Nat.multinomial_insert (by simp), sum_add, sum_nsmul, pow_succ']
+    simp [smul_eq_mul, Finset.sum_const, Finset.card_range]
+    ring
+
+theorem multinomial_nsmul_singleton (k n : ℕ) :
+    (k • {n} : Multiset ℕ).multinomial = Nat.multinomial (Finset.range k) (fun _ ↦ n) := by
+  simp [multinomial_nsmul]
+
+end Multiset