By definition.

By definition.

By definition.

By definition of length.

By induction on the composition. The base case (empty composition) is trivial. For the inductive step, \(|\alpha | = a + |\beta | \geq 1 + \ell (\beta ) = \ell (\alpha )\) since \(a \geq 1\).

If \(\alpha = (a) \cdot \beta \), then \(|\alpha | = a + |\beta | \geq 1 {\gt} 0\) since \(a\) is a positive integer. Hence a composition of size \(0\) must be empty.

Convert between lists of positive integers and lists of natural numbers with positivity proofs.

Follows from the equivalence in Lemma 1.298, restricting to compositions of the appropriate length.

This is the composition of the Mathlib equivalences between compositions of \(n\), composition-as-set representations, and finite subsets of \(\{ 1, 2, \ldots , n-1\} \).

The boundary set of \(c\) has \(\ell (c) + 1\) elements (including \(0\) and \(n\)). The equivalence maps to the interior points, obtained by removing \(0\) and \(n\). The resulting finset has \(\ell (c) + 1 - 2 = \ell (c) - 1\) elements.

Follows directly from Lemma 1.301 applied to the composition-as-set representation of \(c\).

Compositions of length \(k\) correspond (via the composition-to-finset equivalence) to \((k-1)\)-element subsets of \(\{ 1, 2, \ldots , n-1\} \). These are counted by \(\binom {n-1}{k-1}\).

Fix \(k\in \mathbb {N}\), but don’t fix \(n\). Let

We want to find \(a_{n,k}\). We define the generating function

Let us write \(\mathbb {P}\) for the set \(\left\{ 1,2,3,\ldots \right\} \). Then, a composition of \(n\) into \(k\) parts is nothing but a \(k\)-tuple \(\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{k}\right) \in \mathbb {P}^{k}\) satisfying \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{k}=n\). Hence, (35) can be rewritten as

Thus, we can rewrite the equality \(A_{k}=\sum _{n\in \mathbb {N}}a_{n,k}x^{n}\) as

(here, we have renamed all the \(k\) summation indices as \(n\), and realized that all \(k\) sums are identical). Since

this can be rewritten further as

In order to simplify this, we need to expand \(\left( 1-x\right) ^{-k}\). This is routine by now: Theorem 1.119 (applied to \(-k\) instead of \(n\)) yields

Substituting \(-x\) for \(x\) on both sides of this equality (i.e., applying the map \(f\mapsto f\circ \left( -x\right) \)), we obtain

(where we used Theorem 1.120, applied to \(k\) and \(j\) instead of \(n\) and \(k\), to simplify \(\binom {-k}{j}\); and we have substituted \(n-k\) for \(j\) in the sum). Hence, our above computation of \(A_{k}\) can be completed as follows:

(here, we have extended the range of the summation from all \(n\geq k\) to all \(n\in \mathbb {N}\); this did not change the sum, since all the newly introduced addends with \(n{\lt}k\) are \(0\)). Comparing coefficients, we thus obtain

If \(n{\gt}0\), then we can rewrite the right hand side of this equality as \(\binom {n-1}{k-1}\) (using Theorem 1.9). However, if \(n=0\), then this right hand side equals \(\delta _{k,0}\) instead (where we are using Definition 1.167). Thus, we can rewrite (40) as

In the Lean formalization, this proceeds by:

1. Using the equivalence between our compositions and Mathlib’s composition type (Lemma 1.299).

2. Using Mathlib’s equivalence between compositions of \(n\) and subsets of \(\{ 1, 2, \ldots , n-1\} \).

3. Showing that compositions of length \(k\) correspond to subsets of size \(k-1\).

4. Computing \(|\{ S \subseteq \{ 1, \ldots , n-1\} \mid |S| = k-1\} | = \binom {n-1}{k-1}\) using the formula for counting subsets of a given size.

The edge cases are:

• For \(n {\gt} 0\) and \(k = 0\): There are no compositions (since parts are positive, and a tuple of zero positive integers sums to \(0\), not \(n\)). This gives \(0 = \binom {n-1}{-1} = 0\).

• For \(n = 0\): The empty tuple is the only composition of \(0\) (by Lemma 1.297), and it has length \(0\). So the count is \(\delta _{k,0}\).

If \(n=0\), then the # of compositions of \(n\) is \(1\) (since the empty tuple \(\left( {}\right) \) is the only composition of \(0\)). Thus, for the rest of this proof, we WLOG assume that \(n\neq 0\). Hence, we must prove that the # of compositions of \(n\) is \(2^{n-1}\).

If \(\left( n_{1},n_{2},\ldots ,n_{m}\right) \) is a composition of \(n\), then \(m\in \left\{ 1,2,\ldots ,n\right\} \). In other words, any composition of \(n\) is a composition of \(n\) into \(k\) parts for some \(k\in \left\{ 1,2,\ldots ,n\right\} \). Hence,

(where the second equality uses Theorem 1.304; and we have substituted \(k\) for \(n-k\) in the sum). Comparing this with

