Partition basics

This file formalizes the basic theory of integer partitions from Section "Partition basics" of the Algebraic Combinatorics textbook.

Main definitions

• IversonBracket.iverson - the Iverson bracket [P] converting propositions to 0 or 1
• FloorCeiling.floor_def - the floor function ⌊a⌋ (largest integer ≤ a)
• FloorCeiling.ceil_def - the ceiling function ⌈a⌉ (smallest integer ≥ a)
• Nat.Partition.partitionCount - the partition function p(n), counting partitions of n
• Nat.Partition.partsCount - the function p_k(n), counting partitions of n into k parts
• Nat.Partition.largestPart - the largest part of a partition (0 for the empty partition)
• Nat.Partition.transpose - the conjugate/transpose of a partition
• Nat.Partition.partsLeqCount - count of partitions with parts ≤ m
• Nat.Partition.partsInCount - count of partitions with parts in a set I

Main results

Integer partitions (Definition \ref{def.pars.parts})

• Nat.Partition.size_eq - The size of a partition equals the sum of parts (Definition \ref{def.pars.parts} (c))
• Nat.Partition.parts_pos' - All parts are positive (Definition \ref{def.pars.parts} (a))
• Nat.Partition.parts_le - Each part is bounded by the size
• Nat.Partition.parts_eq_zero_of_partition_zero - The partition of 0 has no parts
• Nat.Partition.parts_card_zero - The partition of 0 has length 0
• Nat.Partition.indiscrete_parts_card - The indiscrete partition (n) has one part
• Nat.Partition.ofList' - Construct a partition from a list of positive integers
• Nat.Partition.eq_iff_parts_eq - Partitions are determined by their parts

Iverson bracket (Definition \ref{def.pars.iverson})

• IversonBracket.iverson - [P] = 1 if P is true, [P] = 0 if P is false
• IversonBracket.iverson_true - [P] = 1 when P is true
• IversonBracket.iverson_false - [P] = 0 when P is false
• IversonBracket.kronecker_eq_iverson - Kronecker delta δ_{i,j} = [i = j]
• IversonBracket.sum_iverson_eq_card - ∑ [P(x)] = |{x : P(x)}|
• IversonBracket.iverson_and - [P ∧ Q] = [P] * [Q]
• IversonBracket.iverson_not - [¬P] = 1 - [P]
• IversonBracket.iverson_or - [P ∨ Q] = [P] + [Q] - [P] * [Q]
• IversonBracket.iverson_imp - [P → Q] = 1 - [P] * (1 - [Q])

Floor and ceiling (Definition \ref{def.pars.floor-ceil})

• FloorCeiling.floor_def - n ≤ ⌊a⌋ ↔ n ≤ a (characterization of floor)
• FloorCeiling.ceil_def - ⌈a⌉ ≤ n ↔ a ≤ n (characterization of ceiling)
• FloorCeiling.floor_of_int - ⌊n⌋ = n for integers
• FloorCeiling.ceil_of_int - ⌈n⌉ = n for integers
• FloorCeiling.nat_div_eq_floor - n / m = ⌊n/m⌋ for natural numbers

Basic properties (Proposition \ref{prop.pars.basics})

• Nat.Partition.partsCount_of_gt - p_k(n) = 0 when k > n
• Nat.Partition.partsCount_of_gt' - @[simp] lemma for p_k(n) = 0 when n < k
• Nat.Partition.partsCount_eq_zero_iff - p_k(n) = 0 iff k > n or k = 0 ∧ n > 0
• Nat.Partition.partsCount_zero - p_0(n) = [n = 0]
• Nat.Partition.partsCount_one - p_1(n) = [n > 0]
• Nat.Partition.partsCount_recurrence - p_k(n) = p_k(n-k) + p_{k-1}(n-1) for k > 0 and n > 0
• Nat.Partition.partsCount_two - p_2(n) = ⌊n/2⌋ for n ∈ ℕ
• Nat.Partition.partitionCount_sum - p(n) = p_0(n) + p_1(n) + ... + p_n(n) for n ∈ ℕ

Generating functions (Theorems \ref{thm.pars.main-gf}, \ref{thm.pars.main-gf-parts-n}, \ref{thm.pars.main-gf-parts-I}, \ref{thm.pars.main-gf-0n})

• Nat.Partition.partitionCount_genFun - ∑ p(n) x^n = ∏_{k≥1} 1/(1-x^k)
• Nat.Partition.partitionCount_genFun_partsLeq - ∑ p_{parts≤m}(n) x^n = ∏_{k=1}^m 1/(1-x^k)
• Nat.Partition.partitionCount_genFun_partsIn - ∑ p_I(n) x^n = ∏_{k∈I} 1/(1-x^k)
• Nat.Partition.partsCountSum_genFun - ∑ (p_0(n) + ... + p_m(n)) x^n = ∏_{k=1}^m 1/(1-x^k)

Odd-distinct theorem (Theorem \ref{thm.pars.odd-dist-equal})

• Nat.Partition.card_odds_eq_card_distincts - Euler's odd-distinct identity (from Mathlib)

Conjugation (Proposition \ref{prop.pars.pkn=dual})

• Nat.Partition.partsCount_eq_largestPartCount - p_k(n) = #{ partitions of n with largest part k }

Counting by parts and largest (Proposition \ref{prop.pars.qbinom.intro-count-binom})

• Nat.Partition.partsAndLargestCountTotal_eq - #{ partitions with k parts and largest ℓ } = C(k+ℓ-2, k-1)

Partition numbers and divisor sums (Theorem \ref{thm.pars.sigma1})

• Nat.Partition.partitionCount_divisorSum - n·p(n) = ∑_{k=1}^n σ(k)·p(n-k)

Implementation notes

We use Mathlib's Nat.Partition type which represents a partition as a multiset of positive integers. This is equivalent to the "weakly decreasing tuple" representation in the source text.

The functions partsCount and partitionCount are defined as cardinalities of finite sets, which automatically ensures they are nonnegative. For negative n, there are no partitions, so these functions return 0 naturally.

The generating function theorems use Mathlib's HasProd to express convergent infinite products in the power series topology. The identity ∏_{k≥1} 1/(1-x^k) is expressed as ∏_{k≥1} ∑_{j≥0} x^{kj} since the geometric series 1/(1-x^k) = ∑_{j≥0} x^{kj}.

References

• The source text: Algebraic Combinatorics, Section on Partition Basics
• Mathlib: Mathlib.Combinatorics.Enumerative.Partition.Basic
• Mathlib: Mathlib.Combinatorics.Enumerative.Partition.GenFun
• Mathlib: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Iverson bracket notation (Definition \ref{def.pars.iverson})

The Iverson bracket notation represents the truth value of a proposition P:

• 1 if P is true
• 0 if P is false

In Lean, this is represented as if P then 1 else 0 or equivalently (decide P).toNat.

The Kronecker delta δ_{i,j} is a special case: δ_{i,j} = [i = j].

@[reducible, inline]

abbrev IversonBracket.iverson (P : Prop) [Decidable P] {α : Type u_1} [Zero α] [One α] : α

The Iverson bracket converts a proposition to its truth value (0 or 1). (Definition \ref{def.pars.iverson})

This is the standard way to embed boolean values into a semiring:

• 1 if P is true
• 0 if P is false

In Mathlib, this is if P then 1 else 0 or (decide P).toNat for naturals.

Equations

• IversonBracket.iverson P = if P then 1 else 0

def IversonBracket.«term⦃_⦄» : Lean.ParserDescr

Notation ⦃P⦄ for the Iverson bracket.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IversonBracket.iverson_true {α : Type u_1} [Zero α] [One α] {P : Prop} [Decidable P] (h : P) : iverson P = 1

The Iverson bracket of a true proposition is 1.

@[simp]

theorem IversonBracket.iverson_false {α : Type u_1} [Zero α] [One α] {P : Prop} [Decidable P] (h : ¬P) : iverson P = 0

The Iverson bracket of a false proposition is 0.

theorem IversonBracket.iverson_eq_one_iff {α : Type u_1} [Zero α] [One α] [NeZero 1] {P : Prop} [Decidable P] : iverson P = 1 ↔ P

The Iverson bracket equals 1 iff the proposition is true.

theorem IversonBracket.iverson_eq_zero_iff {α : Type u_1} [Zero α] [One α] [NeZero 1] {P : Prop} [Decidable P] : iverson P = 0 ↔ ¬P

The Iverson bracket equals 0 iff the proposition is false (assuming 1 ≠ 0).

