Mathlib.Combinatorics.Enumerative.Partition

Module docstring

{"# 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.

References

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

Nat.Partition structure

(n : ℕ)

Full source

/-- A partition of `n` is a multiset of positive integers summing to `n`. -/
@[ext]
structure Partition (n : ℕ) where
  /-- positive integers summing to `n` -/
  parts : Multiset ℕ
  /-- proof that the `parts` are positive -/
  parts_pos : ∀ {i}, i ∈ parts → 0 < i
  /-- proof that the `parts` sum to `n` -/
  parts_sum : parts.sum = n
deriving DecidableEq

Partition of a natural number

Informal description

A partition of a natural number $n$ is a multiset of positive integers whose sum is equal to $n$. Two partitions are considered the same if they differ only by the order of their parts.

Nat.instDecidableEqPartition instance

{n✝} : DecidableEq✝ (@Nat.Partition✝ n✝)

Full source

DecidableEq

Decidable Equality for Partitions of $n$

Informal description

For any natural number $n$, there is a decidable equality relation on the partitions of $n$.

Nat.Partition.decidableEqPartition instance

{n : ℕ} : DecidableEq (Partition n)

Full source

@[deprecated "Partition now derives an instance of DecidableEq." (since := "2024-12-28")]
instance decidableEqPartition {n : ℕ} : DecidableEq (Partition n) :=
  fun _ _ => decidable_of_iff' _ Partition.ext_iff

Decidable Equality for Partitions of $n$

Informal description

For any natural number $n$, there is a decidable equality relation on the partitions of $n$.

Nat.Partition.ofComposition definition

(n : ℕ) (c : Composition n) : Partition n

Full source

/-- A composition induces a partition (just convert the list to a multiset). -/
@[simps]
def ofComposition (n : ℕ) (c : Composition n) : Partition n where
  parts := c.blocks
  parts_pos hi := c.blocks_pos hi
  parts_sum := by rw [Multiset.sum_coe, c.blocks_sum]

Partition from a composition

Informal description

Given a composition $c$ of a natural number $n$, the function constructs a partition of $n$ by taking the multiset of blocks (parts) of the composition. Each block is a positive integer, and the sum of all blocks equals $n$.

Nat.Partition.ofComposition_surj theorem

{n : ℕ} : Function.Surjective (ofComposition n)

Full source

theorem ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n) := by
  rintro ⟨b, hb₁, hb₂⟩
  induction b using Quotient.inductionOn with | _ b => ?_
  exact ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext rfl⟩

Surjectivity of the Partition-from-Composition Construction

Informal description

For any natural number $n$, the function `ofComposition` that maps a composition of $n$ to its corresponding partition is surjective. In other words, every partition of $n$ can be obtained from some composition of $n$ via this function.

Nat.Partition.ofSums definition

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

Full source

/-- Given a multiset which sums to `n`, construct a partition of `n` with the same multiset, but
without the zeros.
-/
@[simps]
def ofSums (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : Partition n where
  parts := l.filter (· ≠ 0)
  parts_pos hi := (of_mem_filter hi).bot_lt
  parts_sum := by
    have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]
    rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl

Partition from a sum-matching multiset

Informal description

Given a multiset $ l $ of natural numbers whose sum is $ n $, the function constructs a partition of $ n $ by removing all zero elements from $ l $. The resulting multiset consists of positive integers that sum to $ n $.

Nat.Partition.ofMultiset definition

(l : Multiset ℕ) : Partition l.sum

Full source

/-- A `Multiset ℕ` induces a partition on its sum. -/
@[simps!]
def ofMultiset (l : Multiset ℕ) : Partition l.sum := ofSums _ l rfl

Partition from a multiset of natural numbers

Informal description

Given a multiset $ l $ of natural numbers, the function constructs a partition of the sum of the elements in $ l $. The resulting partition is obtained by removing all zero elements from $ l $, ensuring that the remaining elements are positive integers whose sum equals the original sum of $ l $.

Nat.Partition.ofSym definition

{n : ℕ} {σ : Type*} (s : Sym σ n) [DecidableEq σ] : n.Partition

Full source

/-- An element `s` of `Sym σ n` induces a partition given by its multiplicities. -/
def ofSym {n : ℕ} {σ : Type*} (s : Sym σ n) [DecidableEq σ] : n.Partition where
  parts := s.1.dedup.map s.1.count
  parts_pos := by simp [Multiset.count_pos]
  parts_sum := by
    show ∑ a ∈ s.1.toFinset, count a s.1 = n
    rw [toFinset_sum_count_eq]
    exact s.2

Partition from symmetric power multiplicities

Informal description

Given a symmetric power element `s : Sym σ n` (a multiset of size `n` with elements from type `σ`), the function constructs a partition of `n` where the parts are the multiplicities of the distinct elements in `s`. Specifically, for each distinct element in `s`, its multiplicity (count) in `s` becomes a part of the partition. The resulting partition is a multiset of positive integers (the counts) that sum to `n`.

