# Documentation

Mathlib.Combinatorics.Composition

# Compositions #

A composition of a natural number n is a decomposition n = i₀ + ... + i_{k-1} of n into a sum of positive integers. Combinatorially, it corresponds to a decomposition of {0, ..., n-1} into non-empty blocks of consecutive integers, where the iⱼ are the lengths of the blocks. This notion is closely related to that of a partition of n, but in a composition of n the order of the iⱼs matters.

We implement two different structures covering these two viewpoints on compositions. The first one, made of a list of positive integers summing to n, is the main one and is called Composition n. The second one is useful for combinatorial arguments (for instance to show that the number of compositions of n is 2^(n-1)). It is given by a subset of {0, ..., n} containing 0 and n, where the elements of the subset (other than n) correspond to the leftmost points of each block. The main API is built on Composition n, and we provide an equivalence between the two types.

## Main functions #

• c : Composition n is a structure, made of a list of integers which are all positive and add up to n.
• composition_card states that the cardinality of Composition n is exactly 2^(n-1), which is proved by constructing an equiv with CompositionAsSet n (see below), which is itself in bijection with the subsets of Fin (n-1) (this holds even for n = 0, where - is nat subtraction).

Let c : Composition n be a composition of n. Then

• c.blocks is the list of blocks in c.

• c.length is the number of blocks in the composition.

• c.blocks_fun : Fin c.length → ℕ is the realization of c.blocks as a function on Fin c.length. This is the main object when using compositions to understand the composition of analytic functions.

• c.sizeUpTo : ℕ → ℕ is the sum of the size of the blocks up to i.;

• c.embedding i : Fin (c.blocks_fun i) → Fin n is the increasing embedding of the i-th block in Fin n;

• c.index j, for j : Fin n, is the index of the block containing j.

• Composition.ones n is the composition of n made of ones, i.e., [1, ..., 1].

• Composition.single n (hn : 0 < n) is the composition of n made of a single block of size n.

Compositions can also be used to split lists. Let l be a list of length n and c a composition of n.

• l.splitWrtComposition c is a list of lists, made of the slices of l corresponding to the blocks of c.
• join_splitWrtComposition states that splitting a list and then joining it gives back the original list.
• joinSplitWrtComposition_join states that joining a list of lists, and then splitting it back according to the right composition, gives back the original list of lists.

We turn to the second viewpoint on compositions, that we realize as a finset of Fin (n+1). c : CompositionAsSet n is a structure made of a finset of Fin (n+1) called c.boundaries and proofs that it contains 0 and n. (Taking a finset of Fin n containing 0 would not make sense in the edge case n = 0, while the previous description works in all cases). The elements of this set (other than n) correspond to leftmost points of blocks. Thus, there is an equiv between Composition n and CompositionAsSet n. We only construct basic API on CompositionAsSet (notably c.length and c.blocks) to be able to construct this equiv, called compositionEquiv n. Since there is a straightforward equiv between CompositionAsSet n and finsets of {1, ..., n-1} (obtained by removing 0 and n from a CompositionAsSet and called compositionAsSetEquiv n), we deduce that CompositionAsSet n and Composition n are both fintypes of cardinality 2^(n - 1) (see compositionAsSet_card and composition_card).

## Implementation details #

The main motivation for this structure and its API is in the construction of the composition of formal multilinear series, and the proof that the composition of analytic functions is analytic.

The representation of a composition as a list is very handy as lists are very flexible and already have a well-developed API.

## Tags #

Composition, partition

https://en.wikipedia.org/wiki/Composition_(combinatorics)