Stars and bars

Stream: Is there code for X?

[Oliver Nash]

We don't seem to have this in Mathlib. I don't suppose someone has it elsewhere:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Sym.Basic

open BigOperators

def Sym.starsAndBarsEquiv (ι : Type*) [Fintype ι] (k : ℕ) :
    Sym ι k ≃ {P : ι → ℕ // ∑ i, P i = k} :=
  sorry

[Johan Commelin]

$ rg -i "stars and bars"
Mathlib/Data/Finset/Sym.lean
113:/-- Finset **stars and bars** for the case `n = 2`. -/

Mathlib/Data/Sym/Card.lean
14:# Stars and bars
20:this is central to the "stars and bars" technique in combinatorics, where we switch between
32:The "stars and bars" technique arises from another way of presenting the same problem. Instead of
47:while the "stars and bars" technique gives
53:stars and bars, multichoose
117:/-- The *stars and bars* lemma: the cardinality of `Sym α k` is equal to
191:/-- Type **stars and bars** for the case `n = 2`. -/

Mathlib/Data/Nat/Choose/Basic.lean
33:This is central to the "stars and bars" technique in informal mathematics, where we switch between
39:binomial coefficient, combination, multicombination, stars and bars

[Johan Commelin]

So I think it is there in some form.

[Oliver Nash]

Thanks, I did a similar search. IIUC, the results we have compute the cardinality of Sym ι k in terms of binomial coefficients, but do not provide the bijection I request.

[Oliver Nash]

Of course, I'd love to be corrected!

[Johan Commelin]

Ooh, I see. That's sad. Hopefully it is easy to refactor the proofs to get the equiv?

[Oliver Nash]

I'll take a look later this afternoon if I hear nothing else here.

[Oliver Nash]

OK I caved in and did it by hand:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Sym.Basic

open BigOperators

@[simp]
lemma Multiset.sum_count_eq_card {α : Type*} [Fintype α] [DecidableEq α] (s : Multiset α) :
    ∑ a, s.count a = Multiset.card s := by
  rw [← Multiset.toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
  congr
  ext
  simp

/-- A classic "stars and bars" bijection. -/
def Sym.starsAndBarsEquiv (ι : Type*) [DecidableEq ι] [Fintype ι] (k : ℕ) :
    Sym ι k ≃ {P : ι → ℕ // ∑ i, P i = k} where
  toFun := fun ⟨s, hs⟩ ↦ ⟨s.count, by simp [← hs]⟩
  invFun := fun ⟨P, hP⟩ ↦ ⟨∑ i, (P i) • ({i} : Multiset ι), by simpa⟩
  left_inv := by
    rintro ⟨s, hs⟩
    simp only
    congr
    ext i
    erw [Multiset.count_sum] -- TODO Fix
    simp [Multiset.count_singleton]
  right_inv := by
    rintro ⟨P, hP⟩
    ext i
    simp only
    erw [Multiset.count_sum] -- TODO Fix
    simp [Multiset.count_singleton]

I now need to divert my attention but I'll PR this later today unless I hear a reason not to do so.

[Eric Wieser]

I think I discussed something similar in a DM with @Kyle Miller long ago

[Eric Wieser]

This shouldn't need finiteness, should it?

[Junyan Xu]

This also came up here in the complete homogeneous symmetric polynomial PR and I suggested constructing the Equiv but it was not actually done.

[Junyan Xu]

Eric Wieser said:

This shouldn't need finiteness, should it?

You can't write ∑ i, without ι being a Fintype. But you might use docs#Finsupp.sum. In fact there is docs#Multiset.toFinsupp. Maybe we should combine docs#Equiv.image with it to construct starsAndBarsEquiv.

[Kyle Miller]

@Oliver Nash That should be in mathlib. Having a version without Fintype seems like a separate project — having {P : ι → ℕ // ∑ i, P i = k} in bijective correspondence to some type with a know cardinality is important.

I wouldn't call this stars-and-bars however. This bijection is the observation that multisets are determined — and described by — finitely supported Nat-valued functions, via Multiset.count (which, by the way, seems to be missing results about how fun m => m.count is injective, and how the image of m.count is finite). Where are the stars and where are the bars?

[Kyle Miller]

I see, docs#Multiset.toFinsupp would be great for creating this equivalence. (And injectivity/finiteness facts about Multiset.count would be nice to factor out of it.)

[Oliver Nash]

Agreed, I shouldn't really call this "stars and bars". Fiddling with this now we can have the Finsupp version too if we do something like:

lemma Multiset.foo (ι : Type*) [DecidableEq ι] (k : ℕ) :
    toFinsupp.toEquiv '' {s | Multiset.card s = k} = {P : ι →₀ ℕ | P.sum (fun _ ↦ id) = k} := by
  ext P
  simp only [AddEquiv.toEquiv_eq_coe, EquivLike.coe_coe, mem_image, mem_setOf_eq]
  refine ⟨?_, ?_⟩
  · rintro ⟨s, rfl, rfl⟩
    simp [← Finsupp.card_toMultiset]
  · rintro rfl
    exact ⟨Multiset.toFinsupp.symm P, by simp [← Finsupp.card_toMultiset], by simp⟩

def Sym.starsAndBarsEquiv' (ι : Type*) [DecidableEq ι] (k : ℕ) :
    Sym ι k ≃ {P : ι →₀ ℕ // P.sum (fun _ ↦ id) = k} :=
  (Multiset.toFinsupp.toEquiv.image _).trans <| Equiv.Set.ofEq <| Multiset.foo ι k

[Junyan Xu]

We also have docs#Finsupp.equivFunOnFinite to convert to the Fintype.sum version.

[Oliver Nash]

OK I'll PR something along these lines after dinner:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Finsupp.Multiset
import Mathlib.Data.Sym.Basic

open BigOperators

-- No longer need this lemma but still worth adding
@[simp]
lemma Multiset.sum_count_eq_card {α : Type*} [Fintype α] [DecidableEq α] (s : Multiset α) :
    ∑ a, s.count a = Multiset.card s := by
  rw [← Multiset.toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
  congr
  ext
  simp

attribute [simp] Finsupp.card_toMultiset

@[simp]
lemma Multiset.toFinsupp_sum_eq {ι : Type*} [DecidableEq ι] (s : Multiset ι) :
    s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s := by
  rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]

lemma Multiset.toFinsupp_image_card_eq (ι : Type*) [DecidableEq ι] (k : ℕ) :
    toFinsupp '' {s | Multiset.card s = k} = {P : ι →₀ ℕ | P.sum (fun _ ↦ id) = k} := by
  ext P
  refine ⟨?_, ?_⟩
  · rintro ⟨s, rfl, rfl⟩
    simp
  · rintro rfl
    exact ⟨Multiset.toFinsupp.symm P, by simp, by simp⟩

def Sym.equivNatSum (ι : Type*) [DecidableEq ι] (k : ℕ) :
    Sym ι k ≃ {P : ι →₀ ℕ // P.sum (fun _ ↦ id) = k} :=
  (Multiset.toFinsupp.toEquiv.image _).trans <| Equiv.Set.ofEq <|
    Multiset.toFinsupp_image_card_eq ι k

-- It is `Finsupp.equivFunOnFinite` that makes this noncomputable.
noncomputable def Sym.equivNatSum' (ι : Type*) [DecidableEq ι] [Fintype ι] (k : ℕ) :
    Sym ι k ≃ {P : ι → ℕ // ∑ i, P i = k} :=
  (Sym.equivNatSum ι k).trans <| (Finsupp.equivFunOnFinite.image _).trans <| Equiv.Set.ofEq (by
    ext P
    refine ⟨?_, ?_⟩
    · rintro ⟨Q, rfl, rfl⟩
      simp [Set.mem_def, Finsupp.sum_fintype]
    · rintro rfl
      exact ⟨Finsupp.equivFunOnFinite.symm P, by simp [Set.mem_def, Finsupp.sum_fintype], by simp⟩)

[Oliver Nash]

#11360

[Eric Wieser]

It seems pretty silly to me that this is noncomputable... will comment in the PR

[Oliver Nash]

Follow-up PR #11380 (in which stars and bars really do make an appearance).