Combinatorics / variant of Bell numbers

Stream: maths

[Antoine Chambert-Loir]

For our work (with @María Inés de Frutos Fernández ) on divided powers in #15644, we need to make use of the number of ways of dividing a set with $mn$ elements into $m$ parts with $n$ elements. This is classically equal to $(mn)!/m!n!^m$, but for this formula to be usable, because one first has to prove that the denominator divides the numerator.
There is a formula for that:
$(mn)!/m! n!^m = \prod_{k<m} {k n+n-1 \choose n-1}.$

Anyway, we had coined a word mchoose for that, which, as @Eric Wieser pointed out, is suboptimal.

In general, the number of set partitions of a set with $n$ elements is called the Bell number $B_n$.

What we are interested in is a variant of Bell numbers where we fix the docs#Multiset of cardinalities. If $m$ is a multiset of integers, this number is classically given by $(\sum m)!/\prod_{k\in m}k! \prod_{k>0} n_k(m)!$, where $n_k(m)$ is the multiplicity of $k$ in $m$. Again, for this formula to be usable, one has to prove that the denominator divides the numerator. The best way would be to show that this is precisely the cardinality of what we want, but we don't want to embark in this for now, which would be off topic, but a nice combinatorics project for mathlib.

Just playing with integers, I can prove that this holds by induction, but that uses the previous result, which is not so nice.

[Antoine Chambert-Loir]

In any case, what names could be used for these numbers in mathlib?
“restricted Bell numbers”?
“multiset Bell numbers” — mBell?

[Scott Carnahan]

uniform partition Bell numbers?

[Antoine Chambert-Loir]

Those would be our initial numbers? then maybe “uniform Bell numbers” is enough? and uBell would be a reasonable name…

[Kim Morrison]

Just a general comment here: the bias for authors is to prefer uBell over uniformBell (because they will have to type it many times), but in the end if it is useful work it will be read more often than written, and uniformBell is way better.

[Antoine Chambert-Loir]

I could finally find a formula that explains why the multisetBell number is an integer, I haven't formalized it yet, but I wrote a blog post about it.

https://freedommathdance.blogspot.com/2024/08/combinatorics-of-partitions.html

[Johan Commelin]

Very nice! One comment: in the final formula the lhs is repeated in the rhs

[Antoine Chambert-Loir]

Would ‘Multiset.Bell', with type ‘Multiset Nat -> Nat‘ be a reasonable name? That would leave the possibility to have ‘Nat.Bell‘ for the classical Bell numbers.

[Antoine Chambert-Loir]

(by the way, ‘Bell‘ or ‘bell‘?)

[Yaël Dillies]

bell, since it's not a type