# 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 partialOddGF m := $$\prod_{i=0}^m \frac {1}{1-X^{2i+1}}$$;
2. prove oddGF_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 partialDistinctGF m := $$\prod_{i=0}^m (1+X^{i+1})$$;
4. prove distinctGF_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

def Theorems100.partialOddGF {α : Type u_1} (m : ) [] :

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 oddGF_prop. It is stated for an arbitrary field α, though it usually suffices to use ℚ or ℝ.

Equations
• = i ∈ , (1 - PowerSeries.X ^ (2 * i + 1))⁻¹
Instances For
def Theorems100.partialDistinctGF {α : 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 distinctGF_prop. It is stated for an arbitrary commutative semiring α, though it usually suffices to use ℕ, ℚ or ℝ.

Equations
• = i ∈ , (1 + PowerSeries.X ^ (i + 1))
Instances For
def Theorems100.indicatorSeries (α : Type u_2) [] (s : ) :

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

Equations
Instances For
theorem Theorems100.coeff_indicator {α : Type u_1} (s : ) [] (n : ) :
() = if n s then 1 else 0
theorem Theorems100.coeff_indicator_pos {α : Type u_1} (s : ) [] (n : ) (h : n s) :
() = 1
theorem Theorems100.coeff_indicator_neg {α : Type u_1} (s : ) [] (n : ) (h : ns) :
() = 0
theorem Theorems100.constantCoeff_indicator {α : Type u_1} (s : ) [] :
= if 0 s then 1 else 0
theorem Theorems100.two_series {α : Type u_1} (i : ) [] :
1 + PowerSeries.X ^ i.succ = Theorems100.indicatorSeries α {0, i.succ}
theorem Theorems100.num_series' {α : Type u_1} [] (i : ) :
(1 - PowerSeries.X ^ (i + 1))⁻¹ = Theorems100.indicatorSeries α {k : | i + 1 k}
Equations
Instances For
theorem Theorems100.partialGF_prop (α : Type u_2) [] (n : ) (s : ) (hs : is, 0 < i) (c : ) (hc : is, 0 c i) :
(Finset.filter (fun (p : n.Partition) => (∀ (j : ), Multiset.count j p.parts c j) jp.parts, j s) Finset.univ).card = () (is, Theorems100.indicatorSeries α ((fun (x : ) => x * i) '' c i))
theorem Theorems100.partialOddGF_prop {α : Type u_1} [] (n : ) (m : ) :
(Finset.filter (fun (p : n.Partition) => jp.parts, ) Finset.univ).card =
theorem Theorems100.oddGF_prop {α : Type u_1} [] (n : ) (m : ) (h : n < m * 2) :
.card =

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

theorem Theorems100.partialDistinctGF_prop {α : Type u_1} [] (n : ) (m : ) :
(Finset.filter (fun (p : n.Partition) => p.parts.Nodup jp.parts, j Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } ()) Finset.univ).card =
theorem Theorems100.distinctGF_prop {α : Type u_1} [] (n : ) (m : ) (h : n < m + 1) :
.card =

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

theorem Theorems100.same_gf {α : Type u_1} [] (m : ) :
* i, (1 - PowerSeries.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 Theorems100.same_coeffs {α : Type u_1} [] (m : ) (n : ) (h : n m) :
=
theorem Theorems100.partition_theorem (n : ) :
.card = .card