Partitions

A partition of a natural number n is a way of writing n as a sum of positive integers, where the order does not matter: two sums that differ only in the order of their summands are considered the same partition. This notion is closely related to that of a composition of n, but in a composition of n the order does matter. A summand of the partition is called a part.

Main functions

• p : Partition n is a structure, made of a multiset of integers which are all positive and add up to n.

Implementation details

The main motivation for this structure and its API is to show Euler's partition theorem, and related results.

The representation of a partition as a multiset is very handy as multisets are very flexible and already have a well-developed API.

TODO

Link this to Young diagrams.

Tags

Partition

References

https://en.wikipedia.org/wiki/Partition_(number_theory)

structure Nat.Partition (n : ℕ) : Type

A partition of n is a multiset of positive integers summing to n.

• parts : Multiset ℕ

  positive integers summing to n

• parts_pos {i : ℕ} : i ∈ self.parts → 0 < i

  proof that the parts are positive

• parts_sum : self.parts.sum = n

  proof that the parts sum to n

theorem Nat.Partition.ext {n : ℕ} {x y : n.Partition} (parts : x.parts = y.parts) : x = y

theorem Nat.Partition.ext_iff {n : ℕ} {x y : n.Partition} : x = y ↔ x.parts = y.parts

def Nat.instDecidableEqPartition.decEq {n✝ : ℕ} (x✝ x✝¹ : n✝.Partition) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Nat.instDecidableEqPartition {n✝ : ℕ} : DecidableEq n✝.Partition

theorem Nat.Partition.le_of_mem_parts {n : ℕ} {p : n.Partition} {m : ℕ} (h : m ∈ p.parts) : m ≤ n

def Nat.Partition.ofComposition (n : ℕ) (c : Composition n) : n.Partition

A composition induces a partition (just convert the list to a multiset).

@[simp]

theorem Nat.Partition.ofComposition_parts (n : ℕ) (c : Composition n) : (ofComposition n c).parts = ↑c.blocks

theorem Nat.Partition.ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n)

def Nat.Partition.ofSums (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : n.Partition

Given a multiset which sums to n, construct a partition of n with the same multiset, but without the zeros.

@[simp]

theorem Nat.Partition.ofSums_parts (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : (ofSums n l hl).parts = Multiset.filter (fun (x : ℕ) => x ≠ 0) l

def Nat.Partition.ofMultiset (l : Multiset ℕ) : l.sum.Partition

A Multiset ℕ induces a partition on its sum.

@[simp]

theorem Nat.Partition.ofMultiset_parts (l : Multiset ℕ) : (ofMultiset l).parts = Multiset.filter (fun (x : ℕ) => ¬x = 0) l

def Nat.Partition.ofSym {n : ℕ} {σ : Type u_1} (s : Sym σ n) [DecidableEq σ] : n.Partition

An element s of Sym σ n induces a partition given by its multiplicities.

@[simp]

theorem Nat.Partition.ofSym_map {n : ℕ} {σ : Type u_1} {τ : Type u_2} [DecidableEq σ] [DecidableEq τ] (e : σ ≃ τ) (s : Sym σ n) : ofSym (Sym.map (⇑e) s) = ofSym s

def Nat.Partition.ofSymShapeEquiv {n : ℕ} {σ : Type u_1} {τ : Type u_2} [DecidableEq σ] [DecidableEq τ] (μ : n.Partition) (e : σ ≃ τ) : { x : Sym σ n // ofSym x = μ } ≃ { x : Sym τ n // ofSym x = μ }

An equivalence between σ and τ induces an equivalence between the subtypes of Sym σ n and Sym τ n corresponding to a given partition.

def Nat.Partition.toFinsuppAntidiag {n : ℕ} (p : n.Partition) : ℕ →₀ ℕ

Convert a Partition n to a member of (Finset.Icc 1 n).finsuppAntidiag n (see Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag for the proof). p.toFinsuppAntidiag i is defined as i times the number of occurrence of i in p.

theorem Nat.Partition.toFinsuppAntidiag_injective (n : ℕ) : Function.Injective toFinsuppAntidiag

theorem Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag {n : ℕ} (p : n.Partition) : p.toFinsuppAntidiag ∈ (Finset.Icc 1 n).finsuppAntidiag n

def Nat.Partition.indiscrete (n : ℕ) : n.Partition

The partition of exactly one part.

@[implicit_reducible]

instance Nat.Partition.instInhabited {n : ℕ} : Inhabited n.Partition

@[simp]

theorem Nat.Partition.indiscrete_parts {n : ℕ} (hn : n ≠ 0) : (indiscrete n).parts = {n}

@[simp]

theorem Nat.Partition.partition_zero_parts (p : Partition 0) : p.parts = 0

@[implicit_reducible]

instance Nat.Partition.UniquePartitionZero : Unique (Partition 0)

@[simp]

theorem Nat.Partition.partition_one_parts (p : Partition 1) : p.parts = {1}

@[implicit_reducible]

instance Nat.Partition.UniquePartitionOne : Unique (Partition 1)

@[simp]

theorem Nat.Partition.ofSym_one {σ : Type u_1} [DecidableEq σ] (s : Sym σ 1) : ofSym s = indiscrete 1

theorem Nat.Partition.count_ofSums_of_ne_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) {i : ℕ} (hi : i ≠ 0) : Multiset.count i (ofSums n l hl).parts = Multiset.count i l

The number of times a positive integer i appears in the partition ofSums n l hl is the same as the number of times it appears in the multiset l. (For i = 0, Partition.non_zero combined with Multiset.count_eq_zero_of_notMem gives that this is 0 instead.)

theorem Nat.Partition.count_ofSums_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) : Multiset.count 0 (ofSums n l hl).parts = 0

@[implicit_reducible]

instance Nat.Partition.instFintype (n : ℕ) : Fintype n.Partition

Show there are finitely many partitions by considering the surjection from compositions to partitions.

def Nat.Partition.restricted (n : ℕ) (p : ℕ → Prop) [DecidablePred p] : Finset n.Partition

The finset of those partitions in which every part satisfies a certain condition.

def Nat.Partition.countRestricted (n m : ℕ) : Finset n.Partition

The finset of those partitions in which every part is used less than m times.

def Nat.Partition.odds (n : ℕ) : Finset n.Partition

The finset of those partitions in which every part is odd.

def Nat.Partition.distincts (n : ℕ) : Finset n.Partition

The finset of those partitions in which each part is used at most once.

theorem Nat.Partition.countRestricted_two (n : ℕ) : countRestricted n 2 = distincts n

def Nat.Partition.oddDistincts (n : ℕ) : Finset n.Partition

The finset of those partitions in which every part is odd and used at most once.