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

By definition.

Follows from the fact that the partition of \(0\) has no parts.

By induction on the multiset.

Since each part is \(\geq 1\), the number of parts is at most the sum of parts, which is \(n\).

If a partition of a positive \(n\) had no parts, its sum would be \(0\), a contradiction.

Since the partition has at least one part and all parts are positive, the maximum is positive.

The empty partition (for \(n=0\)) or the indiscrete partition \((n)\) (for \(n{\gt}0\)) provides at least one partition.

By case analysis on whether the proposition is true or false.

By case analysis on whether the proposition is true or false.

Follows from the definition of the Iverson bracket and the identity \(\sum _{x \in s} \left[ p(x) \right] = |\{ x \in s : p(x)\} |\).

By case split on both propositions.

The partition of \(0\) has no parts, so the maximum (with default \(0\)) is \(0\).

Each part is bounded by \(n\) (by Lemma 2.2).

The largest part is the maximum of all parts, so it is \(\leq m\) iff every part is \(\leq m\).

Follows directly from Lemma 2.20.

(a) The size of a partition is always nonnegative (being a sum of positive integers). Thus, a negative number \(n\) has no partitions whatsoever. Thus, \(p_{k}\left( n\right) =0\) whenever \(n{\lt}0\) and \(k\in \mathbb {N}\). (In the formalization, \(n\) is a natural number, so this case is vacuous.)

(b) If \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\right) \) is a partition, then \(\lambda _{i}\geq 1\) for each \(i\in \left\{ 1,2,\ldots ,k\right\} \) (because a partition is a tuple of positive integers, i.e., of integers \(\geq 1\)). Hence, if \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\right) \) is a partition of \(n\) into \(k\) parts, then

Thus, a partition of \(n\) into \(k\) parts cannot satisfy \(k{\gt}n\). Thus, no such partitions exist if \(k{\gt}n\). In other words, \(p_{k}\left( n\right) =0\) if \(k{\gt}n\).

(c) The integer \(0\) has a unique partition into \(0\) parts, namely the empty tuple \(\left( {}\right) \). A nonzero integer \(n\) cannot have any partitions into \(0\) parts, since the empty tuple has size \(0\neq n\). Thus, \(p_{0}\left( n\right) \) equals \(1\) for \(n=0\) and equals \(0\) for \(n\neq 0\). In other words, \(p_{0}\left( n\right) =\left[ n=0 \right]\).

(d) Any positive integer \(n\) has a unique partition into \(1\) part – namely, the \(1\)-tuple \(\left( n\right) \). On the other hand, if \(n\) is not positive, then this \(1\)-tuple is not a partition, so in this case \(n\) has no partition into \(1\) part. Thus, \(p_{1}\left( n\right) \) equals \(1\) if \(n\) is positive and equals \(0\) otherwise. In other words, \(p_{1}\left( n\right) =\left[ n{\gt}0 \right]\).

(e) Assume that \(k{\gt}0\). We must prove that \(p_{k}\left( n\right) =p_{k}\left( n-k\right) +p_{k-1}\left( n-1\right) \).

We consider all partitions of \(n\) into \(k\) parts. We classify these partitions into two types:

• Type 1 consists of all partitions that have \(1\) as a part.

• Type 2 consists of all partitions that don’t.

Any type-1 partition has \(1\) as a part, therefore as its last part (because it is weakly decreasing). Hence, any type-1 partition has the form \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k-1},1\right) \). If \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k-1},1\right) \) is a type-1 partition (of \(n\) into \(k\) parts), then \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k-1}\right) \) is a partition of \(n-1\) into \(k-1\) parts. Thus, we have a bijection

given by removing the trailing \(1\).

A type-2 partition does not have \(1\) as a part; hence, all its parts are larger than \(1\), and therefore we can subtract \(1\) from each part and still have a partition. If \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\right) \) is a type-2 partition of \(n\) into \(k\) parts, then \(\left( \lambda _{1}-1,\lambda _{2}-1,\ldots ,\lambda _{k}-1\right) \) is a partition of \(n-k\) into \(k\) parts. This gives a bijection

