Glaisher’s Bijection on integer partitions

Stream: mathlib4

[Chi-Yun Hsu]

Hi everyone,

I am seeking feedback for my PR #33031 opened last month, which currently formalizes the combinatorial proof of Euler’s partition identity via the Glaisher bijection between odd partitions and distinct partitions.

Currently the proof of Euler’s identity in mathlib4 is through generating functions @Bhavik Mehta . This has also been brought forward by @Weiyi Wang to formalize Glaisher’s theorem: the number of partitions whose parts are not divisible by $d$ is the same as the number of partitions whose parts have multiplicity $< d$.

As mathlib4 does not simply accept alternative proofs, I would like to expand the PR to provide stronger results coming from Glaisher’s bijection. Indeed, the Glaisher bijection between odd partitions of $n$ and distinct partitions of $n$ can be lifted to a bijection on all partitions of $n$, and this bijection is actually an involution. My proposal to expand the PR is: 
(1) formalize the involution on the set of partitions of $n$
(2) the involution restricts to a bijection between odd partitions and distinct partitions
(2)’ the involution restricts to a bijection between partitions whose parts are not divisible by $2^i$ and partitions whose hav multiplicity $< 2^i$. (Glaisher’s theorem for $d=2^i$.)
(3) the partitions fixed by the involution are the distinct odd partitions.

A technical note: The current Lean code uses ordProj[p] n, the largest power of $p$ dividing $n$. This makes generalizing from $p=2$ to any prime $p$ straightforward. Moving to a general $d$ (Glaisher’s Theorem) is the end goal, though it will require expansions on other libraries.

Do people agree that the Glaisher involution would provide enough added value to be included in mathlib4?

[Weiyi Wang]

I am neutral on this, as I wasn't aware the alternative proof and its value when making the current one. The proof was more of a demonstration of using recently developed lemmas for infinite sum of power series

[Weiyi Wang]

Just by your post here, it looks like it can be only generalized to d = p ^ i for prime p? How do we get this for any positive integer d?

[Weiyi Wang]

I guess it is hiding behind "it will require expansions on other libraries". I think even if people don't agree with including your complete proof of Glaisher's theorem, you can still work on upstreaming those useful intermediate lemma. And if a lot of intermediate lemma is upstreamed, perhaps the final proof will be short, which might make this a more convincing case

[Chi-Yun Hsu]

@Weiyi Wang Thank you for sharing your thoughts. The current code does not directly generalize to non-primes $d$ because I was using ordProj[p] n. The solution is to use multiplicity d n instead. I simply have not looked into switching equivalent lemmas between the ordProj and multiplicity. The current code focuses entirely on the proof of Euler's identity, so upstreaming intermediate lemmas to multiplicity (if needed) would not considerably shorten the proof either.

Because Glaisher's Theorem is already formalized, my understanding is that mathlib4 only wants to accept one proof. I thinks there are merits formalizing Glaisher's bijection, so I am supporting it by results which could only be proven through the bijection but not through generating series.

[Bhavik Mehta]

I agree that looking for results that could only be proven through the bijection is the right thing to do here - have you managed to identify any these that could be nicely done from your work?

[Chi-Yun Hsu]

I think the main result which is impossible to get from generating series is that the bijection is an involution.

[Bhavik Mehta]

Are there any theorems that use the fact that it's an involution? The one you mention is a result about the bijection itself, rather than something which uses the bijection

[Chi-Yun Hsu]

I think the fact that there is an involution on Partition(n) inducing the bijection between odd partitions and distinct partitions is itself interesting enough.

On the other hand, if we are looking for partition identities which can be proved using the Glaisher bijection, there are

1. The total number of parts in Dist(n) is the sum of 2-binary digits of the multiplicities of parts in Odd(n)
2. The number of odd partitions consisting of odd integers from a set S is equal to the number of distinct partitions consisting of integers whose odd part is in S.
3. The bijection implies #Odd(n) = #Dist(n), and #$2^i$-regular partitions = #$2^i$-distinct partitions. The fact that the bijection is an involution allows to create bijections on the intersections, eg #Odd $2^i$-distinct partitions = Distinct $2^i$-regular partitions. On the other hand, this can be proven by generating series too.

The results can be a bit deliberate to make a case for Glaisher's bijection. The broader question would be whether mathlib wants to accept any bijective proofs at all. For example, Sylvester's bijection is another bijection between Odd(n) and Dist(n), which provides interesting refined identity: #odd partitions with k distinct odd parts = #distinct partitions with k consecutive sequences. Historically Sylvester's bijection came before the generating series proof, but ultimately it is pretty hard to think of identities where generating series proof does not exist.