theorem IversonBracket.kronecker_eq_iverson {α : Type u_1} [DecidableEq α] {R : Type u_2} [Zero R] [One R] (i j : α) : (if i = j then 1 else 0) = iverson (i = j)

The Kronecker delta is a special case of the Iverson bracket: δ_{i,j} = [i = j].

In Mathlib, this is represented by Pi.single i 1 j for dependent functions, or if i = j then 1 else 0 directly.

theorem IversonBracket.iverson_nat_eq_toNat (P : Prop) [Decidable P] : iverson P = (decide P).toNat

The Iverson bracket for natural numbers equals Bool.toNat of the decision.

theorem IversonBracket.sum_iverson_eq_card {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] : ∑ x ∈ s, iverson (p x) = (Finset.filter p s).card

Sum of Iverson brackets equals cardinality of the filtered set.

theorem IversonBracket.iverson_and {α : Type u_1} [MulZeroOneClass α] {P Q : Prop} [Decidable P] [Decidable Q] : iverson (P ∧ Q) = iverson P * iverson Q

The Iverson bracket is multiplicative for conjunctions: [P ∧ Q] = [P] * [Q] when the propositions are decidable.

theorem IversonBracket.iverson_sq {α : Type u_1} [MonoidWithZero α] {P : Prop} [Decidable P] : iverson P ^ 2 = iverson P

The Iverson bracket satisfies [P]² = [P] (idempotent under multiplication).

theorem IversonBracket.iverson_not {α : Type u_1} [Ring α] [NeZero 1] {P : Prop} [Decidable P] : (iverson ¬P) = 1 - iverson P

The Iverson bracket of a negation: [¬P] = 1 - [P]. This requires 1 ≠ 0 in the ring.

theorem IversonBracket.iverson_or {α : Type u_1} [Ring α] {P Q : Prop} [Decidable P] [Decidable Q] : iverson (P ∨ Q) = iverson P + iverson Q - iverson P * iverson Q

The Iverson bracket of a disjunction: [P ∨ Q] = [P] + [Q] - [P] * [Q]. This is the inclusion-exclusion principle for Iverson brackets.

theorem IversonBracket.iverson_imp {α : Type u_1} [Ring α] {P Q : Prop} [Decidable P] [Decidable Q] : iverson (P → Q) = 1 - iverson P * (1 - iverson Q)

The Iverson bracket of an implication: [P → Q] = 1 - [P] * (1 - [Q]) = 1 - [P] * [¬Q]. Equivalently, [P → Q] = 1 - [P] + [P] * [Q].

Floor and ceiling functions (Definition \ref{def.pars.floor-ceil})

The floor of a real number a, denoted ⌊a⌋, is the largest integer that is ≤ a. The ceiling of a real number a, denoted ⌈a⌉, is the smallest integer that is ≥ a.

In Mathlib, these are provided by the FloorRing and FloorSemiring typeclasses:

• Int.floor gives the floor as an integer
• Int.ceil gives the ceiling as an integer
• Nat.floor gives the floor as a natural number (for nonnegative inputs)
• Nat.ceil gives the ceiling as a natural number (for nonnegative inputs)

The notation ⌊a⌋ and ⌈a⌉ is available via import Mathlib.

Definition (def.pars.floor-ceil)

Let a be a real number.

• ⌊a⌋ (the floor of a) is the largest integer that is ≤ a.
• ⌈a⌉ (the ceiling of a) is the smallest integer that is ≥ a.

These are formalized in Mathlib as Int.floor and Int.ceil.

theorem FloorCeiling.floor_def (a : ℝ) (n : ℤ) : n ≤ ⌊a⌋ ↔ ↑n ≤ a

The floor of a real number is the largest integer ≤ a. (Definition \ref{def.pars.floor-ceil})

This is the characterization: n ≤ ⌊a⌋ iff n ≤ a.

theorem FloorCeiling.ceil_def (a : ℝ) (n : ℤ) : ⌈a⌉ ≤ n ↔ a ≤ ↑n

The ceiling of a real number is the smallest integer ≥ a. (Definition \ref{def.pars.floor-ceil})

This is the characterization: ⌈a⌉ ≤ n iff a ≤ n.

theorem FloorCeiling.floor_le (a : ℝ) : ↑⌊a⌋ ≤ a

The floor is at most the original number.

theorem FloorCeiling.le_ceil (a : ℝ) : a ≤ ↑⌈a⌉

The original number is at most the ceiling.

theorem FloorCeiling.floor_le_ceil (a : ℝ) : ⌊a⌋ ≤ ⌈a⌉

The floor is at most the ceiling.

theorem FloorCeiling.floor_of_int (n : ℤ) : ⌊↑n⌋ = n

The floor of an integer is itself. (Example from the textbook: ⌊n⌋ = n for n ∈ ℤ)

theorem FloorCeiling.ceil_of_int (n : ℤ) : ⌈↑n⌉ = n

The ceiling of an integer is itself. (Example from the textbook: ⌈n⌉ = n for n ∈ ℤ)

theorem FloorCeiling.floor_eq_ceil_of_int (n : ℤ) : ⌊↑n⌋ = ⌈↑n⌉

For integers, floor equals ceiling. (Example from the textbook: ⌊n⌋ = ⌈n⌉ = n for n ∈ ℤ)

Examples from the textbook

The textbook gives π ≈ 3.14 as an example. We use 3.14 directly as a rational.

Connection to natural number division

theorem FloorCeiling.nat_div_eq_floor (n m : ℕ) (_hm : m ≠ 0) : n / m = ⌊↑n / ↑m⌋₊

Natural number division equals the floor of rational division. This connects n / m (natural number division) to ⌊n/m⌋ (floor of rational division).

Additional properties

theorem FloorCeiling.floor_add_int (a : ℝ) (n : ℤ) : ⌊a + ↑n⌋ = ⌊a⌋ + n

Floor of a sum: ⌊a + n⌋ = ⌊a⌋ + n for integer n.

theorem FloorCeiling.ceil_add_int (a : ℝ) (n : ℤ) : ⌈a + ↑n⌉ = ⌈a⌉ + n

Ceiling of a sum: ⌈a + n⌉ = ⌈a⌉ + n for integer n.

