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

Instances For

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

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

        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 : 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)

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

        Instances For
          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) :
          theorem Theorems100.coeff_indicator_neg {α : Type u_1} (s : Set ) [Semiring α] (n : ) (h : ¬n s) :
          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}
          theorem Theorems100.partialGF_prop (α : Type u_1) [CommSemiring α] (n : ) (s : Finset ) (hs : ∀ (i : ), i s0 < i) (c : Set ) (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)) = ↑(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.partsj 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) :

          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.partsj Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (Finset.range m)) Finset.univ)) = ↑(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 : ) :

          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.