Since any partition of \(n\) into \(k\) parts is either type-1 or type-2, \(p_{k}\left( n\right) =p_{k}\left( n-k\right) +p_{k-1}\left( n-1\right)\).

(f) Let \(n\in \mathbb {N}\). The partitions of \(n\) into \(2\) parts are

Thus there are \(\left\lfloor n/2\right\rfloor \) of them. In other words, \(p_{2}\left( n\right) =\left\lfloor n/2\right\rfloor \).

(g) Let \(n\in \mathbb {N}\). Any partition of \(n\) must have \(k\) parts for some \(k\in \mathbb {N}\). Thus,

(h) Same argument as for (a).

By the disjoint union of the two filtered sets.

The forward map removes one copy of \(1\); the backward map adds one. Injectivity and surjectivity follow from the fact that removing and adding a trailing \(1\) are mutually inverse operations.

The forward map subtracts \(1\) from each part (valid since all parts \({\gt}1\)). The backward map adds \(1\) to each part. Injectivity uses the fact that subtracting \(1\) from each entry is injective on multisets whose all elements are \({\gt}1\).

If the partition has parts \(\{ a, b\} \) with \(b\le a\), then \(a+b = n\) and \(b\ge 1\) (since parts are positive), so \(a = n-b\) and \(2b\le n\).

The forward direction follows by constructing an explicit partition with \(k\) parts when \(0 {\lt} k \leq n\) (namely \((1, 1, \ldots , 1, n - k + 1)\)). The backward direction uses parts (b) and (c) of Proposition 2.22.

We have

where

It suffices to show that \(\left\vert Q_{n}\right\vert =p\left( n\right) \) for each \(n\in \mathbb {N}\).

We construct a bijection \(\pi :Q_{n}\rightarrow \left\{ \text{partitions of }n\right\} \): for any \(\left( u_{1},u_{2},u_{3},\ldots \right) \in Q_{n}\), define