theorem FloorCeiling.floor_mono {a b : ℝ} (h : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋

Floor is monotone: a ≤ b implies ⌊a⌋ ≤ ⌊b⌋.

theorem FloorCeiling.ceil_mono {a b : ℝ} (h : a ≤ b) : ⌈a⌉ ≤ ⌈b⌉

Ceiling is monotone: a ≤ b implies ⌈a⌉ ≤ ⌈b⌉.

theorem FloorCeiling.fract_nonneg (a : ℝ) : 0 ≤ a - ↑⌊a⌋

The fractional part of a real number: a - ⌊a⌋ ∈ [0, 1).

theorem FloorCeiling.fract_lt_one (a : ℝ) : a - ↑⌊a⌋ < 1

The fractional part of a real number: a - ⌊a⌋ < 1.

theorem FloorCeiling.ceil_eq_floor_add_one_iff (a : ℝ) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ≠ ↑⌊a⌋

Relationship between floor and ceiling: ⌈a⌉ = ⌊a⌋ + 1 iff a is not an integer.

theorem FloorCeiling.floor_eq_ceil_iff (a : ℝ) : ⌊a⌋ = ⌈a⌉ ↔ a = ↑⌊a⌋

When a is an integer, floor equals ceiling.

Definition of integer partitions (Definition \ref{def.pars.parts})

This section formalizes Definition \ref{def.pars.parts} from the source text.

In Mathlib, Nat.Partition n represents partitions of n. The underlying data is a multiset of positive integers that sums to n. This is equivalent to the "weakly decreasing tuple" representation in the source text:

Definition \ref{def.pars.parts}:

(a) An (integer) partition means a (finite) weakly decreasing tuple of positive integers -- i.e., a finite tuple (λ₁, λ₂, ..., λₘ) of positive integers such that λ₁ ≥ λ₂ ≥ ... ≥ λₘ.

(b) The parts of a partition (λ₁, λ₂, ..., λₘ) are simply its entries λ₁, λ₂, ..., λₘ.

(c) Let n ∈ ℤ. A partition of n means a partition whose size is n.

(d) Let n ∈ ℤ and k ∈ ℕ. A partition of n into k parts is a partition whose size is n and whose length is k.

Implementation note: Mathlib uses multisets rather than tuples, which is equivalent since partitions are determined by their parts (with multiplicity), regardless of order. The "weakly decreasing" constraint in the tuple representation is automatically satisfied when we sort the multiset in decreasing order.

Parts of a partition (Definition \ref{def.pars.parts} (b))

In Mathlib, Partition.parts returns the multiset of parts. Each part is a positive integer (guaranteed by parts_pos), and the sum of parts equals the size (guaranteed by parts_sum).

The parts are the fundamental data of a partition. They are positive integers whose sum equals the size n. We use Mathlib's Partition.parts directly rather than redefining it, and provide wrapper lemmas for the key properties.

theorem Nat.Partition.size_eq {n : ℕ} (p : n.Partition) : p.parts.sum = n

The size of a partition is the sum of its parts. (Definition \ref{def.pars.parts} (c))

For a partition of n, the size is n. This is guaranteed by Partition.parts_sum. The type Partition n itself encodes that the partition has size n.

theorem Nat.Partition.parts_pos' {n : ℕ} (p : n.Partition) (i : ℕ) (hi : i ∈ p.parts) : 0 < i

All parts of a partition are positive. (Definition \ref{def.pars.parts} (a) - "tuple of positive integers")

This is a fundamental property: every entry in a partition is ≥ 1. This is the defining property that distinguishes partitions from weak compositions.

theorem Nat.Partition.parts_le {n : ℕ} (p : n.Partition) (i : ℕ) (hi : i ∈ p.parts) : i ≤ n

A partition of n has all parts ≤ n. (Consequence of Definition \ref{def.pars.parts})

Since parts are positive and sum to n, each individual part is bounded by n.

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

The empty partition is the unique partition of 0. (Definition \ref{def.pars.parts} (a) - empty tuple case)

The partition of 0 has no parts.

theorem Nat.Partition.parts_card_zero (p : Partition 0) : p.parts.card = 0

The length of the partition of 0 is 0. (Definition \ref{def.pars.parts} (a) - empty tuple has length 0)

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

For n > 0, the indiscrete partition (n) has exactly one part. (Example of Definition \ref{def.pars.parts})

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

The parts of the indiscrete partition (n) for n > 0. (Example of Definition \ref{def.pars.parts})

def Nat.Partition.ofList' {n : ℕ} (l : List ℕ) (hl_pos : ∀ i ∈ l, 0 < i) (hl_sum : l.sum = n) : n.Partition

Constructing a partition from a list of positive integers. (Definition \ref{def.pars.parts} (a) - the tuple representation)

Given a list of positive integers that sums to n, we can construct a partition of n. The list need not be sorted; Mathlib's Partition uses multisets.

Equations

• Nat.Partition.ofList' l hl_pos hl_sum = { parts := ↑l, parts_pos := ⋯, parts_sum := ⋯ }

@[simp]

theorem Nat.Partition.ofList'_parts {n : ℕ} (l : List ℕ) (hl_pos : ∀ i ∈ l, 0 < i) (hl_sum : l.sum = n) : (ofList' l hl_pos hl_sum).parts = ↑l

The parts of a partition constructed from a list. (Definition \ref{def.pars.parts} (b))

theorem Nat.Partition.eq_iff_parts_eq {n : ℕ} (p q : n.Partition) : p = q ↔ p.parts = q.parts

Two partitions are equal iff their parts are equal. (Definition \ref{def.pars.parts} - partitions are determined by their parts)

Examples from the textbook (Example \ref{exa.pars.pars5})

The partitions of 5 are:

• (5): one part
• (4,1): two parts
• (3,2): two parts
• (3,1,1): three parts
• (2,2,1): three parts
• (2,1,1,1): four parts
• (1,1,1,1,1): five parts

Auxiliary lemmas

theorem Nat.Partition.card_le_sum_of_pos (s : Multiset ℕ) (h : ∀ i ∈ s, 0 < i) : s.card ≤ s.sum

The cardinality of a multiset of positive naturals is at most its sum.

theorem Nat.Partition.fold_max_ge_of_mem (p : Multiset ℕ) (a : ℕ) (ha : a ∈ p) : a ≤ Multiset.fold max 0 p

Elements of a multiset are bounded by the fold max.

theorem Nat.Partition.sum_filter_card_range_extend (s : Multiset ℕ) (M N : ℕ) (hM : ∀ x ∈ s, x ≤ M) (hMN : M ≤ N) : ∑ i ∈ Finset.range N, (Multiset.filter (fun (x : ℕ) => x > i) s).card = ∑ i ∈ Finset.range M, (Multiset.filter (fun (x : ℕ) => x > i) s).card

Extending the range of summation when elements are bounded.

theorem Nat.Partition.card_range_filter_gt (x M : ℕ) : {i ∈ Finset.range M | x > i}.card = min x M

The number of i < M with i < x is exactly min x M.

theorem Nat.Partition.sum_filter_card_eq_sum (p : Multiset ℕ) (hp : ∀ i ∈ p, 0 < i) : ∑ i ∈ Finset.range (Multiset.fold max 0 p), (Multiset.filter (fun (x : ℕ) => x > i) p).card = p.sum

Double counting: sum of filter cardinalities equals multiset sum.

theorem Nat.Partition.sum_filter_positive (s : Multiset ℕ) : (Multiset.filter (fun (x : ℕ) => x > 0) s).sum = s.sum

Filtering out zeros doesn't change the sum.

Partition counting functions

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

The partition function p(n): the number of partitions of n. (Definition \ref{def.pars.pn-pkn} (b))

Equations

• Nat.Partition.partitionCount n = Fintype.card n.Partition

def Nat.Partition.partsCount (k n : ℕ) : ℕ

The function p_k(n): the number of partitions of n into exactly k parts. (Definition \ref{def.pars.pn-pkn} (a))

Equations

• Nat.Partition.partsCount k n = {p : n.Partition | p.parts.card = k}.card

def Nat.Partition.partsLeqCount (m n : ℕ) : ℕ

The number of partitions of n with all parts ≤ m. (Used in Theorem \ref{thm.pars.main-gf-parts-n})

Equations

• Nat.Partition.partsLeqCount m n = (Nat.Partition.restricted n fun (x : ℕ) => x ≤ m).card

def Nat.Partition.partsInCount (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] (n : ℕ) : ℕ

The number of partitions of n with all parts in a set I. (Used in Theorem \ref{thm.pars.main-gf-parts-I})

Equations

• Nat.Partition.partsInCount I n = (Nat.Partition.restricted n fun (x : ℕ) => x ∈ I).card

Basic API for partition counting functions

@[simp]

theorem Nat.Partition.partitionCount_zero : partitionCount 0 = 1

p(0) = 1: there is exactly one partition of 0 (the empty partition). (Definition \ref{def.pars.pn-pkn} (b), special case)

@[simp]

theorem Nat.Partition.partitionCount_one : partitionCount 1 = 1

p(1) = 1: there is exactly one partition of 1 (the partition (1)).

theorem Nat.Partition.partitionCount_pos (n : ℕ) : 0 < partitionCount n

p(n) > 0 for all n ∈ ℕ: there is always at least one partition of any natural number. For n > 0, the partition (n) has one part. For n = 0, the empty partition works.

Examples from the textbook

The following examples verify the definitions against the values given in the textbook following Definition \ref{def.pars.pn-pkn}.

Basic properties of partition numbers

def Nat.Partition.numParts {n : ℕ} (p : n.Partition) : ℕ

The number of parts of a partition equals the cardinality of its parts multiset.

Equations

• p.numParts = p.parts.card

theorem Nat.Partition.partsCount_eq_filter_numParts (k n : ℕ) : partsCount k n = {p : n.Partition | p.numParts = k}.card

Alternative characterization: partsCount k n counts partitions with numParts = k.

def Nat.Partition.largestPart {n : ℕ} (p : n.Partition) : ℕ

The largest part of a partition (0 for the empty partition). (Convention \ref{conv.pars.largest-part-0})

Equations

• p.largestPart = Multiset.fold max 0 p.parts

theorem Nat.Partition.largestPart_le_iff_all_parts_le {n m : ℕ} (p : n.Partition) : p.largestPart ≤ m ↔ ∀ i ∈ p.parts, i ≤ m

A partition has largest part ≤ m iff all its parts are ≤ m. This is because the largest part is defined as the maximum of all parts.

This lemma is key for proving Theorem \ref{thm.pars.main-gf-0n}, which states that the generating function for p_0(n) + p_1(n) + ... + p_m(n) equals ∏_{k=1}^m 1/(1-x^k). The proof uses:

