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

Equations

• Theorems100.partialOddGF m = ∏ i ∈ Finset.range m, (1 - PowerSeries.X ^ (2 * i + 1))⁻¹

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

Equations

• Theorems100.partialDistinctGF m = ∏ i ∈ Finset.range m, (1 + PowerSeries.X ^ (i + 1))

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

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

Equations

• Theorems100.indicatorSeries α s = PowerSeries.mk fun (n : ℕ) => if n ∈ s then 1 else 0

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 ^ i.succ = Theorems100.indicatorSeries α {0, i.succ}

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

def Theorems100.mkOdd : ℕ ↪ ℕ

Equations

• Theorems100.mkOdd = { toFun := fun (i : ℕ) => 2 * i + 1, inj' := Theorems100.mkOdd.proof_1 }

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

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

theorem Theorems100.oddGF_prop {α : Type u_1} [Field α] (n m : ℕ) (h : n < m * 2) : ↑(Nat.Partition.odds n).card = (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.filter (fun (p : n.Partition) => p.parts.Nodup ∧ ∀ j ∈ p.parts, j ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (Finset.range m)) Finset.univ).card = (PowerSeries.coeff α n) (Theorems100.partialDistinctGF m)

theorem Theorems100.distinctGF_prop {α : Type u_1} [CommSemiring α] (n m : ℕ) (h : n < m + 1) : ↑(Nat.Partition.distincts n).card = (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 * ∏ i ∈ Finset.range m, (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 : ℕ) : (Nat.Partition.odds n).card = (Nat.Partition.distincts n).card