Multinomial coefficients definition

Stream: new members

[Pim Otte]

Below a definition for multinomial coefficients with the multiplicative defintion (rather than the recursive one)

A general question of "Does this look okay?" as well as the more specific:

Is the convention to use a finsupp because any function from \alpha would be finsupp, or is the convention to use something else (function, fun_like?), because it would automatically be finsupp?

import data.finsupp.basic

open nat

open_locale big_operators

noncomputable theory

def multinomial (α : Type*) [fintype α] [has_le α] : (ℕ) → (α →₀ ℕ) → ℕ :=  λ n, (λ (k : α →₀ ℕ), (factorial n)*∏ i, choose (∑ j in {j' ∈ fintype.elems α | j' ≤ i}, (k j)) (k i))

[Pim Otte]

I actually switched to function since I managed to make that work first with the defintion of the multinomial theorem I was trying to formulate.

Does the following look okay? The main thing I'm kind of doubting are the explicit coercions.

import data.finsupp.basic

open nat

open_locale big_operators

noncomputable theory

def multinomial {α : Type*} [fintype α] [has_le α] : (ℕ) → (α → ℕ) → ℕ :=  λ n, (λ (k : α → ℕ), (factorial n)*∏ i, choose (∑ j in {j' ∈ fintype.elems α | j' ≤ i}, (k j)) (k i))


def multinomial_theorem (α : Type*) [fintype α]  [decidable_eq α] [has_le α] {R : Type*} [comm_ring R] (x: α →₀ R) (n : ℕ) : (∑ i, x i)^n = ∑ k : α → (fin (n+1)), ite ((∑ i, k i) = n) (comm_ring.nat_cast (multinomial n (λ i, fin.coe_embedding (n+1) (k i)))*(∏ i, (x i)^(fin.coe_embedding (n+1) (k i)))) 0 :=
begin
  sorry,
end

[Junyan Xu]

There are several problems with this definition:

1. I think factorial n shouldn't be there, and the argument n is not necessary.
2. This definition of multinomial only works with [linear_order α]; has_le is insufficient. You may take α to be fin m for m := fintype.card α, but that's less flexible. Since the multinomial coefficient doesn't really depend on the choice of an order, I suggest you use an order-independent definition. Your definition could become a lemma and serves as a nice formula to calculate it when there's a linear order.
3. fintype.elems α is usually written finset.univ.

[Junyan Xu]

Here are three definitions I came up with, and I like the last one because it's the shortest and doesn't have the fintype restriction, and could be used to state a multinomial theorem in e.g. a docs#mv_power_series ring; I'm not sure what the statement should be, but at least this definition realizes the coefficients of (X1+X2+X3+...)^n as multinomial coefficients. However, we have to use multiset α ≃ (α →₀ ℕ) to connect it to mv_power_series and to your choose formula; the third definition uses finsupp instead of multiset, so it's more directly connected to mv_power_series, but (finsupp.sum f $ λ _, id) is slightly awkward.

import data.finsupp.basic
import data.finite.card
open_locale big_operators
noncomputable theory