we obtain \(\left( \text{\# of compositions of }n\right) =2^{n-1}\).

In the Lean formalization, this is proved by establishing an equivalence with Mathlib’s composition type (Lemma 1.298) and using Mathlib’s theorem on the cardinality of compositions.

The forward direction converts a list \([\alpha _0, \alpha _1, \ldots , \alpha _{k-1}]\) to the function \(i \mapsto \alpha _i\). The backward direction converts a function \(f\) to the list \([f(0), f(1), \ldots , f(k-1)]\).

The bijection sends \(f : \{ 0, \ldots , k-1\} \to \mathbb {N}\) with \(\sum _i f(i) = n\) to the multiset containing \(f(i)\) copies of \(i\) for each \(i\), and the inverse sends a multiset \(m\) to the function \(i \mapsto \text{count}(i, m)\).

If \(\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{k}\right) \) is a weak composition of \(n\) into \(k\) parts, then \(\left( \alpha _{1}+1,\alpha _{2}+1,\ldots ,\alpha _{k}+1\right) \) is a composition of \(n+k\) into \(k\) parts (since adding \(1\) to each nonnegative entry yields a positive integer, and the sum increases by \(k\)). The inverse map subtracts \(1\) from each entry.

By the equivalence with multisets of size \(n\) from a \(k\)-element alphabet and the formula \(\binom {n + k - 1}{n}\) for counting such multisets.

Adding \(1\) to each entry of a weak composition of \(n\) into \(k\) parts gives a composition of \(n+k\) into \(k\) parts (Lemma 1.309). This map is a bijection (its inverse subtracts \(1\) from each entry). Thus, by the bijection principle, we have

(Here, the last step follows by Theorem 1.304, applied to \(n+k\) instead of \(n\).) It remains to prove that this equals \(\begin{cases} \binom {n+k-1}{k-1}, & \text{if }k{\gt}0;\\ \delta _{n,0}, & \text{if }k=0 \end{cases} \) as well. If \(k=0\), then it is clear by inspection; otherwise it follows from Theorem 1.9.

In the Lean formalization, the primary proof uses the “stars and bars” technique: weak compositions of \(n\) into \(k\) parts are equivalent to multisets of size \(n\) from a \(k\)-element alphabet, via Lemmas 1.307 and 1.308. These are counted by \(\binom {n+k-1}{n}\) using the formula for counting multisets.

By induction on \(p\) and ring arithmetic.

Multiply both sides by \((1 - x)\) and use Lemma 1.312.

By induction on \(k\), using the identity \((1-x)^{-(a+b)} = (1-x)^{-a} \cdot (1-x)^{-b}\) from Mathlib.

This is a standard result from Mathlib’s power series library.

Use Lemma 1.313 and raise both sides to the \(k\)-th power, using Lemma 1.314 to simplify \(\left((1-x)^{-1}\right)^k = (1-x)^{-k}\).

Use the product rule for power series coefficients and show that the product of indicator functions picks out exactly the bounded weak compositions summing to \(n\).

Expand the product \((1-x^p)^k \cdot (1-x)^{-k}\) using the binomial theorem for \((1-x^p)^k\) and the expansion of \((1-x)^{-k}\) via Lemma 1.315, then extract the coefficient of \(x^n\) via the convolution formula.

We fix three nonnegative integers \(n\), \(k\) and \(p\). We are looking for the # of \(k\)-tuples \(\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{k}\right) \in \left\{ 0,1,\ldots ,p-1\right\} ^{k}\) satisfying \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{k}=n\). In other words, we are looking for the # of all weak compositions of \(n\) into \(k\) parts with the property that each entry is \({\lt}p\). Let us denote this # by \(w_{n,k,p}\).

We invoke a generating function. Define the FPS

For each \(n\in \mathbb {N}\), we have

Thus, we can rewrite \(W_{k,p}=\sum _{n\in \mathbb {N}}w_{n,k,p}x^{n}\) as

(by the product rule). Since

this can be rewritten further as

In order to expand the right hand side, let us expand \(\left( 1-x^{p}\right) ^{k}\) and \(\left( 1-x\right) ^{-k}\) separately.

The binomial theorem yields

Multiplying this by (39), we obtain

Thus, (50) becomes

Comparing coefficients, we find that each \(n\in \mathbb {N}\) satisfies

Establish a bijection between binary \(k\)-strings with \(n\) ones and \(n\)-element subsets of \(\{ 1, 2, \ldots , k\} \) (a binary string corresponds to the set of positions where a \(1\) appears). Then use the formula for counting subsets of a given size.

The \(k\)-tuples \(\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{k}\right) \in \left\{ 0,1\right\} ^{k}\) are just the binary \(k\)-strings, i.e., the \(k\)-tuples formed of \(0\)s and \(1\)s. Imposing the condition \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{k}=n\) on such a \(k\)-tuple is tantamount to requiring that it contain exactly \(n\) many \(1\)s. Therefore, the # of all \(k\)-tuples \(\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{k}\right) \in \left\{ 0,1\right\} ^{k}\) satisfying \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{k}=n\) is \(\binom {k}{n}\), since we have to choose which \(n\) of its \(k\) positions will be occupied by \(1\)s (Lemma 1.320). However, Theorem 1.319 (applied to \(p=2\)) yields that this # equals \(\sum _{j=0}^{k}\left( -1\right) ^{j}\binom {k}{j}\binom {n-2j+k-1}{n-2j}\). Comparing these two results, we obtain the identity.