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 : ℕ) [Field α] : PowerSeries α

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

def Theorems100.partialDistinctGF {α : Type u_1} (m : ℕ) [CommSemiring α] : PowerSeries α

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

def Theorems100.cut {ι : Type u_1} (s : Finset ι) (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.

theorem Theorems100.mem_cut {ι : Type u_1} (s : Finset ι) (n : ℕ) (f : ι → ℕ) : f ∈ Theorems100.cut s n ↔ Finset.sum s f = n ∧ ∀ (i : ι), ¬i ∈ s → f i = 0

theorem Theorems100.cut_equiv_antidiag (n : ℕ) : ↑(Equiv.finsetCongr (Equiv.boolArrowEquivProd ℕ)) (Theorems100.cut Finset.univ n) = Finset.Nat.antidiagonal n

theorem Theorems100.cut_univ_fin_eq_antidiagonalTuple (n : ℕ) (k : ℕ) : Theorems100.cut Finset.univ n = Finset.Nat.antidiagonalTuple k n

@[simp]

theorem Theorems100.cut_zero {ι : Type u_1} (s : Finset ι) : Theorems100.cut s 0 = {0}

There is only one cut of 0.

@[simp]

theorem Theorems100.cut_empty_succ {ι : Type u_1} (n : ℕ) : Theorems100.cut ∅ (n + 1) = ∅

theorem Theorems100.cut_insert {ι : Type u_1} (n : ℕ) (a : ι) (s : Finset ι) (h : ¬a ∈ s) : Theorems100.cut (insert a s) n = Finset.biUnion (Finset.Nat.antidiagonal n) 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} [CommSemiring α] {ι : Type u_2} (s : Finset ι) (f : ι → PowerSeries α) (n : ℕ) : ↑(PowerSeries.coeff α n) (Finset.prod s fun j => f j) = Finset.sum (Theorems100.cut s n) fun l => Finset.prod s fun i => ↑(PowerSeries.coeff α (l i)) (f i)

def Theorems100.indicatorSeries (α : Type u_1) [Semiring α] (s : Set ℕ) : PowerSeries α

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

theorem Theorems100.coeff_indicator {α : Type u_1} (s : Set ℕ) [Semiring α] (n : ℕ) : ↑(PowerSeries.coeff α n) (Theorems100.indicatorSeries α s) = if n ∈ s then 1 else 0

theorem Theorems100.coeff_indicator_pos {α : Type u_1} (s : Set ℕ) [Semiring α] (n : ℕ) (h : n ∈ s) : ↑(PowerSeries.coeff α n) (Theorems100.indicatorSeries α s) = 1

theorem Theorems100.coeff_indicator_neg {α : Type u_1} (s : Set ℕ) [Semiring α] (n : ℕ) (h : ¬n ∈ s) : ↑(PowerSeries.coeff α n) (Theorems100.indicatorSeries α s) = 0

theorem Theorems100.constantCoeff_indicator {α : Type u_1} (s : Set ℕ) [Semiring α] : ↑(PowerSeries.constantCoeff α) (Theorems100.indicatorSeries α s) = if 0 ∈ s then 1 else 0

theorem Theorems100.two_series {α : Type u_1} (i : ℕ) [Semiring α] : 1 + PowerSeries.X ^ Nat.succ i = Theorems100.indicatorSeries α {0, Nat.succ i}

theorem Theorems100.num_series' {α : Type u_1} [Field α] (i : ℕ) : (1 - PowerSeries.X ^ (i + 1))⁻¹ = Theorems100.indicatorSeries α {k | i + 1 ∣ k}

def Theorems100.mkOdd : ℕ ↪ ℕ

theorem Theorems100.partialGF_prop (α : Type u_1) [CommSemiring α] (n : ℕ) (s : Finset ℕ) (hs : ∀ (i : ℕ), i ∈ s → 0 < i) (c : ℕ → Set ℕ) (hc : ∀ (i : ℕ), ¬i ∈ s → 0 ∈ c i) : ↑(Finset.card (Finset.filter (fun p => (∀ (j : ℕ), Multiset.count j p.parts ∈ c j) ∧ ∀ (j : ℕ), j ∈ p.parts → j ∈ s) Finset.univ)) = ↑(PowerSeries.coeff α n) (Finset.prod s fun i => Theorems100.indicatorSeries α ((fun x => x * i) '' c i))

theorem Theorems100.partialOddGF_prop {α : Type u_1} [Field α] (n : ℕ) (m : ℕ) : ↑(Finset.card (Finset.filter (fun p => ∀ (j : ℕ), j ∈ p.parts → j ∈ Finset.map Theorems100.mkOdd (Finset.range m)) Finset.univ)) = ↑(PowerSeries.coeff α n) (Theorems100.partialOddGF m)

theorem Theorems100.oddGF_prop {α : Type u_1} [Field α] (n : ℕ) (m : ℕ) (h : n < m * 2) : ↑(Finset.card (Nat.Partition.odds n)) = ↑(PowerSeries.coeff α n) (Theorems100.partialOddGF m)

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

theorem Theorems100.partialDistinctGF_prop {α : Type u_1} [CommSemiring α] (n : ℕ) (m : ℕ) : ↑(Finset.card (Finset.filter (fun p => Multiset.Nodup p.parts ∧ ∀ (j : ℕ), j ∈ p.parts → j ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (Finset.range m)) Finset.univ)) = ↑(PowerSeries.coeff α n) (Theorems100.partialDistinctGF m)

theorem Theorems100.distinctGF_prop {α : Type u_1} [CommSemiring α] (n : ℕ) (m : ℕ) (h : n < m + 1) : ↑(Finset.card (Nat.Partition.distincts n)) = ↑(PowerSeries.coeff α n) (Theorems100.partialDistinctGF m)

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

theorem Theorems100.same_gf {α : Type u_1} [Field α] (m : ℕ) : (Theorems100.partialOddGF m * Finset.prod (Finset.range m) fun i => 1 - PowerSeries.X ^ (m + i + 1)) = Theorems100.partialDistinctGF m

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} [Field α] (m : ℕ) (n : ℕ) (h : n ≤ m) : ↑(PowerSeries.coeff α n) (Theorems100.partialOddGF m) = ↑(PowerSeries.coeff α n) (Theorems100.partialDistinctGF m)

theorem Theorems100.partition_theorem (n : ℕ) : Finset.card (Nat.Partition.odds n) = Finset.card (Nat.Partition.distincts n)