def multinomial {α} [fintype α] (n : ℕ) (f : α → ℕ) : ℕ :=
(finset.univ.filter $ λ k : fin n → α, ∀ a, nat.card (k⁻¹' {a}) = f a).card
-- This will be zero if `n ≠ ∑ a, f a`.

def multinomial' {α} [fintype α] (f : α → ℕ) : ℕ :=
(finset.univ.filter $ λ k : fin (∑ a, f a) → α, ∀ a, nat.card (k⁻¹' {a}) = f a).card

def multinomial'' {α} (f : α →₀ ℕ) : ℕ :=
nat.card {k : fin (finsupp.sum f $ λ _, id) → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def multinomial''' {α} [decidable_eq α] (s : multiset α) : ℕ :=
nat.card {k : fin s.card → α // ∀ a, nat.card (k⁻¹' {a}) = s.count a}
-- notice that `multiset α ≃ (α →₀ ℕ)`; could also use `multiset.has_coe_to_sort`.

[Pim Otte]

Thanks so much, this is extremely helpful! I'm not quite familiar with the "//" operator, what's it called/is there some documentation on it?

[Junyan Xu]

// is docs#subtype.

[Junyan Xu]

Just came up to me, this def may be nicer:

def multinomial'''' {α} (n) (f : α →₀ ℕ) : ℕ :=
nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}
-- This will be zero if `n ≠ finsupp.sum f $ λ _, id`, so you don't need the `ite ((∑ i, k i) = n)` to state the multinomial theorem.

[Matt Diamond]

@Junyan Xu is {α} equivalent to {α : Type*}? I wasn't aware of that shorthand, seems useful

[Junyan Xu]

@Matt Diamond Not writing the type means the type will get inferred as usual. In this case yes α will have type Type* since finsupp (α : Type u_13) (M : Type u_14) [has_zero M] :, but sometimes it might be Sort*, for example if α appears in the expression psum α α, because docs#psum takes arguments (α : Sort u) (β : Sort v).

[Matt Diamond]

gotcha

[Pim Otte]

@Junyan Xu I've made an attempt to formulate the multinomial theorem, but I'm a little stuck on how to get the required fintype instance. (My attempts are the commented lines. The problem with the first line is that I'm not even sure restrict_support_equiv gets what I need, and if it does, I don't know how to get the fintype for the subtype introduced in that lemma. The second one doesn't work because it requires a fintype on alpha, which I don't think should be necessary.)

I'm also aware of some problems: 1. It's a little messy. I played with s/k.support/casts until all the types worked out, and though I think it's semantically correct, it's kind of whacky still. 2. I didn't use the mv_power_series approach. I don't strictly need it for the result I want to prove, but I do recognize it would be nicer to formulate for that, since it is more general. I wouldn't know how to get the sum on the right though, since then the "domain" of the sum would no longer be finite, right? I guess you could formulate the theorem in terms of coeff (\sum x_i)^n, but that seems kind of hacky too.

If you have any pointers, it would be greatly appreciated:)

import data.finsupp.basic
import data.finite.card
open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def fintype.finsupp_on_finset (α : Type*) (s : finset α) (n : ℕ) :  fintype (coe_sort s →₀ (fin (n+1))) := sorry
   -- fintype.of_equiv _ ((finsupp.restrict_support_equiv (s : set α) (fin (n+1))))
   -- fintype.of_equiv (coe_sort s → fin (n+1)) (equiv.symm (finsupp.equiv_fun_on_fintype))

def multinomial_theorem (α : Type*) (s : finset α) {R : Type*} [comm_ring R] (x: α →₀ R) (n : ℕ) :
   (∑ i in s, x i)^n = ∑ k : s →₀ (fin (n+1)), (@multinomial s n (finsupp.map_range (λ (i : (fin (n+1))), (i : ℕ)) (rfl) k))*(∏ i in k.support, (x i)^(((k i) : ℕ)))  :=
begin
   sorry,
end

[Junyan Xu]

@Pim Otte I've also found the question about the indexing type for the summation tricky, but I think I just found the preferred choice: sym s n (docs#sym), which has a fintype instance docs#sym.fintype, albeit a very inefficient one if you want to use it for computation, because the time complexity is like #s^n; a generalized docs#list.nat.antidiagonal (which is the special case #s=2) would have time complexity (n+#s-1).choose n and be much more friendly for computation for large n. This would be an issue if you want to do explicit computation and have Lean enumerate all the monomials in the sum expansion for you, but it doesn't matter if you just want to prove things.

docs#sym gives you multiset s, and you can use docs#multiset.map subtype.val to get multiset α and then docs#multiset.to_finsupp to get to α →₀ ℕ. You may also simply use multiset α in the definition of multinomial to make this conversion unnecessary. (And note that finsupp is also notoriously known to be unamenable to computation.)

[Junyan Xu]

Notice that there is docs#sym.sym' is a quotient of vector α n and has an equiv docs#sym.sym_equiv_sym' with docs#sym, so you may define the multinomial coefficients as cardinalities of the fibers of the map vector α n → sym α n as well.

[Junyan Xu]

Of course if you don't care about computability at all you can prove your indexing set is finite and then use the noncomputable docs#set.finite.to_finset to get a indexing finset.

[Yaël Dillies]

Also mind docs#finset.sym as a way to avoid fintype computation. I introduced it a while back precisely for multinomial coefficients.

[Jake Levinson]

Pim Otte said:

Junyan Xu I've made an attempt to formulate the multinomial theorem, but I'm a little stuck on how to get the required fintype instance. (My attempts are the commented lines. The problem with the first line is that I'm not even sure restrict_support_equiv gets what I need, and if it does, I don't know how to get the fintype for the subtype introduced in that lemma. The second one doesn't work because it requires a fintype on alpha, which I don't think should be necessary.)

I'm also aware of some problems: 1. It's a little messy. I played with s/k.support/casts until all the types worked out, and though I think it's semantically correct, it's kind of whacky still. 2. I didn't use the mv_power_series approach. I don't strictly need it for the result I want to prove, but I do recognize it would be nicer to formulate for that, since it is more general. I wouldn't know how to get the sum on the right though, since then the "domain" of the sum would no longer be finite, right? I guess you could formulate the theorem in terms of coeff (\sum x_i)^n, but that seems kind of hacky too.

If you have any pointers, it would be greatly appreciated:)

import data.finsupp.basic
import data.finite.card
open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def fintype.finsupp_on_finset (α : Type*) (s : finset α) (n : ℕ) :  fintype (coe_sort s →₀ (fin (n+1))) := sorry
   -- fintype.of_equiv _ ((finsupp.restrict_support_equiv (s : set α) (fin (n+1))))
   -- fintype.of_equiv (coe_sort s → fin (n+1)) (equiv.symm (finsupp.equiv_fun_on_fintype))

def multinomial_theorem (α : Type*) (s : finset α) {R : Type*} [comm_ring R] (x: α →₀ R) (n : ℕ) :
   (∑ i in s, x i)^n = ∑ k : s →₀ (fin (n+1)), (@multinomial s n (finsupp.map_range (λ (i : (fin (n+1))), (i : ℕ)) (rfl) k))*(∏ i in k.support, (x i)^(((k i) : ℕ)))  :=
begin
   sorry,
end

Hmm, is there a reason you aren't assuming [decidable_eq α]? With that, your second attempt works:

def fintype.finsupp_on_finset (α : Type*) (s : finset α) [decidable_eq α] (n : ℕ) :
   fintype (coe_sort s →₀ (fin (n+1))) :=
   fintype.of_equiv _ (equiv.symm (finsupp.equiv_fun_on_fintype))

[Pim Otte]

Thanks a lot, all of you! I'm going to experiment a little bit and see if I want to switch to docs#sym or stay with the current approach.

@Jake Levinson I'm guessing this works because there's some fintype floating around that applies when you add the [decidable_eq α], but how did you get to this? Is it just intuition or is there a systematic approach you took that I could apply in the future?

[Pim Otte]

The saga continues!

I managed to formulate the theorem using sym, which looks kind of nice. I also managed to do it for arbitrary finsets, not just univ of a fintype. However, I used coe_sort to coerce the type s to a structure to iterate over it, which I think is correct, but in the proof I'm stuck going the other way, identifying an emptyset that's coerced to sort with an emptyset. Any pointers for this, or should I have gone another way in the definition?

import data.finsupp.basic
import data.finite.card
import data.finset.sym
import data.finsupp.multiset

open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def multinomial_theorem (α : Type*) [decidable_eq α] (s : finset α) {R : Type*} [comm_ring R] (x: s →₀ R) (n : ℕ) (hn: n > 0):
   (∑ (i : coe_sort s), x i)^n = ∑ k : (sym s n), ((multinomial n (k.val.to_finsupp))*(∏ (i : coe_sort s), (x i)^(k.val.count i)))  :=
begin
   induction s using finset.cons_induction with h₁ h₂ h₃ h₄,
   {
      simp only [zero_pow hn, finset.univ_eq_attach, finset.attach_empty, finset.sum_empty, subtype.val_eq_coe, finset.prod_empty,
  mul_one],
      have fact: sym (coe_sort (finset.empty : finset α)) n = finset.empty,
      {
         unfold finset.empty,
         rw finset.mk_zero,

         exact finset.sym_eq_empty.mpr ⟨ne_of_gt hn, rfl⟩,
      },
   },
   sorry,
end

[Junyan Xu]

I'll take a look later if no one does; now I'd just point out that you can simply write i : s and Lean will parse it as i : coe_sort s, displayed as i : ↥s.

[Junyan Xu]

I think what you want are docs#finset.is_empty_coe_sort and docs#sym.is_empty

[Junyan Xu]

similarly there's no need to write coe_sort in sym (coe_sort (finset.empty : finset α)) n. Since Lean expects a type/sort as the first argument of sym, it will automatically insert a coe_sort.
And you can write ∅ : finset α

[Yakov Pechersky]

The right way to sum over a finset is Sum i in s, also

[Junyan Xu]

Yes, ∑ i in s instead of ∑ (i : coe_sort s)
∑ k : sym s n is correct because sym s n is a (finite) type.

[Pim Otte]

I'm still working on the other stuff, but ∑ i in s leads to i : α, whereas ∑ i leads to i : ↥s, which works a little better with the definition of x, so I'm currently rolling ∑ iwhich does look a lot nicer:D

[Junyan Xu]

Oh I see x: s →₀ R is also problematic. Since s is finite there's no need of the ₀. Moreover, finset big operator lemmas are usually stated with x : α → R instead.

[Junyan Xu]

Some other comments:
[comm_semiring R] should work.
mathlib prefers 0 < n over n > 0. The convention is to always use le/lt not ge/gt (except for epsilon in anlysis).

[Pim Otte]

Attempt to reformulate with x : α →₀ R. Two issues: It gives a type mismatch with the finsupp derived from the sym element. Also, I kept the finsupp, because I have no idea how to make the sums in the infinite context (I guess that has something to do with the power_series approach you mentioned earlier?)

import data.finsupp.basic
import data.finite.card
import data.finset.sym
import data.finsupp.multiset

import data.nat.basic

open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x: α →₀ R) (n : ℕ) (hn: 0 < n):
   (∑ i in x.support, x i)^n = ∑ k : (sym x.support n), ((multinomial n (k.val.to_finsupp))*(∏ i in x.support, (x i)^(k.val.count i)))  :=
begin
end

[Junyan Xu]

Sorry, this is what I mean; we still need the finset, and x need only be a function not finsupp:

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ) (hn : 0 < n) :
  (∑ i in s, x i) ^ n = /- or simply `s.sum x` -/
  ∑ k : sym s n, multinomial n k.val.to_finsupp * (k.val.map (x ∘ subtype.val)).prod :=
  /- changed the product to use `multiset.map`and `multiset.prod` -/

