mathlib3 documentation

combinatorics.partition

Partitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Tags #

Partition

References #

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

@[protected, instance]

def nat.partition.decidable_eq (n : ℕ) :

decidable_eq n.partition

theorem nat.partition.ext_iff {n : ℕ} (x y : n.partition) :

x = y ↔ x.parts = y.parts

theorem nat.partition.ext {n : ℕ} (x y : n.partition) (h : x.parts = y.parts) :

x = y

@[ext]

structure nat.partition (n : ℕ) :

parts : multiset ℕ
parts_pos : ∀ {i : ℕ}, i ∈ self.parts → 0 < i
parts_sum : self.parts.sum = n

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

Instances for nat.partition

nat.partition.has_sizeof_inst
nat.partition.inhabited
nat.partition.fintype

def nat.partition.of_composition (n : ℕ) (c : composition n) :

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

Equations

nat.partition.of_composition n c = {parts := ↑(c.blocks), parts_pos := _, parts_sum := _}

theorem nat.partition.of_composition_surj {n : ℕ} :

function.surjective (nat.partition.of_composition n)

def nat.partition.of_sums (n : ℕ) (l : multiset ℕ) (hl : l.sum = n) :

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

Equations

nat.partition.of_sums n l hl = {parts := multiset.filter (λ (_x : ℕ), _x ≠ 0) l, parts_pos := _, parts_sum := _}

def nat.partition.of_multiset (l : multiset ℕ) :

l.sum.partition

A multiset ℕ induces a partition on its sum.

Equations

nat.partition.of_multiset l = nat.partition.of_sums l.sum l _

def nat.partition.indiscrete_partition (n : ℕ) :

The partition of exactly one part.

Equations

nat.partition.indiscrete_partition n = nat.partition.of_sums n {n} _

@[protected, instance]

def nat.partition.inhabited {n : ℕ} :

inhabited n.partition

Equations

nat.partition.inhabited = {default := nat.partition.indiscrete_partition n}

theorem nat.partition.count_of_sums_of_ne_zero {n : ℕ} {l : multiset ℕ} (hl : l.sum = n) {i : ℕ} (hi : i ≠ 0) :

multiset.count i (nat.partition.of_sums n l hl).parts = multiset.count i l

The number of times a positive integer i appears in the partition of_sums 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_not_mem gives that this is 0 instead.)

theorem nat.partition.count_of_sums_zero {n : ℕ} {l : multiset ℕ} (hl : l.sum = n) :

multiset.count 0 (nat.partition.of_sums n l hl).parts = 0

@[protected, instance]

def nat.partition.fintype (n : ℕ) :

fintype n.partition

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

Equations

nat.partition.fintype n = fintype.of_surjective (nat.partition.of_composition n) nat.partition.of_composition_surj

def nat.partition.odds (n : ℕ) :

finset n.partition

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

Equations

nat.partition.odds n = finset.filter (λ (c : n.partition), ∀ (i : ℕ), i ∈ c.parts → ¬even i) finset.univ

def nat.partition.distincts (n : ℕ) :

finset n.partition

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

Equations

nat.partition.distincts n = finset.filter (λ (c : n.partition), c.parts.nodup) finset.univ

def nat.partition.odd_distincts (n : ℕ) :

finset n.partition

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

Equations

nat.partition.odd_distincts n = nat.partition.odds n ∩ nat.partition.distincts n