Nat.Partition.ofSym_map theorem

(e : σ ≃ τ) (s : Sym σ n) : ofSym (s.map e) = ofSym s

Full source

@[simp] lemma ofSym_map (e : σ ≃ τ) (s : Sym σ n) :
    ofSym (s.map e) = ofSym s := by
  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, toFinset_val, mk.injEq]
  rw [Multiset.dedup_map_of_injective e.injective]
  simp only [map_map, Function.comp_apply]
  congr; funext i
  rw [← Multiset.count_map_eq_count' e _ e.injective]

Preservation of Partition Shape under Type Equivalence in Symmetric Powers

Informal description

Given an equivalence $e : \sigma \simeq \tau$ between types $\sigma$ and $\tau$, and a symmetric power element $s \in \text{Sym}\,\sigma\,n$, the partition $\text{ofSym}(s \cdot e)$ obtained by applying $e$ to $s$ is equal to the partition $\text{ofSym}(s)$ obtained from $s$ directly. In other words, the partition shape is preserved under type equivalence applied to the symmetric power elements.

Nat.Partition.ofSymShapeEquiv definition

(μ : Partition n) (e : σ ≃ τ) : { x : Sym σ n // ofSym x = μ } ≃ { x : Sym τ n // ofSym x = μ }

Full source

/-- An equivalence between `σ` and `τ` induces an equivalence between the subtypes of `Sym σ n` and
`Sym τ n` corresponding to a given partition. -/
def ofSymShapeEquiv (μ : Partition n) (e : σ ≃ τ) :
    {x : Sym σ n // ofSym x = μ}{x : Sym σ n // ofSym x = μ} ≃ {x : Sym τ n // ofSym x = μ} where
  toFun := fun x => ⟨Sym.equivCongr e x, by simp [ofSym_map, x.2]⟩
  invFun := fun x => ⟨Sym.equivCongr e.symm x, by simp [ofSym_map, x.2]⟩
  left_inv := by intro x; simp
  right_inv := by intro x; simp

Equivalence of symmetric power subsets preserving partition shape

Informal description

Given a partition $\mu$ of a natural number $n$ and an equivalence $e : \sigma \simeq \tau$ between types $\sigma$ and $\tau$, the function constructs an equivalence between the sets $\{x \in \text{Sym}\,\sigma\,n \mid \text{ofSym}\,x = \mu\}$ and $\{x \in \text{Sym}\,\tau\,n \mid \text{ofSym}\,x = \mu\}$. This is done by applying the equivalence $e$ to each element of the symmetric power via $\text{Sym.equivCongr}\,e$, with the inverse constructed similarly using the inverse equivalence $e^{-1}$. The construction ensures that applying $e$ followed by $e^{-1}$ (or vice versa) returns the original symmetric power element.

Nat.Partition.indiscrete definition

(n : ℕ) : Partition n

Full source

/-- The partition of exactly one part. -/
def indiscrete (n : ℕ) : Partition n := ofSums n {n} rfl

Indiscrete partition of $ n $

Informal description

The partition of a natural number $ n $ consisting of exactly one part, which is $ n $ itself. This is constructed as the multiset $\{n\}$ whose sum is trivially $ n $.

Nat.Partition.instInhabited instance

{n : ℕ} : Inhabited (Partition n)

Full source

instance {n : ℕ} : Inhabited (Partition n) := ⟨indiscrete n⟩

Existence of Partitions for Every Natural Number

Informal description

For any natural number $n$, the type of partitions of $n$ is inhabited.

Nat.Partition.indiscrete_parts theorem

{n : ℕ} (hn : n ≠ 0) : (indiscrete n).parts = { n }

Full source

@[simp] lemma indiscrete_parts {n : ℕ} (hn : n ≠ 0) : (indiscrete n).parts = {n} := by
  simp [indiscrete, filter_eq_self, hn]

Parts of Indiscrete Partition of Nonzero Natural Number

Informal description

For any nonzero natural number $n$, the multiset of parts of the indiscrete partition of $n$ is the singleton multiset $\{n\}$.

Nat.Partition.partition_zero_parts theorem

(p : Partition 0) : p.parts = 0

Full source

@[simp] lemma partition_zero_parts (p : Partition 0) : p.parts = 0 :=
  eq_zero_of_forall_not_mem fun _ h => (p.parts_pos h).ne' <| sum_eq_zero_iff.1 p.parts_sum _ h

Parts of the Partition of Zero are Empty

Informal description

For any partition $p$ of the natural number $0$, the multiset of parts of $p$ is equal to the empty multiset, i.e., $p.\text{parts} = \emptyset$.

Nat.Partition.UniquePartitionZero instance

: Unique (Partition 0)

Full source

instance UniquePartitionZero : Unique (Partition 0) where
  uniq _ := Partition.ext <| by simp

Uniqueness of the Partition of Zero

Informal description

The type of partitions of the natural number $0$ has exactly one element, which is the empty partition.

Nat.Partition.partition_one_parts theorem

(p : Partition 1) : p.parts = { 1 }

Full source

@[simp] lemma partition_one_parts (p : Partition 1) : p.parts = {1} := by
  have h : p.parts = replicate (card p.parts) 1 := eq_replicate_card.2 fun x hx =>
    ((le_sum_of_mem hx).trans_eq p.parts_sum).antisymm (p.parts_pos hx)
  have h' : card p.parts = 1 := by simpa using (congrArg sum h.symm).trans p.parts_sum
  rw [h, h', replicate_one]

Parts of the Partition of One are Singleton One

Informal description

For any partition $p$ of the natural number $1$, the multiset of parts of $p$ is equal to $\{1\}$.

Nat.Partition.UniquePartitionOne instance

: Unique (Partition 1)

Full source

instance UniquePartitionOne : Unique (Partition 1) where
  uniq _ := Partition.ext <| by simp

Uniqueness of the Partition of One

Informal description

The type of partitions of the natural number $1$ has exactly one element, which is the partition consisting of the single part $\{1\}$.

Nat.Partition.ofSym_one theorem

(s : Sym σ 1) : ofSym s = indiscrete 1

Full source

@[simp] lemma ofSym_one (s : Sym σ 1) : ofSym s = indiscrete 1 := by
  ext; simp

Partition from Symmetric Power of Size One is Indiscrete

Informal description

For any symmetric power element $s$ of size $1$ over a type $\sigma$, the partition constructed from $s$ is equal to the indiscrete partition of $1$, which consists of the single part $\{1\}$.

Nat.Partition.count_ofSums_of_ne_zero theorem

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

Full source

/-- 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_not_mem` gives that
this is `0` instead.)
-/
theorem count_ofSums_of_ne_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) {i : ℕ} (hi : i ≠ 0) :
    (ofSums n l hl).parts.count i = l.count i :=
  count_filter_of_pos hi

Preservation of Nonzero Count in Partition Construction

Informal description

For any natural number $n$, multiset $l$ of natural numbers with sum $n$, and nonzero natural number $i$, the count of $i$ in the parts of the partition constructed from $l$ equals the count of $i$ in $l$. That is, if $p = \text{ofSums}\,n\,l\,\text{hl}$ is the partition formed from $l$, then $\text{count}\,i\,p.\text{parts} = \text{count}\,i\,l$.

Nat.Partition.count_ofSums_zero theorem

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

Full source

theorem count_ofSums_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) :
    (ofSums n l hl).parts.count 0 = 0 :=
  count_filter_of_neg fun h => h rfl

Zero Count in Partition Parts

Informal description

For any natural number $n$ and any multiset $l$ of natural numbers such that the sum of $l$ is $n$, the count of $0$ in the parts of the partition constructed from $l$ is zero. That is, if $p$ is the partition formed from $l$ via `ofSums`, then $\text{count}\,0\,p.\text{parts} = 0$.

Nat.Partition.instFintype instance

(n : ℕ) : Fintype (Partition n)

Full source

/-- Show there are finitely many partitions by considering the surjection from compositions to
partitions.
-/
instance (n : ℕ) : Fintype (Partition n) :=
  Fintype.ofSurjective (ofComposition n) ofComposition_surj

Finiteness of Partitions of a Natural Number

Informal description

For any natural number $n$, the set of partitions of $n$ is finite.

Nat.Partition.odds definition

(n : ℕ) : Finset (Partition n)

Full source

/-- The finset of those partitions in which every part is odd. -/
def odds (n : ℕ) : Finset (Partition n) :=
  Finset.univ.filter fun c => ∀ i ∈ c.parts, ¬Even i

Partitions with odd parts

Informal description

The finset of partitions of a natural number $n$ where every part in the partition is odd. That is, for each partition $p$ in this finset, every element $i$ in the multiset $p.\text{parts}$ satisfies that $i$ is not even (i.e., $i$ is odd).

Nat.Partition.distincts definition

(n : ℕ) : Finset (Partition n)

Full source

/-- The finset of those partitions in which each part is used at most once. -/
def distincts (n : ℕ) : Finset (Partition n) :=
  Finset.univ.filter fun c => c.parts.Nodup

Partitions with distinct parts

Informal description

The finset of partitions of a natural number $n$ where each part is distinct (i.e., no part is repeated in the partition).

Nat.Partition.oddDistincts definition

(n : ℕ) : Finset (Partition n)

Full source

/-- The finset of those partitions in which every part is odd and used at most once. -/
def oddDistincts (n : ℕ) : Finset (Partition n) :=
  oddsodds n ∩ distincts n

Partitions with distinct odd parts

Informal description

The finset of partitions of a natural number $n$ where every part is odd and appears at most once. That is, for each partition $p$ in this finset, every element $i$ in the multiset $p.\text{parts}$ is odd and has multiplicity one.

Main functions

Implementation details

TODO

Tags

References