[Jake Levinson]

Pim Otte said:

Thanks a lot, all of you! I'm going to experiment a little bit and see if I want to switch to docs#sym or stay with the current approach.

Jake Levinson I'm guessing this works because there's some fintype floating around that applies when you add the [decidable_eq α], but how did you get to this? Is it just intuition or is there a systematic approach you took that I could apply in the future?

In this case I had previously looked for the fintype instance for maps α → β when both are fintypes, and I eventually found pi.fintype:

instance pi.fintype {α : Type*} {β : α → Type*}
  [decidable_eq α] [fintype α] [∀ a, fintype (β a)] : fintype (Π a, β a) := sorry

This is actually slightly more general since it allows dependent functions. I don't have much intuition for decidability, but I think the idea is that to enumerate all the functions α → β, we would enumerate through the elements a : α and then through the choices of where to map them. But then, to map an arbitrary term a' : α through a function constructed "by cases" this way, we have to match a' with one of the a : α's, and that requires decidable_eq α.

[Junyan Xu]

Yeah, I think the decidable_eq originates from the ites in the recursive definition of the (dependent) functions in docs#multiset.pi.cons.

[Pim Otte]

I've made some more steps, but I'm missing the final bit.

I think finset.sum_of_empty should apply, and I have the is_empty on the type, but it doesn't seem to apply. What am I missing?:)