1. Corollary \ref{cor.pars.p0kn=dual}: the sum equals the count of partitions with largest part ≤ m
2. This lemma: "largest part ≤ m" is equivalent to "all parts ≤ m"
3. Theorem \ref{thm.pars.main-gf-parts-n}: the generating function for "all parts ≤ m"

theorem Nat.Partition.filter_largestPart_le_eq_restricted (n m : ℕ) : {p : n.Partition | p.largestPart ≤ m} = restricted n fun (x : ℕ) => x ≤ m

The set of partitions with largest part ≤ m equals the set of partitions with all parts ≤ m (i.e., restricted n (· ≤ m)).

This is a key equivalence used in the proof of Theorem \ref{thm.pars.main-gf-0n}.

@[simp]

theorem Nat.Partition.numParts_zero (p : Partition 0) : p.numParts = 0

Partitions of 0 have no parts.

@[simp]

theorem Nat.Partition.largestPart_zero (p : Partition 0) : p.largestPart = 0

The largest part of the partition of 0 is 0. (Convention conv.pars.largest-part-0)

Since the partition of 0 has no parts, the largest part (defined as the maximum of all parts, with 0 as the default) is 0.

theorem Nat.Partition.largestPart_le {n : ℕ} (p : n.Partition) : p.largestPart ≤ n

For a partition of n, the largest part is at most n. This parallels the existing numParts_le lemma which states p.numParts ≤ n.

theorem Nat.Partition.largestPart_pos {n : ℕ} (hn : n > 0) (p : n.Partition) : 0 < p.largestPart

For a partition of n > 0, the largest part is positive. This parallels largestPart_zero (for n = 0) and largestPart_le.

Since n > 0, the partition has at least one part (by numParts_pos), and all parts are positive (by parts_pos). The largest part (fold max 0) of a non-empty multiset of positive numbers is positive.

theorem Nat.Partition.numParts_le {n : ℕ} (p : n.Partition) : p.numParts ≤ n

A partition has at most n parts.

theorem Nat.Partition.numParts_pos {n : ℕ} (hn : n > 0) (p : n.Partition) : 0 < p.numParts

For a partition of n > 0, the number of parts is positive. This parallels numParts_zero (for n = 0) and numParts_le.

theorem Nat.Partition.partsCount_of_gt {k n : ℕ} (h : k > n) : partsCount k n = 0

There are no partitions of n into more than n parts. (Proposition \ref{prop.pars.basics} (b))

@[simp]

theorem Nat.Partition.partsCount_of_gt' {k n : ℕ} (h : n < k) : partsCount k n = 0

p_k(n) = 0 when n < k: alternative form of partsCount_of_gt with the hypothesis n < k instead of k > n, useful for simp. (Proposition \ref{prop.pars.basics} (b))

theorem Nat.Partition.partsCount_zero (n : ℕ) : partsCount 0 n = if n = 0 then 1 else 0

p_0(n) = [n = 0]: the only partition into 0 parts is the empty partition of 0. (Proposition \ref{prop.pars.basics} (c))

@[simp]

theorem Nat.Partition.partsCount_zero_left (n : ℕ) (hn : n > 0) : partsCount 0 n = 0

There are no partitions of n > 0 into exactly 0 parts. This is a simp-friendly form of partsCount_zero for positive n. (Corollary of Proposition \ref{prop.pars.basics} (c))

theorem Nat.Partition.partsCount_eq_zero_iff (k n : ℕ) : partsCount k n = 0 ↔ k > n ∨ k = 0 ∧ n > 0

partsCount k n = 0 iff k > n or k = 0 ∧ n > 0. This provides a complete characterization of when the partition count is zero.

theorem Nat.Partition.partsCount_one (n : ℕ) : partsCount 1 n = if n > 0 then 1 else 0

p_1(n) = [n > 0]: the only partition of a positive n into 1 part is (n). (Proposition \ref{prop.pars.basics} (d))

Helper lemmas for the recurrence relation

def Nat.Partition.containsOne {n : ℕ} (p : n.Partition) : Prop

A partition containing 1 as a part.

Equations

• p.containsOne = (1 ∈ p.parts)

instance Nat.Partition.instDecidablePredContainsOne {n : ℕ} : DecidablePred containsOne

Equations

• p.instDecidablePredContainsOne = Multiset.decidableMem 1 p.parts

def Nat.Partition.partsWithOne (k n : ℕ) : Finset n.Partition

Partitions of n into k parts that contain 1.

Equations

• Nat.Partition.partsWithOne k n = {p : n.Partition | p.parts.card = k ∧ p.containsOne}

def Nat.Partition.partsWithoutOne (k n : ℕ) : Finset n.Partition

Partitions of n into k parts that don't contain 1.

Equations

• Nat.Partition.partsWithoutOne k n = {p : n.Partition | p.parts.card = k ∧ ¬p.containsOne}

theorem Nat.Partition.partsCount_split {k n : ℕ} : partsCount k n = (partsWithOne k n).card + (partsWithoutOne k n).card

def Nat.Partition.removeOne {n : ℕ} (p : n.Partition) (h : 1 ∈ p.parts) : (n - 1).Partition

Remove one 1 from a partition containing 1 to get a partition of n-1.

Equations

• p.removeOne h = Nat.Partition.ofSums (n - 1) (p.parts.erase 1) ⋯

def Nat.Partition.addOne {n : ℕ} (p : n.Partition) : (n + 1).Partition

Add one 1 to a partition to get a partition of n+1.

Equations

• p.addOne = Nat.Partition.ofSums (n + 1) (1 ::ₘ p.parts) ⋯

def Nat.Partition.subtractOneFromEach {n k : ℕ} (p : n.Partition) (hk : p.parts.card = k) (h : ∀ x ∈ p.parts, x > 1) : (n - k).Partition

Subtract 1 from each part of a partition (when all parts > 1) to get a partition of n - k.

Equations

• p.subtractOneFromEach hk h = Nat.Partition.ofSums (n - k) (Multiset.map (fun (x : ℕ) => x - 1) p.parts) ⋯

def Nat.Partition.addOneToEach {n k : ℕ} (p : n.Partition) (hk : p.parts.card = k) : (n + k).Partition

Add 1 to each part of a partition to get a partition of n + k.

Equations

• p.addOneToEach hk = Nat.Partition.ofSums (n + k) (Multiset.map (fun (x : ℕ) => x + 1) p.parts) ⋯

theorem Nat.Partition.partsWithOne_card_eq {k n : ℕ} (hk : k > 0) (hn : n > 0) : (partsWithOne k n).card = partsCount (k - 1) (n - 1)

Bijection: partsWithOne k n ↔ partitions of (n-1) into (k-1) parts.

theorem Nat.Partition.partsWithoutOne_card_eq {k n : ℕ} (hk : k > 0) : (partsWithoutOne k n).card = partsCount k (n - k)

Bijection: partsWithoutOne k n ↔ partitions of (n-k) into k parts.

theorem Nat.Partition.partsCount_recurrence {k n : ℕ} (hk : k > 0) (hn : n > 0) : partsCount k n = partsCount k (n - k) + partsCount (k - 1) (n - 1)

The recurrence relation for partition numbers: p_k(n) = p_k(n-k) + p_{k-1}(n-1) for k > 0 and n > 0. (Proposition \ref{prop.pars.basics} (e))

Note: The hypothesis n > 0 is required because in natural number arithmetic, 0 - 1 = 0, so the recurrence fails for k = 1, n = 0:

• LHS = p_1(0) = 0
• RHS = p_1(0) + p_0(0) = 0 + 1 = 1

This classifies partitions into:

• Type 1: partitions with 1 as a part (bijection with partitions of n-1 into k-1 parts)
• Type 2: partitions without 1 (subtract 1 from each part → partitions of n-k into k parts)

The proof requires establishing two bijections:

1. {partitions of n into k parts containing 1} ↔ {partitions of n-1 into k-1 parts} via removeOne/addOne
2. {partitions of n into k parts not containing 1} ↔ {partitions of n-k into k parts} via subtractOneFromEach/addOneToEach

theorem Nat.Partition.partition_two_parts_form {n : ℕ} (p : n.Partition) (hp : p.parts.card = 2) : ∃ (b : ℕ), 1 ≤ b ∧ 2 * b ≤ n ∧ p.parts = {n - b, b}

A partition into 2 parts has the form {n-b, b} for some 1 ≤ b ≤ n/2.