This is a partition of \(n\). Its inverse map \(\rho \) sends each partition \(\lambda \) of \(n\) to \(\left( \text{\# of }1\text{'s in }\lambda ,\text{ \# of }2\text{'s in }\lambda , \ldots \right) \in Q_{n}\).

This proof is analogous to the proof of Theorem 2.30, using \(m\)-tuples instead of infinite sequences. We have

where \(Q_{n}=\left\{ \left( u_{1},u_{2},\ldots ,u_{m}\right) \in \mathbb {N}^{m} \mid \ 1u_{1}+2u_{2}+\cdots +mu_{m}=n\right\} \). It suffices to show \(\left\vert Q_{n}\right\vert =p_{\operatorname {parts}\leq m}\left( n\right)\). The bijection \(\pi :Q_{n}\rightarrow \left\{ \text{partitions }\lambda \text{ of }n\text{ with all parts }\leq m\right\} \) is analogous to that in Theorem 2.30.

Analogous to the proof of Theorem 2.31, with \(\prod _{k=1}^{m}\) replaced by \(\prod _{k\in I}\) and \(m\)-tuples replaced by essentially finite families \((u_i)_{i\in I}\in \mathbb {N}^{I}\).

By definition.

By definition.

This is the characterization of “no duplicates” in terms of counts.

Let \(n\in \mathbb {N}\). We construct a bijection

Given a partition \(\lambda \) of \(n\) into odd parts, we repeatedly merge pairs of equal parts in \(\lambda \) until no more equal parts appear. The final result is \(A\left( \lambda \right) \).

More precisely: if the original partition \(\lambda \) contains an odd part \(k\) exactly \(m\) times, and if the binary representation of \(m\) is \(m = \sum _{j=0}^{i} m_j 2^j\) with \(m_j \in \{ 0,1\} \), then the partition \(A(\lambda )\) contains the number \(2^j k\) exactly \(m_j\) times for each \(j\). Since the binary digits \(m_j\) are all \(\leq 1\), the partition \(A(\lambda )\) has distinct parts.

The inverse map \(B\) starts with a partition \(\lambda \) into distinct parts. Each part \(k \cdot 2^i\) (with \(k\) odd and \(i \geq 0\)) is replaced by \(2^i\) copies of \(k\). Equivalently, one repeatedly splits even parts into halves until only odd parts remain. The result \(B(\lambda )\) is a partition into odd parts.

The maps \(A\) and \(B\) are mutually inverse, establishing the bijection. Thus \(p_{\operatorname {odd}}(n) = p_{\operatorname {dist}}(n)\).

In the formalization, this is proved using Glaisher’s theorem from Mathlib, 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 sum of the new parts equals the original size by a double-counting argument: \(\sum _i \mu _i = \sum _i \# \{ j : \lambda _j \geq i\} = \sum _j \lambda _j = n\).

This is a restatement of the defining property of the transpose.

The proof uses the sorted list representation and the key combinatorial fact that for a sorted decreasing list, the transpose operation is controlled by the count of parts exceeding each threshold (Lemma 2.41). This establishes that applying the Young diagram transpose twice recovers the original partition.

Forward: If \(|\{ k : \ell _k {\gt} i\} | \le j\), then \(\ell _j \le i\) (since the sorted property implies all elements from position \(j\) onward are \(\le \ell _j\), so at most \(j\) elements exceed \(i\)). Contrapositive gives the result.

Backward: If \(\ell _j {\gt} i\), then all \(\ell _0, \ldots , \ell _j\) are \({\gt} i\) (by the sorted property), so \(|\{ k : \ell _k {\gt} i\} | \ge j+1 {\gt} j\).

The transpose has as many parts as there are columns in the Young diagram, which equals the number of boxes in the first row, i.e., the largest part.

If all parts were \(\le i\), then the largest part would be \(\le i\), contradicting \(i {\lt}\) largest part.

Every part of a partition is positive, so restricting to positive parts does not change the count.

The largest part of the transpose is the number of rows in the transposed diagram, which equals the number of rows of the original, i.e., \(\ell (\lambda )\).

We use the transpose as a bijection between:

• partitions of \(n\) with \(k\) parts, and

• partitions of \(n\) with largest part \(k\).

For any partition \(\lambda =\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\right) \), we define the conjugate \(\lambda ^{t}\) by \(\lambda ^{t}=\left( \mu _{1},\mu _{2},\ldots ,\mu _{p}\right) \), where \(p\) is the largest part of \(\lambda \) and \(\mu _{i}=\left( \text{\# of parts of }\lambda \text{ that are }\geq i\right) \) for each \(i\in \left\{ 1,2,\ldots ,p\right\} \). We have \(\left\vert \lambda ^{t}\right\vert =\left\vert \lambda \right\vert \) and \(\left( \lambda ^{t}\right) ^{t}=\lambda \) for each partition \(\lambda \), and the largest part of \(\lambda ^{t}\) equals the length of \(\lambda \). By Lemma 2.45, the transpose sends a partition with \(k\) parts to one whose largest part is \(k\). By Lemma 2.40, the transpose is an involution, hence a bijection. This establishes the result.

We have

(by Proposition 2.46 applied to each \(i\)). This sum counts partitions of \(n\) whose largest part is \(\leq k\).

Direct from the two referenced results.

For each \(n\in \mathbb {N}\), Corollary 2.47 shows that

where \(p_{\operatorname {parts}\leq m}\left( n\right) \) is defined as in Theorem 2.31. Hence,

(by Theorem 2.31).

The proof uses a bijection between the disjoint union \(\bigsqcup _{n\in [k, k\ell ]} \{ p \vdash n : \ell (p)=k,\; \text{largest}=\ell \} \) and the set of \((k-1)\)-element multisubsets of \(\{ 0,1,\ldots ,\ell -1\} \), whose cardinality is \(\binom {\ell + (k-1) - 1}{k-1} = \binom {k+\ell -2}{k-1}\) by the stars-and-bars formula.

Forward map: A \((k-1)\)-element multisubset \(\{ a_1,\ldots ,a_{k-1}\} \subseteq \{ 0,1,\ldots ,\ell -1\} \) maps to the partition \((\ell ,\, a_1+1,\, \ldots ,\, a_{k-1}+1)\) sorted in decreasing order. This has \(k\) parts, largest part \(\ell \), and size \(\ell + \sum (a_i+1) \in [k, k\ell ]\).

Backward map: A partition \((\ell , \lambda _2,\ldots ,\lambda _k)\) maps to the multiset \(\{ \lambda _2-1, \ldots , \lambda _k-1\} \subseteq \{ 0,1,\ldots ,\ell -1\} \), since each \(\lambda _i\in \{ 1,\ldots ,\ell \} \).

The maps are mutual inverses: incrementing each element of the multiset by \(1\) after decrementing undoes the decrement on parts \(\ge 1\), and prepending \(\ell \) to the result of erasing \(\ell \) recovers the original multiset.

Each property follows from elementary multiset operations. In particular, (3) uses \(a_i+1\le \ell \) for \(a_i \in \{ 0,1,\ldots ,\ell -1\} \), and (5) uses the bounds \(1\le a_i+1\le \ell \).

Each partition \(p\) of \(n\) has size \(|p| = n\), so the sum of a constant equals the constant times the count.

This is the standard identity \(\sum _i f(i) = \sum _{j\ge 1}|\{ i : f(i)\ge j\} |\) applied with \(f(p) = \operatorname {count}(d, p)\), bounded by \(n\) since at most \(n/d\) copies of \(d\) fit in a partition of \(n\).

By induction on the multiset of parts.

At most \(n/d\) copies of \(d\) can fit in a partition of \(n\).

Removing copies preserves positivity of remaining parts and adjusts the sum. Adding copies preserves positivity since \(d {\gt} 0\).

The forward map removes \(j\) copies of \(d\) from the partition. The backward map adds \(j\) copies. Both preserve the property that all parts are in \(I\). Injectivity and surjectivity are verified by showing the maps are mutual inverses.

The reindexing bijection is \((k, d) \leftrightarrow (d, j)\) where \(k = d \cdot j - 1\). The forward map sends \((k, d)\) to \((d, (k+1)/d)\) and the backward map sends \((d, j)\) to \((d \cdot j - 1, d)\).

The proof uses a double counting argument. Both sides count weighted pairs.

LHS Analysis:

Swapping the order of summation and using the identity \(\sum _p \operatorname {count}(d, p) = \sum _{j \geq 1} |\{ p : \operatorname {count}(d, p) \geq j\} |\), together with the bijection from Lemma 2.58, gives:

RHS Analysis:

By the reindexing lemma (Lemma 2.59), this equals the same expression.

This is the particular case of Theorem 2.60 for \(I=\left\{ 1,2,3,\ldots \right\} \). We specialize the restricted version with \(I = \{ n \in \mathbb {N} : n {\gt} 0\} \). Since all parts of a partition are positive, the restricted set equals the set of all partitions, so \(p_I(n) = p(n)\). Similarly, \(\sigma _I(n) = \sigma (n)\) since all divisors of a positive integer are positive.

Immediate from the definition of \(P\).

Since \([x^n](X\cdot f') = n\cdot [x^n]f\) for any FPS \(f\).

Expand the Cauchy product \([x^n](S\cdot P) = \sum _{i+j=n} [x^i]S\cdot [x^j]P\), noting that \([x^0]S = 0\) so the \(i=0\) term vanishes.

Comparing coefficients at each \(x^n\): \([x^n](X\cdot P') = n\cdot p(n) = \sum _{k=1}^{n}\sigma (k)\cdot p(n-k) = [x^n](S\cdot P)\), where the middle equality is Theorem 2.61.