import data.finsupp.basic
import data.finite.card
import data.finset.sym
import data.finsupp.multiset


open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ) (hn : 0 < n) :
  (s.sum x) ^ n = ∑ k : sym s n, multinomial n k.val.to_finsupp * (k.val.map (x ∘ subtype.val)).prod :=
begin
      induction s using finset.cons_induction with h₁ h₂ h₃ h₄,
   {
      simp only [zero_pow hn, finset.univ_eq_attach, finset.attach_empty, finset.sum_empty, subtype.val_eq_coe, finset.prod_empty,
  mul_one],
      have fact : is_empty (sym (∅ : finset α) n),
      {
         rw ← nat.pred_inj (n - 1).succ_pos hn rfl,
         apply sym.is_empty _,
         rw finset.is_empty_coe_sort,
      },
      rw eq_comm,

      apply finset.sum_of_empty,
      -- apply (@finset.sum_of_empty R (sym (∅ : finset α) n) (λ k, multinomial n k.val.to_finsupp * (k.val.map (x ∘ subtype.val)).prod) _ fact),
      sorry,
   },
   {
   },
end

[Yakov Pechersky]

haveI instead of have. is_empty is used as a typeclass constraint, and haveI populates it into the typeclass instance cache

[Pim Otte]

Thanks! I've corrected this, but it still fails to unify, I'm afraid

[Junyan Xu]

Yeah Lean seems to have trouble figuring out the function sym ↥∅ n → R in finset.sum_of_empty when doing apply or exact, but this works:

      convert finset.sum_of_empty,
      exact fact,

[Junyan Xu]

By the way the theorem should hold for n=0 right? Just the proof would be different.

[Junyan Xu]

Curiously, if you do haveI, then convert creates the goal sym ↥∅ n → R. I've seen this bug elsewhere ...

[Pim Otte]

Awesome, new tactic time:)

With respect to n=0: the part that I was kind of fuzzy about is the 0^0 issue for s = ∅and n=0. I don't really know how I'd work around that.

[Yaël Dillies]

