Euler's Partition Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Theorem 45 from the 100 Theorems List.

The theorem concerns the counting of integer partitions -- ways of writing a positive integer n as a sum of positive integer parts.

Specifically, Euler proved that the number of integer partitions of n into distinct parts equals the number of partitions of n into odd parts.

Proof outline #

The proof is based on the generating functions for odd and distinct partitions, which turn out to be equal:

$$\prod_{i=0}^\infty \frac {1}{1-X^{2i+1}} = \prod_{i=0}^\infty (1+X^{i+1})$$

In fact, we do not take a limit: it turns out that comparing the n'th coefficients of the partial products up to m := n + 1 is sufficient.

In particular, we

1. define the partial product for the generating function for odd partitions partial_odd_gf m := $$\prod_{i=0}^m \frac {1}{1-X^{2i+1}}$$;
2. prove odd_gf_prop: if m is big enough (m * 2 > n), the partial product's coefficient counts the number of odd partitions;
3. define the partial product for the generating function for distinct partitions partial_distinct_gf m := $$\prod_{i=0}^m (1+X^{i+1})$$;
4. prove distinct_gf_prop: if m is big enough (m + 1 > n), the nth coefficient of the partial product counts the number of distinct partitions of n;
5. prove same_coeffs: if m is big enough (m ≥ n), the nth coefficient of the partial products are equal;
6. combine the above in partition_theorem.

References #

https://en.wikipedia.org/wiki/Partition_(number_theory)#Odd_parts_and_distinct_parts