theorem Nat.Partition.partsCount_two (n : ℕ) : partsCount 2 n = n / 2

p_2(n) = ⌊n/2⌋ for n ∈ ℕ. (Proposition \ref{prop.pars.basics} (f))

The partitions of n into 2 parts are (n-1,1), (n-2,2), ..., (⌈n/2⌉, ⌊n/2⌋).

theorem Nat.Partition.partitionCount_sum (n : ℕ) : partitionCount n = ∑ k ∈ Finset.range (n + 1), partsCount k n

p(n) = p_0(n) + p_1(n) + ... + p_n(n) for n ∈ ℕ. (Proposition \ref{prop.pars.basics} (g))

Generating functions

theorem Nat.Partition.partitionCount_genFun {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] : HasProd (fun (k : ℕ) => ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j)) (PowerSeries.mk fun (n : ℕ) => ↑(partitionCount n))

The generating function for partition numbers: ∑_{n≥0} p(n) x^n = ∏_{k≥1} 1/(1-x^k). (Theorem \ref{thm.pars.main-gf})

More precisely, this states that the power series whose n-th coefficient is the number of partitions of n equals the infinite product ∏{k≥1} (∑{j≥0} x^{kj}).

The product converges in the power series topology because multiplying by 1/(1-x^k) = ∑_{j≥0} x^{kj} doesn't affect the first k coefficients.

The proof uses Mathlib's hasProd_powerSeriesMk_card_restricted with the trivially true predicate.

theorem Nat.Partition.partitionCount_genFun_partsLeq {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (m : ℕ) : HasProd (fun (k : ℕ) => if k + 1 ≤ m then ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j) else 1) (PowerSeries.mk fun (n : ℕ) => ↑(partsLeqCount m n))

The generating function for partitions with parts ≤ m: ∑_{n≥0} p_{parts≤m}(n) x^n = ∏_{k=1}^m 1/(1-x^k). (Theorem \ref{thm.pars.main-gf-parts-n})

This is a finite product version of the partition generating function. The product is over k from 1 to m, expressed here with shifted index as a conditional infinite product.

theorem Nat.Partition.partitionCount_genFun_partsLeq_finprod {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (m : ℕ) : ∏ k ∈ Finset.range m, ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j) = PowerSeries.mk fun (n : ℕ) => ↑(restricted n fun (x : ℕ) => x ≤ m).card

The generating function for partitions with parts ≤ m, expressed as a finite product: ∑_{n≥0} p_{parts≤m}(n) x^n = ∏_{k=1}^m (∑_{j≥0} x^{kj}). (Theorem \ref{thm.pars.main-gf-parts-n})

This is the same theorem as partitionCount_genFun_partsLeq, but expressed as an equality of power series rather than a HasProd statement.

The product ∏_{k=1}^m (∑_{j≥0} x^{kj}) equals ∏_{k=1}^m 1/(1-x^k) since the geometric series 1/(1-x^k) = ∑_{j≥0} x^{kj} converges in the power series topology.

theorem Nat.Partition.partsLeqCount_eq_coeff {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (m n : ℕ) : ↑(restricted n fun (x : ℕ) => x ≤ m).card = (PowerSeries.coeff n) (∏ k ∈ Finset.range m, ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j))

The number of partitions with parts ≤ m equals the n-th coefficient of the finite product ∏{k=1}^m (∑{j≥0} x^{kj}). (Corollary to Theorem \ref{thm.pars.main-gf-parts-n})

theorem Nat.Partition.partitionCount_genFun_partsIn {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] : HasProd (fun (k : ℕ) => if k + 1 ∈ I then ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j) else 1) (PowerSeries.mk fun (n : ℕ) => ↑(partsInCount I n))

The generating function for partitions with parts in a set I: ∑_{n≥0} p_I(n) x^n = ∏_{k∈I} 1/(1-x^k). (Theorem \ref{thm.pars.main-gf-parts-I})

This generalizes both the standard partition generating function (I = ℕ⁺) and the finite product version (I = {1, ..., m}).

The product is over k in I, expressed here with shifted index as a conditional infinite product. Each factor ∑' j, X^((k+1)*j) equals 1/(1-X^(k+1)) as a geometric series.

Proof sketch: The bijection from the TeX source maps each essentially finite family (u_i)_{i∈I} of nonnegative integers to the partition containing each i ∈ I exactly u_i times. The coefficient of X^n on the product side counts such families with ∑_{i∈I} i·u_i = n, which bijects with partitions of n having all parts in I.

theorem Nat.Partition.partsInCount_genFun_eq_tprod {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] : (PowerSeries.mk fun (n : ℕ) => ↑(partsInCount I n)) = ∏' (k : ℕ), if k + 1 ∈ I then ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j) else 1

The infinite product form of the generating function for partitions with parts in I. This is the tprod version of partitionCount_genFun_partsIn.

Expresses the generating function as an unconditional infinite product.

theorem Nat.Partition.multipliable_partsIn_genFun {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] : Multipliable fun (k : ℕ) => if k + 1 ∈ I then ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j) else 1

The infinite product for partitions with parts in I is multipliable. This is useful when manipulating the product form of the generating function.

Odd parts and distinct parts

This section formalizes Euler's odd-distinct identity (Theorem \ref{thm.pars.odd-dist-equal}), which states that the number of partitions of n into odd parts equals the number of partitions of n into distinct parts.

Definition \ref{def.pars.odd-dist-parts}

• A partition into odd parts is a partition whose all parts are odd.
• A partition into distinct parts is a partition whose parts are all different.
• p_odd(n) = number of partitions of n into odd parts
• p_dist(n) = number of partitions of n into distinct parts

Theorem \ref{thm.pars.odd-dist-equal}: Euler's Odd-Distinct Identity

We have p_odd(n) = p_dist(n) for each n ∈ ℕ.

Generating Function Proof

The identity follows from the generating function identity:

∏_{i>0} (1-x^{2i-1})^{-1} = ∏_{k>0} (1+x^k)

The LHS generates partitions into odd parts (each odd k can appear any number of times). The RHS generates partitions into distinct parts (each k appears 0 or 1 times).

Bijective Proof

Map A: odd parts → distinct parts Given a partition λ into odd parts, repeatedly merge pairs of equal parts until no equal parts remain. The result A(λ) is a partition into distinct parts.

Example: (5,5,3,1,1,1) → (10,3,2,1) by merging (5,5)→10 and (1,1)→2.

This is well-defined because merging equal odd parts produces even parts, and the process terminates. The final partition has distinct parts because if k appears m times in the original partition, then in A(λ), the parts 2^0·k, 2^1·k, 2^2·k, ... appear according to the binary representation of m.

Map B: distinct parts → odd parts Given a partition λ into distinct parts, repeatedly split even parts into halves until only odd parts remain.

Example: (10,3,2,1) → (5,5,3,1,1,1) by splitting 10→(5,5) and 2→(1,1).

The maps A and B are mutually inverse, establishing the bijection.

def Nat.Partition.IsOddParts {n : ℕ} (p : n.Partition) : Prop

A partition into odd parts is a partition whose all parts are odd. (Definition \ref{def.pars.odd-dist-parts} (a))

For example, (7), (5,1,1), (3,3,1), (3,1,1,1,1), (1,1,1,1,1,1,1) are the partitions of 7 into odd parts.

Equations

• p.IsOddParts = ∀ i ∈ p.parts, Odd i

def Nat.Partition.IsDistinctParts {n : ℕ} (p : n.Partition) : Prop

A partition into distinct parts is a partition whose parts are all different. (Definition \ref{def.pars.odd-dist-parts} (b))

For example, (7), (6,1), (5,2), (4,3), (4,2,1) are the partitions of 7 into distinct parts. Note that repeated parts are not allowed.

Equations

• p.IsDistinctParts = p.parts.Nodup

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

The number of partitions of n into odd parts: p_odd(n). (Definition \ref{def.pars.odd-dist-parts} (c))

This counts the partitions of n where every part is an odd number. Uses Mathlib's Nat.Partition.odds which filters partitions by the predicate ¬Even (equivalent to Odd for positive integers).

Equations

• Nat.Partition.oddPartsCount n = (Nat.Partition.odds n).card

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

The number of partitions of n into distinct parts: p_dist(n). (Definition \ref{def.pars.odd-dist-parts} (c))

This counts the partitions of n where all parts are different (no repeats). Uses Mathlib's Nat.Partition.distincts which filters partitions by the Nodup predicate on the parts multiset.

Equations