0^0 = 1 in Lean (at least with the zeroes you're dealing with now :wink:)

[Pim Otte]

Thanks for all the help everyone!

Current roadblock for me: How to handle multiset.map and coe default (which I think represents an emptyset in the current context, but I don't really grasp what it is). It's probably a bit explicit/long too, so if people have golfing suggestions, I'm open to those:)

import data.finsupp.basic
import data.finite.card
import data.finset.sym
import data.finsupp.multiset


open_locale big_operators
noncomputable theory


def multinomial {α} (n) (f : α →₀ ℕ) : ℕ := nat.card {k : fin n → α // ∀ a, nat.card (k⁻¹' {a}) = f a}

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ) :
  (s.sum x) ^ n = ∑ k : sym s n, multinomial n k.val.to_finsupp * (k.val.map (x ∘ subtype.val)).prod :=
begin
      induction s using finset.cons_induction with h₁ h₂ h₃ h₄,
   {
      by_cases hn : 0 < n,
      {
         simp only [zero_pow hn, finset.univ_eq_attach, finset.attach_empty, finset.sum_empty, subtype.val_eq_coe, finset.prod_empty,
  mul_one],
         convert eq_comm.mp finset.sum_of_empty,
         rw ← nat.pred_inj (n - 1).succ_pos hn rfl,
         apply sym.is_empty _,
         rw finset.is_empty_coe_sort,
      },
      {
         have fact : n = 0,
         {
            push_neg at hn,
            exact nat.le_zero_iff.mp hn,
         },
         rw fact,
         rw finset.sum_empty,
         simp,
         have fact': is_empty {x // x ∈ (∅ : finset α)},
         {
            exact set.is_empty_coe_sort.mpr rfl,
         },
         sorry,
      }

   },
   {
      sorry,
   },
end

[Junyan Xu]

↑default is docs#multiset.nil (denoted 0) but this is missing as a simp lemma. You can unfold default to get ↑sym.nil but we don't even have sym.coe_nil ...
I think you don't need induction for n = 0, i.e. you can do by_cases before induction.
I'm not even sure induction is the correct approach to prove the multinomial theorem as formulated, because multinomial isn't defined recursively. I think the we should rather use something like docs#finset.prod_univ_sum, docs#finset.sum_sigma, and docs#fintype.sum_equiv.

[Junyan Xu]

By the way I just remembered that replacing x ∘ subtype.val with x ∘ coe would be nicer. coe (or ↑) is the "simp normal form" of subtype.val.

[Junyan Xu]

For this specific goal: if you do

         convert (mul_one _).symm,
         erw multiset.to_finsupp_zero,

then the goal becomes ↑(multinomial 0 0) = 1.

[Eric Wieser]

a generalized docs#list.nat.antidiagonal (which is the special case #s=2) would have time complexity (n+#s-1).choose n and be much more friendly for computation for large n.

docs#list.nat.antidiagonal_tuple

[Junyan Xu]

Thanks for pointing it out! There are also the multiset/finset versions and docs#finset.nat.sigma_antidiagonal_tuple_equiv_tuple seems to be made exactly for the purpose of multinomial theorem. I guess we should construct an equiv between the finset version and sym so that we can translate freely between sums over both.

[Eric Wieser]

I think there is some code on a branch somewhere that does that; @Kyle Miller might remember

[Kyle Miller]

I'm not sure what "that" is here, but I'm remembering one multinomial-related piece of code: https://github.com/leanprover-community/mathlib/blob/binomial/src/data/nat/choose/multinomial.lean

It's the multinomial coefficient is using a list, so for example multinomial [a, b, c]. I've thought this was nice because it gives a reasonable notation for it.

[Kyle Miller]

I didn't get very far, but this seems like a nice interface for the multinomial coefficient. I suggest proving the combinatorial version as a lemma (and to do this, you probably want a good number of supporting lemmas, giving equivalences for the type that parallel a recursive definition for multinomial)

open_locale big_operators nat

def multinomial {α} [fintype α] (f : α → ℕ) : ℕ := (∑ i, f i)! / ∏ i, (f i)!

#eval multinomial ![1,2,3]
-- 60

lemma multinomial_eq {α} [fintype α] (f : α → ℕ) :
  multinomial f = nat.card {k : fin (∑ i, f i) → α // ∀ a, nat.card (k ⁻¹' {a}) = f a} :=
sorry

[Eric Wieser]

"that" refers to the equivalence between the n-ary antidiagonal, and sym, I think

[Kyle Miller]

A fun application:

#eval ((list.nat.antidiagonal_tuple 5 20).map multinomial).sum
-- 95367431640625
#eval 5^20
-- 95367431640625

It evaluates relatively quickly for Lean, just a second or two.

[Jake Levinson]

Kyle Miller said:

I didn't get very far, but this seems like a nice interface for the multinomial coefficient. I suggest proving the combinatorial version as a lemma (and to do this, you probably want a good number of supporting lemmas, giving equivalences for the type that parallel a recursive definition for multinomial)

open_locale big_operators nat

def multinomial {α} [fintype α] (f : α → ℕ) : ℕ := (∑ i, f i)! / ∏ i, (f i)!

#eval multinomial ![1,2,3]
-- 60

lemma multinomial_eq {α} [fintype α] (f : α → ℕ) :
  multinomial f = nat.card {k : fin (∑ i, f i) → α // ∀ a, nat.card (k ⁻¹' {a}) = f a} :=
sorry

The combinatorialist in me thinks that the underlying combinatorial object
{k : fin (∑ i, f i) → α // ∀ a, nat.card (k ⁻¹' {a}) = f a} should also be given a name, and then the various recursions can be proven bijectively instead of just by counting.

[Jake Levinson]

(Though, that particular lemma should probably be proven using something like the orbit-stabilizer lemma.)

[Pim Otte]

Kyle Miller said:

I'm not sure what "that" is here, but I'm remembering one multinomial-related piece of code: https://github.com/leanprover-community/mathlib/blob/binomial/src/data/nat/choose/multinomial.lean

It's the multinomial coefficient is using a list, so for example multinomial [a, b, c]. I've thought this was nice because it gives a reasonable notation for it.

This looks pretty useful and besides the duplication between bionomial.lean/multinomial.lean, my untrained eye doesn't really spot any reason not to PR this as-is. Of course it could be extended with more lemma's and the combinatorial definition and such, but this seems like plenty already. What would you say would need to be done before starting a PR? Would you mind if I tried my hand at bringing this branch to mathlib?

[Kyle Miller]

@Pim Otte I'm not sure why it hasn't been PR'd. I think this branch was an experiment by @Kevin Buzzard with some additional experimentation of my own.

If you wanted to take it on, I'd suggest getting things from multinomial.lean together for a PR, and I'd also suggest switching to the following definition:

def multinomial {α} [fintype α] (f : α → ℕ) : ℕ := (∑ i, f i)! / ∏ i, (f i)!

That seems to be more versatile than using lists.

[Pim Otte]

Sounds good:) In a comparable situation @Junyan Xu recommended to base a definition on a finset instead of just univ of a fintype. I don't know if that still holds in this context, any thoughts on that?

[Yaël Dillies]

I agree with you. It still applies.

[Kyle Miller]

I like this one because you can write multinomial ![a, b, c], which is some nice notation for free, but I haven't given it too much thought.

[Kyle Miller]

What is the reason? I missed this discussion.

[Yaël Dillies]

It's much easier to add/remove an element to a finset than to a fintype.

[Yaël Dillies]

If we add a finset, your example becomes multinomial univ ![a, b, c], which I think is still quite nice?

[Kyle Miller]

I suppose that's reasonable, and that's a fine enough interface.

[Kyle Miller]

@Pim Otte Then here's an amended suggestion:

/-- The multinomial coefficient. Gives the number of strings
consisting of symbols from `s`, where `c ∈ s`
appears with multiplicity `f c`.

Example: `multinomial finset.univ ![2,2,3]` gives the number of strings
from the set `{0, 1, 2}` with two `0`'s, two `1`'s, and three `2`'s. -/
def multinomial {α} (s : finset α) (f : α → ℕ) : ℕ :=
(∑ i in s, f i)! / ∏ i in s, (f i)!

[Kyle Miller]

I'm forgetting -- what's the mathlib interface to update the value of a function at a particular input? It shows up in the API for summations/products.

[Yaël Dillies]

docs#function.update

[Junyan Xu]

We can do finsupp as well:

open_locale nat
def multinomial {α} (f : α →₀ ℕ) : ℕ := (f.sum $ λ _, id)! / f.prod (λ _ n, n!)

[Kyle Miller]

One weakness with finsupp is that you can't tell the difference between having zero of a symbol in the string and not including the symbol at all. They give the same values, but I worried that it might make some things more awkward.

[Yaël Dillies]

Maybe that's not a bug, but a feature?

[Kyle Miller]

Using the principle that it tends to be better to break apart product types into separate arguments unless the function is specifically about a particular object, maybe it's better writing multinomial f.support f?

[Yaël Dillies]

A finsupp is not a product of a finset and a function, however.

[Kyle Miller]

Sure, it's a finset, a function, and a proof the finset is a support of the function

[Kyle Miller]

and multinomial doesn't make use of the third one

[Kyle Miller]

to be more precise, I mean "sigma type" (i.e., a dependent product)

[Mario Carneiro]

crazy idea: M x ∈ s, f x

[Yaël Dillies]

Oh, does that make M x y, f x y mean the right thing?

[Mario Carneiro]

that sounds unlikely: it works out to (∑ x, (∑ y, f x y)! / ∏ y, (f x y)!)! / ∏ x, ((∑ y, f x y)! / ∏ y, (f x y)!)! which doesn't look like it would be equal to (∑ x y, f x y)! / ∏ x y, (f x y)!

[Mario Carneiro]

def multinomial {α} [fintype α] (f : α → ℕ) : ℕ := (∑ x, f x)! / ∏ x, (f x)!

#eval multinomial (λ x : bool, multinomial (λ y : bool, 1)) -- 6
#eval multinomial (λ x : bool × bool, 1) -- 24

[Kyle Miller]

Hmm, that makes me wonder whether it might be useful to have "universal big operators":

def multinomial {α} [fintype α] (f : α → ℕ) : ℕ := (∑ i, f i)! / ∏ i, (f i)!

notation `<| ` g ` |>λ ` binders `, ` r:(scoped:67 f, g f) := r

#eval <|multinomial|>λ (x : bool) (y : bool), 1

(I'm just using multinomial as an example; I'm not sure it's useful here.)

[Pim Otte]

I collected some of the basic results and PR'd them :D

[Pim Otte]

I've picked up trying the multinomial theorem. Below my progress (I have a separate case for n=0, if necessary)

My guess is that the way forward from this point would be to prove that the term in the first sum is stable under permutation of p, rewrite the sum per "orbit" under permutation (don't know if orbit is the technically correct term here). However, I have no clue how to approach that formally, and I'm not even sure it's the right approach. Proving the other term stable under permutation and "reversing" the quotient on permutation that happens in the definition of multiset would work too, but seems harder.

Any pointers?:)

import algebra.big_operators.fin
import algebra.big_operators.order
import data.nat.choose.basic
import data.finset.sym
import data.finsupp.multiset
import data.fin.vec_notation


open_locale nat
open_locale big_operators

variables {α : Type*} (s : finset α) (f : α → ℕ)

def multinomial : ℕ := (∑ i in s, f i)! / ∏ i in s, (f i)!

def nil_coe : (coe (@sym.nil α)) = (0 : multiset α) :=
begin
  rw sym.nil,
  rw sym.mk_coe 0 multiset.card_zero,
end

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ) :
  (s.sum x) ^ n = ∑ k : sym s n, multinomial k.val.to_finsupp.support k.val.to_finsupp * (k.val.map (x ∘ coe)).prod :=
begin
  simp only [subtype.val_eq_coe, function.comp_app],
  rw finset.pow_eq_prod_const,
  rw ← fin.prod_univ_eq_prod_range,
  rw finset.prod_univ_sum,
  sorry,
end

[Kevin Buzzard]

I'm late to the party but I would proceed by using finset.induction_on. You'll instantly run into a bunch of easier facts about multinomial which you should then factor out and prove first. I don't know if this is the best approach for multinomial coefficients (I'm not implying that is isn't, I just don't know). What do they do in Isabelle/HOL?

[Junyan Xu]

@Pim Otte Here is a continuation of the non-inductive approach, where the sorry should be filled in by considering the action of docs#equiv.perm on fin n → α(acting on the domain) which preserves the range multiset. Then we can use docs#mul_action.card_orbit_mul_card_stabilizer_eq_card_group (but mathlib doesn't even know the cardinality of docs#equiv.perm is docs#nat.factorial, it seems).

import algebra.big_operators.fin
import algebra.big_operators.order
import data.nat.choose.basic
import data.finset.sym
import data.finsupp.multiset
import data.fin.vec_notation

open_locale nat big_operators

variables {α β : Type*} (s : finset α) (f : α → ℕ)

def multinomial : ℕ := (∑ i in s, f i)! / ∏ i in s, (f i)!

def nil_coe : (coe (@sym.nil α)) = (0 : multiset α) :=
begin
  rw sym.nil,
  rw sym.mk_coe 0 multiset.card_zero,
end

def finsupp.multinomial (f : α →₀ ℕ) : ℕ := (f.sum $ λ _, id)! / f.prod (λ _ n, n!)

lemma finsupp.multinomial_eq (f : α →₀ ℕ) :
  f.multinomial = multinomial f.support f := rfl

noncomputable def multiset.multinomial (m : multiset α) : ℕ := m.to_finsupp.multinomial

lemma multiset.to_finsupp_map (f : α → β) (m : multiset α) :
  (m.map f).to_finsupp = m.to_finsupp.map_domain f :=
by conv_lhs
  { rw [← m.to_finsupp_to_multiset, finsupp.to_multiset_map, finsupp.to_multiset_to_finsupp] }

lemma multiset.map_multinomial (f : α ↪ β) (m : multiset α) :
  (m.map f).multinomial = m.multinomial :=
begin
  simp only [multiset.multinomial, finsupp.multinomial, m.to_finsupp_map f],
  congr,
  exacts [finsupp.sum_map_domain_index_inj f.inj', finsupp.prod_map_domain_index_inj f.inj'],
end

@[simps] def sym_finset_to_multiset (n : ℕ) : sym s n ↪ multiset α :=
{ to_fun := λ f, f.1.map coe,
  inj' := (multiset.map_injective subtype.coe_injective).comp subtype.val_injective }

def multiset.trunc_enum_of_fin_card {α} (s : multiset α) :
  trunc {f : fin s.card → α // finset.univ.val.map f = s} :=
quotient.rec_on s (λ l, trunc.mk ⟨λ i, l.nth_le i i.2, congr_arg coe l.map_nth_le⟩)
  (λ _ _ _, subsingleton.elim _ _)

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ) :
  (s.sum x) ^ n = ∑ k : sym s n, k.val.multinomial * (k.val.map (x ∘ coe)).prod :=
begin
  simp only [subtype.val_eq_coe, function.comp_app],
  rw [finset.pow_eq_prod_const, ← fin.prod_univ_eq_prod_range, finset.prod_univ_sum],
  simp_rw finset.prod,
  classical,
  convert finset.sum_comp (λ m : multiset α, (m.map x).prod) (λ f : fin n → α, finset.univ.val.map f) using 1,
  { simp_rw multiset.map_map },
  convert (finset.sum_map _ (sym_finset_to_multiset s n) _).symm,
  { ext1, rw ← nsmul_eq_mul, congr' 2,
    sorry,
    simp only [sym_finset_to_multiset_apply, multiset.map_map], refl },
  ext1, rw [finset.mem_image, finset.mem_map], split,
  { rintro ⟨f, hf, rfl⟩,
    refine ⟨⟨finset.univ.1.map (λ i : fin n, ⟨f i, fintype.mem_pi_finset.1 hf i⟩),
      (multiset.card_map _ _).trans $ finset.card_fin n⟩, finset.mem_univ _, _⟩,
    rw [sym_finset_to_multiset_apply, multiset.map_map], refl },
  { rintro ⟨⟨m, hm⟩, -, rfl⟩,
    obtain ⟨⟨f, hf⟩⟩ := m.trunc_enum_of_fin_card,
    use coe ∘ f ∘ fin_congr hm.symm,
    rw fintype.mem_pi_finset,
    use λ i, finset.coe_mem _,
    rw [← multiset.map_map, ← multiset.map_map f],
    congr,
    convert hf using 1,
    congr,
    exact congr_arg finset.val (finset.map_univ_equiv $ fin_congr hm.symm) },
end

/-
α: Type
_inst_1: decidable_eq α
R: Type ?
_inst_2: comm_semiring R
x: α → R
s: finset α
n: ℕ
x_1: sym ↥s n
⊢ ↑x_1.multinomial =
  (finset.filter
    (λ (a : fin n → α), multiset.map a finset.univ.val = ⇑(sym_finset_to_multiset s n) x_1)
    (fintype.pi_finset (λ (a : fin n), s))).card
-/

[Pim Otte]

@Junyan Xu Thanks a lot! I had made one more step in my original proof, but that sort of fell flat. I'm going to take a good look at it all and see if I get it and then try and fill in the sorry:)

[Junyan Xu]

@Pim Otte I just discovered docs#finset.sym which can make the statement of the multinomial theorem simpler (removes the coercion), and probably the proof as well.
I made some progress in the direction of the inductive approach suggested by @Kevin Buzzard, and it looks like it's gonna yield a shorter proof. Here's my progress so far:

def sym_insert_of_sigma_sym_sub [decidable_eq α] (a : α) (n : ℕ)
  (m : Σ i : fin (n + 1), sym s (n - i)) : sym ↥(insert a s) n :=
⟨m.2.1.map (set.inclusion $ λ x, finset.mem_insert_of_mem) + m.1.1 • {⟨a, s.mem_insert_self a⟩},
  by { rw [multiset.card_add, multiset.card_map, m.2.2, multiset.card_nsmul,
    multiset.card_singleton, mul_one], exact nat.sub_add_cancel (nat.lt_succ_iff.1 m.1.2) }⟩

@[simps] def sym_insert_equiv_sigma_sym_sub [decidable_eq α] (a : α) (ha : a ∉ s) (n : ℕ) :
  sym ↥(insert a s) n ≃ Σ i : fin (n + 1), sym s (n - i) :=
{ to_fun := λ m, ⟨⟨(m.1.map coe).count a,
    (multiset.count_le_card _ _).trans_lt $ by rw [multiset.card_map, m.2, nat.lt_succ_iff]⟩,
    (m.1.filter $ λ x : insert a s, x.1 ≠ a).attach.map
      (λ x, ⟨x, finset.mem_of_mem_insert_of_ne x.1.2 (multiset.mem_filter.1 x.2).2⟩),
    by { rw [multiset.card_map, multiset.card_attach, subtype.coe_mk, multiset.count_map],
      convert ← (tsub_eq_of_eq_add $ multiset.card_eq_countp_add_countp _ _).symm,
      { apply multiset.countp_eq_card_filter },
      { exact m.2 },
      { simp_rw [not_ne_iff, eq_comm], apply multiset.countp_eq_card_filter } }⟩,
  inv_fun := sym_insert_of_sigma_sym_sub s a n,
  left_inv := sorry,
  right_inv := sorry }

theorem multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) :
  ∀ n, (s.sum x) ^ n = ∑ k : sym s n, k.val.multinomial * (k.val.map (x ∘ coe)).prod :=
begin
  induction s using finset.induction with a s ha ih,
  { rw finset.sum_empty,
    rintro (_ | n),
    { rw [pow_zero, finset.sum_unique_nonempty],
      { convert (one_mul _).symm, apply nat.cast_one },
      { apply finset.univ_nonempty } },
    { rw [pow_succ, zero_mul],
      convert finset.sum_of_empty.symm,
      convert sym.is_empty n,
      rw finset.is_empty_coe_sort,
      /- extract instance: finset version of set.has_emptyc.emptyc.is_empty -/ } },
  intro n,
  rw [finset.sum_insert ha, add_pow, finset.sum_range],
  simp_rw [ih, finset.mul_sum, finset.sum_mul, finset.sum_sigma'],
  /- now apply fintype.sum_equiv with `sym_insert_equiv_sigma_sym_sub` and
    rewrite by `multinomial_insert` in #16170;
    however if we switch to `finset.sym` in the statement
    then we would have to use `finset.sum_bij` or `sum_bij'`. -/
  sorry,
end

[Yaël Dillies]

Yaël Dillies said:

Also mind docs#finset.sym as a way to avoid fintype computation. I introduced it a while back precisely for multinomial coefficients.

:point_up: :grinning:

[Pim Otte]

Small rewrite to use finset.sym (which actually does seem to simplify the first part) and to bring the (n : ℕ) to the theorem statement, which I think is preferred?

def multinomial_theorem (α : Type*) [decidable_eq α] {R : Type*} [comm_semiring R] (x : α → R)
  (s : finset α) (n : ℕ):
 (s.sum x) ^ n = ∑ k in finset.sym s n, k.val.multinomial * (k.val.map x).prod :=
begin
 revert n,
 induction s using finset.induction with a s ha ih,
  { rw finset.sum_empty,
    rintro (_ | n),
    { rw [pow_zero, finset.sum_unique_nonempty],
      { convert (one_mul _).symm, apply nat.cast_one },
      { apply finset.univ_nonempty } },
    { rw [pow_succ, zero_mul, finset.sym_empty, finset.sum_empty], } },
  intro n,
  rw [finset.sum_insert ha, add_pow, finset.sum_range],
  simp_rw [ih, finset.mul_sum, finset.sum_mul, finset.sum_sigma'],
  /- TODO: use `finset.sum_bij(')`and rewrite by `multinomial_insert` in #16170; -/
  sorry,
end

[Junyan Xu]

bring the (n : ℕ) to the theorem statement, which I think is preferred?

All arguments before the colon is the general conventnion, but you occasionally see arguments after the colon because it makes the proof shorter, as is the case here.

[Eric Rodriguez]

I think the only "guideline" is make the proof shortest - revert/intros at the very start is always unnecessary. Still, I often see revert at the start, and this is also often OK, especially when the terms being reverted are part of a variables statement

[Yaël Dillies]

intros at the beginning is not always a bad sign. For example if you want to prove that some function is injective, you will intros a b hab

[Junyan Xu]

@Pim Otte I now have a complete proof using the inductive approach at https://gist.github.com/alreadydone/f9d4444bde854a77e9771db3c9011cb1 . Indeed using docs#finset.sym makes things smoother. Have you been working on the orbit-stabilizer approach? I would be curious to know about any progress.

I'm not sure if it's worth providing the original statement using sym s n as a version of the theorem, but I think it's definitely worth making a docs#finset.nat.antidiagonal_tuple version when s is finset.univ in fin k. For general s with a bijection to fin k, I think it's also worth providing the antidiagonal_tuple version, as it allows more efficient computation.

[Pim Otte]

@Junyan Xu Awesome! I had not made any progress on the orbit-stabilizer approach. I don't really have an opinion one way or the other on alternative proofs, but I think for what I was working on this would be sufficient.

If we move this into mathlib, would stuff like finsupp.multinomial go in the data.nat.choose.multinomial (edited), but with a finsupp namespace?

Is it okay if I PR this with you as co-author, in a new PR, dependent on #16170?

[Junyan Xu]

Feel free to PR! I think it's most natural to include the various versions of multinomial coefficients in the multinomial file. data.nat.choose seems a weird place. For example, we can't state finsuop.multinomial_eq without the finset version. (And I think the finset version should probably be renamed finset.multinomial.)

[Junyan Xu]

Interestingly there is another thing that could be called multiset.multinomial, which comes from showing the original list.multinomial (which takes a list of multiplicities as input) is independent of the order of the multiplicities. (And we could also define docs$nat.partition .multinomial.) Do we want both multiset versions, and if so how should we disambiguate the names?

[Pim Otte]

I don't really have the overview to see if we need the alternative version and the naming conventions. Since you can always convert the list to a finsupp easily and use that for the multinomial, I think it's fine using the current version as multiset.mutinomial, and worrying about an alternative name for the other version later?

[Luis Castillo]

(deleted)

[Junyan Xu]

I think multiset.multinomial is good for the current version; the other version could be called multiset.nat_multinomial or multiset.nat.multinomial. The latter dot notation needs a special ^ trick to work and I don't know where it's documented (I only discovered it in the last month) or if anything changed in Lean 4, but it's used for docs#ideal.quotient.mk here for example.