# mathlibdocumentation

mathlib-archive / 100-theorems-list.45_partition

# Euler's Partition Theorem #

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

noncomputable def theorems_100.partial_odd_gf {α : Type u_1} (m : ) [field α] :

The partial product for the generating function for odd partitions. TODO: As m tends to infinity, this converges (in the X-adic topology).

If m is sufficiently large, the ith coefficient gives the number of odd partitions of the natural number i: proved in odd_gf_prop. It is stated for an arbitrary field α, though it usually suffices to use ℚ or ℝ.

Equations
noncomputable def theorems_100.partial_distinct_gf {α : Type u_1} (m : )  :

The partial product for the generating function for distinct partitions. TODO: As m tends to infinity, this converges (in the X-adic topology).

If m is sufficiently large, the ith coefficient gives the number of distinct partitions of the natural number i: proved in distinct_gf_prop. It is stated for an arbitrary commutative semiring α, though it usually suffices to use ℕ, ℚ or ℝ.

Equations
noncomputable def theorems_100.cut {ι : Type u_1} (s : finset ι) (n : ) :

Functions defined only on s, which sum to n. In other words, a partition of n indexed by s. Every function in here is finitely supported, and the support is a subset of s. This should be thought of as a generalisation of finset.nat.antidiagonal_tuple where antidiagonal_tuple k n is the same thing as cut (s : finset.univ (fin k)) n.

Equations
theorem theorems_100.mem_cut {ι : Type u_1} (s : finset ι) (n : ) (f : ι ) :
f s.sum f = n (i : ι), i s f i = 0
@[simp]
theorem theorems_100.cut_zero {ι : Type u_1} (s : finset ι) :
= {0}

There is only one cut of 0.

@[simp]
theorem theorems_100.cut_empty_succ {ι : Type u_1} (n : ) :
(n + 1) =
theorem theorems_100.cut_insert {ι : Type u_1} (n : ) (a : ι) (s : finset ι) (h : a s) :
= (λ (p : × ), finset.map {to_fun := λ (f : ι ), f + λ (t : ι), ite (t = a) p.fst 0, inj' := _} p.snd))
theorem theorems_100.coeff_prod_range {α : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) (n : ) :
n) (s.prod (λ (j : ι), f j)) = n).sum (λ (l : ι ), s.prod (λ (i : ι), (l i)) (f i)))
noncomputable def theorems_100.indicator_series (α : Type u_1) [semiring α] (s : set ) :

A convenience constructor for the power series whose coefficients indicate a subset.

Equations
theorem theorems_100.coeff_indicator {α : Type u_1} (s : set ) [semiring α] (n : ) :
n) = ite (n s) 1 0
theorem theorems_100.coeff_indicator_pos {α : Type u_1} (s : set ) [semiring α] (n : ) (h : n s) :
n) = 1
theorem theorems_100.coeff_indicator_neg {α : Type u_1} (s : set ) [semiring α] (n : ) (h : n s) :
n) = 0
theorem theorems_100.constant_coeff_indicator {α : Type u_1} (s : set ) [semiring α] :
= ite (0 s) 1 0
theorem theorems_100.two_series {α : Type u_1} (i : ) [semiring α] :
1 + = {0, i.succ}
theorem theorems_100.num_series' {α : Type u_1} [field α] (i : ) :
(1 - power_series.X ^ (i + 1))⁻¹ = {k : | i + 1 k}
Equations
theorem theorems_100.partial_gf_prop (α : Type u_1) (n : ) (s : finset ) (hs : (i : ), i s 0 < i) (c : ) (hc : (i : ), i s 0 c i) :
((finset.filter (λ (p : n.partition), ( (j : ), c j) (j : ), j p.parts j s) finset.univ).card) = n) (s.prod (λ (i : ), ((λ (_x : ), _x * i) '' c i)))
theorem theorems_100.partial_odd_gf_prop {α : Type u_1} [field α] (n m : ) :
theorem theorems_100.odd_gf_prop {α : Type u_1} [field α] (n m : ) (h : n < m * 2) :

If m is big enough, the partial product's coefficient counts the number of odd partitions

theorem theorems_100.distinct_gf_prop {α : Type u_1} (n m : ) (h : n < m + 1) :

If m is big enough, the partial product's coefficient counts the number of distinct partitions

theorem theorems_100.same_gf {α : Type u_1} [field α] (m : ) :
* (finset.range m).prod (λ (i : ), 1 - power_series.X ^ (m + i + 1)) =

The key proof idea for the partition theorem, showing that the generating functions for both sequences are ultimately the same (since the factor converges to 0 as m tends to infinity). It's enough to not take the limit though, and just consider large enough m.

theorem theorems_100.same_coeffs {α : Type u_1} [field α] (m n : ) (h : n m) :