• Nat.Partition.distinctPartsCount n = (Nat.Partition.distincts n).card

instance Nat.Partition.instDecidableIsOddParts {n : ℕ} (p : n.Partition) : Decidable p.IsOddParts

Equations

• p.instDecidableIsOddParts = inferInstanceAs (Decidable (∀ i ∈ p.parts, Odd i))

instance Nat.Partition.instDecidableIsDistinctParts {n : ℕ} (p : n.Partition) : Decidable p.IsDistinctParts

Equations

• p.instDecidableIsDistinctParts = inferInstanceAs (Decidable p.parts.Nodup)

Examples from the textbook (following Definition \ref{def.pars.odd-dist-parts})

@[simp]

theorem Nat.Partition.oddPartsCount_zero : oddPartsCount 0 = 1

p_odd(0) = 1: the only partition of 0 into odd parts is the empty partition. (Following Definition \ref{def.pars.odd-dist-parts})

@[simp]

theorem Nat.Partition.distinctPartsCount_zero : distinctPartsCount 0 = 1

p_dist(0) = 1: the only partition of 0 into distinct parts is the empty partition. (Following Definition \ref{def.pars.odd-dist-parts})

API for IsOddParts and IsDistinctParts

theorem Nat.Partition.isOddParts_zero (p : Partition 0) : p.IsOddParts

The empty partition (of 0) is trivially a partition into odd parts.

theorem Nat.Partition.isDistinctParts_zero (p : Partition 0) : p.IsDistinctParts

The empty partition (of 0) is trivially a partition into distinct parts.

theorem Nat.Partition.isOddParts_iff {n : ℕ} (p : n.Partition) : p.IsOddParts ↔ ∀ i ∈ p.parts, Odd i

A partition is into odd parts iff all its parts satisfy Odd.

theorem Nat.Partition.isDistinctParts_iff {n : ℕ} (p : n.Partition) : p.IsDistinctParts ↔ p.parts.Nodup

A partition is into distinct parts iff its parts multiset has no duplicates.

theorem Nat.Partition.isDistinctParts_iff_count_le_one {n : ℕ} (p : n.Partition) : p.IsDistinctParts ↔ ∀ (i : ℕ), Multiset.count i p.parts ≤ 1

Alternative characterization: a partition is into distinct parts iff each part appears at most once.

theorem Nat.Partition.mem_odds_iff {n : ℕ} (p : n.Partition) : p ∈ odds n ↔ p.IsOddParts

Characterization of odds in terms of IsOddParts.

theorem Nat.Partition.mem_distincts_iff {n : ℕ} (p : n.Partition) : p ∈ distincts n ↔ p.IsDistinctParts

Characterization of distincts in terms of IsDistinctParts.

theorem Nat.Partition.oddPartsCount_eq_filter_card (n : ℕ) : oddPartsCount n = (Finset.filter IsOddParts Finset.univ).card

The counting function oddPartsCount equals the cardinality of the filter.

theorem Nat.Partition.distinctPartsCount_eq_filter_card (n : ℕ) : distinctPartsCount n = (Finset.filter IsDistinctParts Finset.univ).card

The counting function distinctPartsCount equals the cardinality of the filter.

theorem Nat.Partition.odd_eq_distinct (n : ℕ) : (odds n).card = (distincts n).card

Euler's odd-distinct identity: the number of partitions of n into odd parts equals the number of partitions of n into distinct parts. (Theorem \ref{thm.pars.odd-dist-equal})

This is Theorem 45 from Freek Wiedijk's list of 100 theorems.

The proof in Mathlib uses Glaisher's theorem, which generalizes this result: for any positive integer d, the number of partitions with parts not divisible by d equals the number of partitions where no part is repeated d or more times. Euler's identity is the special case d = 2.

The bijective proof (sketched in the module docstring) works by:

• Merging pairs of equal parts (odd → distinct)
• Splitting even parts into halves (distinct → odd)

theorem Nat.Partition.oddPartsCount_eq_distinctPartsCount (n : ℕ) : oddPartsCount n = distinctPartsCount n

Euler's odd-distinct identity in terms of counting functions.

theorem Nat.Partition.card_isOddParts_eq_card_isDistinctParts (n : ℕ) : (Finset.filter IsOddParts Finset.univ).card = (Finset.filter IsDistinctParts Finset.univ).card

The odd-distinct identity stated with predicates.

Conjugation / Transposition of partitions

noncomputable def Nat.Partition.transpose {n : ℕ} (p : n.Partition) : n.Partition

The transpose (conjugate) of a partition. For a partition λ = (λ₁, λ₂, ..., λₖ), the transpose λᵗ is defined by:

• The Young diagram of λᵗ is the transpose of the Young diagram of λ
• Equivalently: (λᵗ)ᵢ = #{j : λⱼ ≥ i}

The transpose satisfies:

• |λᵗ| = |λ| (same size)
• (λᵗ)ᵗ = λ (involution)
• length(λᵗ) = largest part of λ
• largest part of λᵗ = length(λ)

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.Partition.sorted_countP_gt_iff {sl : List ℕ} (hsl : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) sl) (j : ℕ) (hj : j < sl.length) (i : ℕ) : List.countP (fun (x : ℕ) => decide (x > i)) sl > j ↔ sl[j] > i

Helper lemma: for a sorted decreasing list, the count of elements > i is > j iff the j-th element > i. This is the key bijection for the Young diagram transpose.

theorem Nat.Partition.transpose_transpose {n : ℕ} (p : n.Partition) : p.transpose.transpose = p

The transpose is an involution.

The proof uses the fundamental property that transposing a Young diagram twice gives back the original diagram. For a partition λ = (λ₁, λ₂, ..., λₖ):

• The transpose λᵗ has parts μⱼ = #{i : λᵢ ≥ j} for j = 1, ..., λ₁
• Applying transpose again: #{j : μⱼ ≥ i} = λᵢ for all i

This is because the number of columns of height ≥ i in the Young diagram of λᵗ equals the i-th row length of λ.

theorem Nat.Partition.transpose_size {n : ℕ} (p : n.Partition) : p.transpose.parts.sum = n

The transpose preserves size.

theorem Nat.Partition.filter_card_pos_of_lt_largest {n : ℕ} (p : n.Partition) (i : ℕ) (hi : i < Multiset.fold max 0 p.parts) : 0 < (Multiset.filter (fun (x : ℕ) => x > i) p.parts).card

Key lemma: for i < largest, the filter count is positive

theorem Nat.Partition.transpose_length_eq_largestPart {n : ℕ} (p : n.Partition) : p.transpose.numParts = p.largestPart

The length of the transpose equals the largest part of the original partition.

theorem Nat.Partition.filter_gt_zero_card_eq {n : ℕ} (p : n.Partition) : (Multiset.filter (fun (x : ℕ) => x > 0) p.parts).card = p.parts.card

theorem Nat.Partition.transpose_largestPart_eq_length {n : ℕ} (p : n.Partition) : p.transpose.largestPart = p.numParts

The largest part of the transpose equals the length of the original partition.

theorem Nat.Partition.partsCount_eq_largestPartCount (n k : ℕ) : partsCount k n = {p : n.Partition | p.largestPart = k}.card

The number of partitions of n into k parts equals the number of partitions of n whose largest part is k. (Proposition \ref{prop.pars.pkn=dual})

This follows from the fact that transpose is a bijection that swaps "number of parts" with "largest part".

theorem Nat.Partition.partsCount_sum_eq_largestPartLeq (n k : ℕ) : ∑ i ∈ Finset.range (k + 1), partsCount i n = {p : n.Partition | p.largestPart ≤ k}.card

Corollary: p_0(n) + p_1(n) + ... + p_k(n) equals the number of partitions of n whose largest part is ≤ k. (Corollary \ref{cor.pars.p0kn=dual})

theorem Nat.Partition.partsCount_sum_eq_partsLeqCount (n m : ℕ) : ∑ k ∈ Finset.range (m + 1), partsCount k n = partsLeqCount m n

The sum p_0(n) + p_1(n) + ... + p_m(n) equals the count of partitions with all parts ≤ m.

This combines Corollary \ref{cor.pars.p0kn=dual} (sum equals count with largest part ≤ m) with the equivalence "largest part ≤ m" ↔ "all parts ≤ m" from filter_largestPart_le_eq_restricted.

