# Documentation

Archive.Wiedijk100Theorems.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 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 ℝ.

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 ℝ.

Instances For
def Theorems100.cut {ι : Type u_1} (s : ) (n : ) :
Finset (ι)

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.antidiagonalTuple where antidiagonalTuple k n is the same thing as cut (s : Finset.univ (Fin k)) n.

Instances For
theorem Theorems100.mem_cut {ι : Type u_1} (s : ) (n : ) (f : ι) :
f = n ∀ (i : ι), ¬i sf i = 0
theorem Theorems100.cut_equiv_antidiag (n : ) :
↑() (Theorems100.cut Finset.univ n) =
@[simp]
theorem Theorems100.cut_zero {ι : Type u_1} (s : ) :
= {0}

There is only one cut of 0.

@[simp]
theorem Theorems100.cut_empty_succ {ι : Type u_1} (n : ) :
theorem Theorems100.cut_insert {ι : Type u_1} (n : ) (a : ι) (s : ) (h : ¬a s) :
Theorems100.cut (insert a s) n = Finset.biUnion () fun p => Finset.map { toFun := fun f => f + fun t => if t = a then p.fst else 0, inj' := (_ : Function.Injective fun x => x + fun t => if t = a then p.fst else 0) } (Theorems100.cut s p.snd)
theorem Theorems100.coeff_prod_range {α : Type u_1} [] {ι : Type u_2} (s : ) (f : ι) (n : ) :
↑() (Finset.prod s fun j => f j) = Finset.sum () fun l => Finset.prod s fun i => ↑(PowerSeries.coeff α (l i)) (f i)
def Theorems100.indicatorSeries (α : Type u_1) [] (s : ) :

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

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 : ¬n s) :
↑() () = 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 ^ =
theorem Theorems100.num_series' {α : Type u_1} [] (i : ) :
(1 - PowerSeries.X ^ (i + 1))⁻¹ = Theorems100.indicatorSeries α {k | i + 1 k}
Instances For
theorem Theorems100.partialGF_prop (α : Type u_1) [] (n : ) (s : ) (hs : ∀ (i : ), i s0 < i) (c : ) (hc : ∀ (i : ), ¬i s0 c i) :
↑(Finset.card (Finset.filter (fun p => (∀ (j : ), Multiset.count j p.parts c j) ∀ (j : ), j p.partsj s) Finset.univ)) = ↑() (Finset.prod s fun i => Theorems100.indicatorSeries α ((fun x => x * i) '' c i))
theorem Theorems100.partialOddGF_prop {α : Type u_1} [] (n : ) (m : ) :
↑(Finset.card (Finset.filter (fun p => ∀ (j : ), j p.parts) Finset.univ)) = ↑() ()
theorem Theorems100.oddGF_prop {α : Type u_1} [] (n : ) (m : ) (h : n < m * 2) :
↑() = ↑() ()

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.card (Finset.filter (fun p => Multiset.Nodup p.parts ∀ (j : ), j p.partsj Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } ()) Finset.univ)) = ↑() ()
theorem Theorems100.distinctGF_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 Theorems100.same_gf {α : Type u_1} [] (m : ) :
( * Finset.prod () fun 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) :
↑() () = ↑() ()