theorem Nat.Partition.partsCountSum_genFun {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [T2Space R] [IsTopologicalSemiring R] (m : ℕ) : (PowerSeries.mk fun (n : ℕ) => ∑ k ∈ Finset.range (m + 1), ↑(partsCount k n)) = ∏ k ∈ Finset.range m, ∑' (j : ℕ), PowerSeries.X ^ ((k + 1) * j)

The generating function for the sum p_0(n) + p_1(n) + ... + p_m(n): ∑_{n≥0} (p_0(n) + p_1(n) + ... + p_m(n)) x^n = ∏_{k=1}^m 1/(1-x^k). (Theorem \ref{thm.pars.main-gf-0n})

The proof uses three key facts:

1. Corollary \ref{cor.pars.p0kn=dual}: p_0(n) + p_1(n) + ... + p_m(n) equals the number of partitions of n with largest part ≤ m.
2. Equivalence: "largest part ≤ m" is equivalent to "all parts ≤ m" (this is obvious from the definition of largest part as the maximum).
3. Theorem \ref{thm.pars.main-gf-parts-n}: The generating function for partitions with all parts ≤ m is ∏_{k=1}^m 1/(1-x^k).

The product ∏_{k=1}^m 1/(1-x^k) is represented here as ∏_{k=0}^{m-1} (∑_{j≥0} x^{(k+1)j}) since the geometric series 1/(1-x^k) = ∑_{j≥0} x^{kj} converges in the power series topology.

Counting partitions by parts and largest part

def Nat.Partition.partsAndLargestCount (k ℓ n : ℕ) : ℕ

The count of partitions with exactly k parts and largest part ℓ, for a specific size n.

Equations

• Nat.Partition.partsAndLargestCount k ℓ n = {p : n.Partition | p.numParts = k ∧ p.largestPart = ℓ}.card

def Nat.Partition.partsAndLargestCountTotal (k ℓ : ℕ) : ℕ

The total count of partitions with exactly k parts and largest part ℓ (summed over all sizes). The size ranges from k (minimum, when all parts are 1 except the largest) to k*ℓ (maximum, when all parts equal ℓ).

Equations

• Nat.Partition.partsAndLargestCountTotal k ℓ = ∑ n ∈ Finset.Icc k (k * ℓ), Nat.Partition.partsAndLargestCount k ℓ n

Helper lemmas for the bijection

The following lemmas provide infrastructure for the bijection proof in partsAndLargestCountTotal_eq. They establish key properties of the forward map (Sym → Partition):

• symToPartsMultiset: constructs partition parts from a Sym
• symToPartsMultiset_pos: all parts are positive
• symToPartsMultiset_card: cardinality is k
• symToPartsMultiset_fold_max: largest part is ℓ
• symToPartsMultiset_erase: erasing ℓ recovers the Sym elements
• symToPartsMultiset_sum_range: sum lies in the valid range [k, k*ℓ]

The backward map (Partition → Sym) uses Multiset.pmap to map each part x in p.parts.erase ℓ to ⟨x - 1, ...⟩ : Fin ℓ, which is valid since all such parts are in {1, ..., ℓ}.

The Equiv construction is completed in partsAndLargestCountTotal_eq using Equiv.ofBijective with toSigma_injective and toSigma_surj.

theorem Nat.Partition.symToPartsMultiset_pos {n : ℕ} (ℓ : ℕ) (hℓ : ℓ ≥ 1) (s : Sym (Fin ℓ) n) (x : ℕ) : x ∈ Nat.Partition.symToPartsMultiset✝ ℓ s → 0 < x

All parts in symToPartsMultiset are positive.

theorem Nat.Partition.symToPartsMultiset_card {n : ℕ} (ℓ : ℕ) (s : Sym (Fin ℓ) n) : (Nat.Partition.symToPartsMultiset✝ ℓ s).card = n + 1

The cardinality of symToPartsMultiset is n + 1.

theorem Nat.Partition.symToPartsMultiset_fold_max {n : ℕ} (ℓ : ℕ) (s : Sym (Fin ℓ) n) : Multiset.fold max 0 (Nat.Partition.symToPartsMultiset✝ ℓ s) = ℓ

The largest part (fold max 0) of symToPartsMultiset is ℓ.

theorem Nat.Partition.symToPartsMultiset_erase {n : ℕ} (ℓ : ℕ) (s : Sym (Fin ℓ) n) : (Nat.Partition.symToPartsMultiset✝ ℓ s).erase ℓ = Multiset.map (fun (x : Fin ℓ) => ↑x + 1) ↑s

Erasing ℓ from symToPartsMultiset recovers the mapped parts.

theorem Nat.Partition.symToPartsMultiset_sum_range (k ℓ : ℕ) (hk : k ≥ 1) (hℓ : ℓ ≥ 1) (s : Sym (Fin ℓ) (k - 1)) : (Nat.Partition.symToPartsMultiset✝ ℓ s).sum ∈ Finset.Icc k (k * ℓ)

The sum of symToPartsMultiset lies in [k, k*ℓ] for s : Sym (Fin ℓ) (k-1).

theorem Nat.Partition.partsAndLargestCountTotal_eq (k ℓ : ℕ) (hk : k ≥ 1) (hℓ : ℓ ≥ 1) : partsAndLargestCountTotal k ℓ = (k + ℓ - 2).choose (k - 1)

Proposition \ref{prop.pars.qbinom.intro-count-binom}: For positive integers k and ℓ, the number of partitions with exactly k parts and largest part ℓ equals C(k+ℓ-2, k-1).

Proof outline: A partition with k parts and largest part ℓ has the form (ℓ, λ₂, ..., λₖ) where ℓ ≥ λ₂ ≥ ... ≥ λₖ ≥ 1.

The tuple (λ₂, ..., λₖ) is a weakly decreasing sequence of k-1 positive integers, each at most ℓ. This is equivalent to choosing a (k-1)-element multisubset of {1, 2, ..., ℓ}, which by the "stars and bars" formula equals C(ℓ + (k-1) - 1, k-1) = C(k + ℓ - 2, k - 1).

Note: This formula is independent of the size n of the partition.

Bijection details:

• Forward: partition (ℓ, λ₂, ..., λₖ) ↦ multiset {λ₂-1, ..., λₖ-1} ⊆ Fin ℓ
• Backward: multiset {a₁, ..., aₖ₋₁} ⊆ Fin ℓ ↦ partition (ℓ, a₁+1, ..., aₖ₋₁+1) sorted

This is well-defined because:

1. Each λᵢ ∈ {1, ..., ℓ}, so λᵢ - 1 ∈ {0, ..., ℓ-1} = Fin ℓ
2. Each aᵢ ∈ Fin ℓ gives aᵢ + 1 ∈ {1, ..., ℓ}
3. The resulting partition has largest part ℓ (which is explicitly the first part)
4. The partition has k parts (one ℓ, plus k-1 from the multiset)

Examples verifying the formula

The following examples verify the formula C(k+ℓ-2, k-1) against computed values:

• k=1, ℓ=1: C(0,0) = 1. Partition: (1).
• k=1, ℓ=5: C(4,0) = 1. Partition: (5).
• k=2, ℓ=1: C(1,1) = 1. Partition: (1,1).
• k=2, ℓ=2: C(2,1) = 2. Partitions: (2,1), (2,2).
• k=2, ℓ=3: C(3,1) = 3. Partitions: (3,1), (3,2), (3,3).
• k=3, ℓ=2: C(3,2) = 3. Partitions: (2,1,1), (2,2,1), (2,2,2).

Partition numbers and divisor sums

@[reducible, inline]

abbrev Nat.Partition.divisorSum (n : ℕ) : ℕ

The sum of divisors function σ(n) = ∑_{d|n} d. This is ArithmeticFunction.sigma 1 in Mathlib.

Equations

• Nat.Partition.divisorSum n = (ArithmeticFunction.sigma 1) n

Proof of Theorem σ₁ (thm.pars.sigma1)

We prove the recurrence n · p(n) = ∑_{k=1}^n σ(k) · p(n-k) using generating functions.

Proof outline (from the TeX source)

Define the generating functions:

• P := ∑_{n≥0} p(n) x^n (the partition generating function)
• S := ∑_{k≥1} σ(k) x^k (the divisor sum generating function)

The key identity is X · P' = S · P, which we prove using logarithmic derivatives.

Since P = ∏_{k≥1} 1/(1-x^k), taking the logarithmic derivative gives:

  P'/P = ∑_{k≥1} loder(1/(1-x^k))
       = ∑_{k≥1} kx^{k-1}/(1-x^k)
       = ∑_{n≥1} σ(n) x^{n-1}

Multiplying by xP gives xP' = SP.

Comparing coefficients of x^n on both sides:

• LHS: coefficient of x^n in xP' is n · p(n)
• RHS: coefficient of x^n in SP is ∑_{k=1}^n σ(k) · p(n-k)

This proves the theorem.

noncomputable def Nat.Partition.P : PowerSeries ℤ

The partition generating function P = ∑_{n≥0} p(n) x^n, specialized to ℤ coefficients.

Equations

• Nat.Partition.P = Nat.Partition.genFun fun (x x_1 : ℕ) => 1

theorem Nat.Partition.coeff_P (n : ℕ) : (PowerSeries.coeff n) P = ↑(partitionCount n)

The coefficient of x^n in P equals p(n).

noncomputable def Nat.Partition.S : PowerSeries ℤ

The divisor sum generating function S = ∑_{k≥1} σ(k) x^k.

Equations

• Nat.Partition.S = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else ↑(Nat.Partition.divisorSum n)

@[simp]

theorem Nat.Partition.coeff_S (n : ℕ) : (PowerSeries.coeff n) S = ↑(if n = 0 then 0 else divisorSum n)

The coefficient of x^n in S.

theorem Nat.Partition.coeff_X_mul_derivative_P (n : ℕ) : (PowerSeries.coeff n) (PowerSeries.X * (PowerSeries.derivative ℤ) P) = ↑n * (PowerSeries.coeff n) P

The coefficient of x^n in X · P' equals n · p(n).

theorem Nat.Partition.coeff_S_mul_P (n : ℕ) : (PowerSeries.coeff n) (S * P) = ↑(∑ k ∈ Finset.range n, divisorSum (k + 1) * partitionCount (n - k - 1))

The coefficient of x^n in S · P equals ∑_{k=1}^n σ(k) · p(n-k).

theorem Nat.Partition.sum_parts_as_weighted_count {n : ℕ} (p : n.Partition) : p.parts.sum = ∑ d ∈ p.parts.toFinset, d * Multiset.count d p.parts

Sum of parts equals sum over distinct parts weighted by count.

theorem Nat.Partition.lhs_eq_sum_parts (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] (n : ℕ) : n * (restricted n fun (x : ℕ) => x ∈ I).card = ∑ p ∈ restricted n fun (x : ℕ) => x ∈ I, p.parts.sum

LHS of the identity equals sum of parts over all partitions.

Helper lemmas for partitionCount_divisorSum_restricted

These lemmas establish the key pieces needed for the double-counting proof:

1. Bijection lemma: Removing j copies of d from a partition gives a partition of n - d*j
2. Count sum identity: ∑p count(d, p) = ∑{j≥1} |{p : count(d,p) ≥ j}|
3. Sum swap lemma: Swap the order of summation over partitions and parts
4. Divisor sum reindexing: Transform ∑k ∑{d | k+1} to ∑d ∑{j : d*j ≤ n}

def Nat.Partition.removePartCopies {n : ℕ} (p : n.Partition) (d j : ℕ) (_hd : d > 0) (hj : j ≤ Multiset.count d p.parts) : (n - d * j).Partition

Remove j copies of element d from a partition, getting a partition of n - d*j. This is the forward direction of the bijection.

Equations

• p.removePartCopies d j _hd hj = { parts := p.parts - Multiset.replicate j d, parts_pos := ⋯, parts_sum := ⋯ }

def Nat.Partition.addPartCopies {m : ℕ} (q : m.Partition) (d j : ℕ) (hd : d > 0) : (m + d * j).Partition

Add j copies of element d to a partition, getting a partition of m + d*j. This is the backward direction of the bijection.

Equations

• q.addPartCopies d j hd = { parts := q.parts + Multiset.replicate j d, parts_pos := ⋯, parts_sum := ⋯ }

theorem Nat.Partition.count_le_div_of_partition (n d : ℕ) (p : n.Partition) (hd : 0 < d) : Multiset.count d p.parts ≤ n / d

Helper: count(d, p) ≤ n/d for any partition of n and d > 0. This is the tight bound: at most n/d copies of d can fit in a partition of n.

theorem Nat.Partition.sum_count_eq_sum_card_ge (n : ℕ) (s : Finset n.Partition) (d : ℕ) : ∑ p ∈ s, Multiset.count d p.parts = ∑ j ∈ Finset.range (n + 1), {p ∈ s | Multiset.count d p.parts ≥ j + 1}.card

The count sum identity: ∑p count(d, p) = ∑{j=1}^{max_count} |{p : count(d,p) ≥ j}|. This is the standard identity that sum of values equals sum of "at least j" counts.

The proof uses double counting: each partition p with count(d,p) = c contributes c to the LHS and is counted in exactly c of the sets {p : count(d,p) ≥ j+1} for j < c.

theorem Nat.Partition.card_count_ge_eq_restricted (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] (hI : ∀ i ∈ I, i > 0) (n d j : ℕ) (hd : d ∈ I) (hdj : d * j ≤ n) : {p ∈ restricted n fun (x : ℕ) => x ∈ I | Multiset.count d p.parts ≥ j}.card = (restricted (n - d * j) fun (x : ℕ) => x ∈ I).card

Partitions with count(d, p) ≥ j biject with partitions of n - dj. Specifically, {p ∈ restricted n I : count(d,p) ≥ j} ≃ restricted (n - dj) I.

Forward: remove j copies of d Backward: add j copies of d

theorem Nat.Partition.divisor_sum_reindex (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] (n : ℕ) (f : ℕ → ℕ) : ∑ k ∈ Finset.range n, ∑ d ∈ (k + 1).divisors with d ∈ I, d * f (n - k - 1) = ∑ d ∈ Finset.Icc 1 n with d ∈ I, d * ∑ j ∈ Finset.Icc 1 (n / d), f (n - d * j)

Divisor sum reindexing: swaps the order of summation from ∑{k=0}^{n-1} ∑{d | k+1, d ∈ I} to ∑{d ∈ I, d ≤ n} ∑{j=1}^{⌊n/d⌋}.

The bijection is: (k, d) ↔ (d, j) where k = dj - 1, j = (k+1)/d. This transforms the constraint "d | k+1" to "k = dj - 1 for some j ≥ 1".

Used in the proof of partitionCount_divisorSum_restricted.

theorem Nat.Partition.partitionCount_divisorSum_restricted (I : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ I] (hI : ∀ i ∈ I, i > 0) (n : ℕ) : n * (restricted n fun (x : ℕ) => x ∈ I).card = ∑ k ∈ Finset.range n, (∑ d ∈ (k + 1).divisors with d ∈ I, d) * (restricted (n - k - 1) fun (x : ℕ) => x ∈ I).card

Generalization of the divisor sum recurrence for partitions with parts in a set I: n · p_I(n) = ∑_{k=1}^n σ_I(k) · p_I(n-k) where σ_I(n) is the sum of divisors of n that belong to I. (Theorem \ref{thm.pars.sigma1-I})

The proof uses the generating function approach via logarithmic derivatives:

• Let P_I = ∑n p_I(n) x^n = ∏{k∈I} 1/(1-x^k)
• Let S_I = ∑_n σ_I(n) x^n
• Taking logarithmic derivative of P_I gives x·P_I'/P_I = S_I
• Therefore x·P_I' = S_I·P_I
• Comparing coefficients of x^n gives the identity

Equivalently, both sides count weighted pairs:

• LHS = ∑_p (sum of parts) = ∑_p ∑_d d·count(d,p)
• RHS = ∑_{m=1}^n σ_I(m)·p_I(n-m) = ∑d d·∑{j≥1} p_I(n-d·j)
• Both equal ∑{d∈I, d≤n} d·∑{j=1}^{n/d} p_I(n-d·j)

theorem Nat.Partition.partitionCount_divisorSum (n : ℕ) : n * partitionCount n = ∑ k ∈ Finset.range n, divisorSum (k + 1) * partitionCount (n - k - 1)

The recurrence relation connecting partition numbers and divisor sums: n · p(n) = ∑_{k=1}^n σ(k) · p(n-k). (Theorem \ref{thm.pars.sigma1})

This is proved using the generalized identity partitionCount_divisorSum_restricted specialized to I = all positive integers.

theorem Nat.Partition.X_mul_derivative_P_eq_S_mul_P : PowerSeries.X * (PowerSeries.derivative ℤ) P = S * P

The key generating function identity: X · P' = S · P.

This follows from the combinatorial identity partitionCount_divisorSum by comparing coefficients.