Compositions
A composition of an integer 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 nis a structure, made of a list of integers which are all positive and add up ton.composition_cardstates that the cardinality ofcomposition nis exactly2^(n-1), which is proved by constructing an equiv withcomposition_as_set n(see below), which is itself in bijection with the subsets offin (n-1)(this holds even forn = 0, where-is nat subtraction).
Let c : composition n be a composition of n. Then
c.blocksis the list of blocks inc.c.lengthis the number of blocks in the composition.c.blocks_fun : fin c.length → ℕis the realization ofc.blocksas a function onfin c.length. This is the main object when using compositions to understand the composition of analytic functions.c.size_up_to : ℕ → ℕis the sum of the size of the blocks up toi.;c.embedding i : fin (c.blocks_fun i) → fin nis the increasing embedding of thei-th block infin n;c.index j, forj : fin n, is the index of the block containingj.
Compositions can also be used to split lists. Let l be a list of length n and c a composition
of n.
l.split_wrt_composition cis a list of lists, made of the slices oflcorresponding to the blocks ofc.join_split_wrt_compositionstates that splitting a list and then joining it gives back the original list.split_wrt_composition_joinstates 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 : composition_as_set 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 composition_as_set n. We
only construct basic API on composition_as_set (notably c.length and c.blocks) to be able
to construct this equiv, called composition_equiv n. Since there is a straightforward equiv
between composition_as_set n and finsets of {1, ..., n-1} (obtained by removing 0 and n
from a composition_as_set and called composition_as_set_equiv n), we deduce that
composition_as_set n and composition n are both fintypes of cardinality 2^(n - 1)
(see composition_as_set_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
References
- boundaries : finset (fin n.succ)
- zero_mem : 0 ∈ c.boundaries
- last_mem : fin.last n ∈ c.boundaries
Combinatorial viewpoint on a composition of n, by seeing it as non-empty blocks of
consecutive integers in {0, ..., n-1}. We register every block by its left end-point, yielding
a finset containing 0. As this does not make sense for n = 0, we add n to this finset, and
get a finset of {0, ..., n} containing 0 and n. This is the data in the structure
composition_as_set n.
Equations
- composition_as_set.inhabited = {default := {boundaries := finset.univ (fin.fintype n.succ), zero_mem := _, last_mem := _}}
Compositions
A composition of an integer n is a decomposition n = i₀ + ... + i_{k-1} of n into a sum of
positive integers.
Equations
- composition.has_to_string n = {to_string := λ (c : composition n), to_string c.blocks}
The length of a composition, i.e., the number of blocks in the composition.
The blocks of a composition, seen as a function on fin c.length. When composing analytic
functions using compositions, this is the main player.
The sum of the sizes of the blocks in a composition up to i.
Equations
- c.size_up_to i = (list.take i c.blocks).sum
The i-th boundary of a composition, i.e., the leftmost point of the i-th block. We include
a virtual point at the right of the last block, to make for a nice equiv with
composition_as_set n.
The boundaries of a composition, i.e., the leftmost point of all the blocks. We include
a virtual point at the right of the last block, to make for a nice equiv with
composition_as_set n.
Equations
To c : composition n, one can associate a composition_as_set n by registering the leftmost
point of each block, and adding a virtual point at the right of the last block.
Equations
- c.to_composition_as_set = {boundaries := c.boundaries, zero_mem := _, last_mem := _}
The canonical increasing bijection between fin (c.length + 1) and c.boundaries is
exactly c.boundary.
Embedding the i-th block of a composition (identified with fin (c.blocks_fun i)) into
fin n at the relevant position.
Equations
- c.embedding i = λ (j : fin (c.blocks_fun i)), ⟨c.size_up_to i.val + j.val, _⟩
index_exists asserts there is some i so j < c.size_up_to (i+1).
In the next definition we use nat.find to produce the minimal such index.
Mapping an element j of fin n to the element in the block containing it, identified with
fin (c.blocks_fun (c.index j)) through the canonical increasing bijection.
Equations
- c.inv_embedding j = ⟨↑j - c.size_up_to ↑(c.index j), _⟩
Equivalence between the disjoint union of the blocks (each of them seen as
fin (c.blocks_fun i)) with fin n.
The composition made of blocks all of size 1.
Equations
- composition.ones n = {blocks := list.repeat 1 n, blocks_pos := _, blocks_sum := _}
Equations
The composition made of a single block of size n.
Equations
- composition.single n h = {blocks := [n], blocks_pos := _, blocks_sum := _}
Splitting a list
Given a list of length n and a composition c of n, one can split l into c.length sublists
of respective lengths c.blocks_fun 0, ..., c.blocks_fun (c.length-1). This is inverse to the
join operation.
Auxiliary for list.split_wrt_composition.
Equations
- l.split_wrt_composition_aux (n :: ns) = list.split_wrt_composition_aux._match_1 (λ (l₂ : list α), l₂.split_wrt_composition_aux ns) (list.split_at n l)
- l.split_wrt_composition_aux list.nil = list.nil
- list.split_wrt_composition_aux._match_1 _f_1 (l₁, l₂) = l₁ :: _f_1 l₂
Given a list of length n and a composition [i₁, ..., iₖ] of n, split l into a list of
k lists corresponding to the blocks of the composition, of respective lengths i₁, ..., iₖ.
This makes sense mostly when n = l.length, but this is not necessary for the definition.
Equations
When one splits a list along a composition c, the number of sublists thus created is
c.length.
When one splits a list along a composition c, the lengths of the sublists thus created are
given by the block sizes in c.
The i-th sublist in the splitting of a list l along a composition c, is the slice of l
between the indices c.size_up_to i and c.size_up_to (i+1), i.e., the indices in the i-th
block of the composition.
If one splits a list along a composition, and then joins the sublists, one gets back the original list.
If one joins a list of lists and then splits the join along the right composition, one gets back the original list of lists.
Compositions as sets
Combinatorial viewpoints on compositions, seen as finite subsets of fin (n+1) containing 0 and
n, where the points of the set (other than n) correspond to the leftmost points of each block.
Bijection between compositions of n and subsets of {0, ..., n-2}, defined by
considering the restriction of the subset to {1, ..., n-1} and shifting to the left by one.
Equations
- composition_as_set_equiv n = {to_fun := λ (c : composition_as_set n), {i : fin (n - 1) | ⟨1 + i.val, _⟩ ∈ c.boundaries}.to_finset, inv_fun := λ (s : finset (fin (n - 1))), {boundaries := {i : fin n.succ | i = 0 ∨ i = fin.last n ∨ ∃ (j : fin (n - 1)) (hj : j ∈ s), i.val = j.val + 1}.to_finset (subtype.fintype (λ (x : fin n.succ), x ∈ {i : fin n.succ | i = 0 ∨ i = fin.last n ∨ ∃ (j : fin (n - 1)) (hj : j ∈ s), i.val = j.val + 1})), zero_mem := _, last_mem := _}, left_inv := _, right_inv := _}
Equations
- composition_as_set_fintype n = fintype.of_equiv (finset (fin (n - 1))) (composition_as_set_equiv n).symm
Number of blocks in a composition_as_set.
Equations
- c.length = c.boundaries.card - 1
Canonical increasing bijection from fin c.boundaries.card to c.boundaries.
Equations
- c.boundary = c.boundaries.mono_of_fin _
List of the sizes of the blocks in a composition_as_set.
Equations
- c.blocks = list.of_fn c.blocks_fun
Associating a composition n to a composition_as_set n, by registering the sizes of the
blocks as a list of positive integers.
Equations
- c.to_composition = {blocks := c.blocks, blocks_pos := _, blocks_sum := _}
Equivalence between compositions and compositions as sets
In this section, we explain how to go back and forth between a composition and a
composition_as_set, by showing that their blocks and length and boundaries correspond to
each other, and construct an equivalence between them called composition_equiv.
Equivalence between composition n and composition_as_set n.
Equations
- composition_equiv n = {to_fun := λ (c : composition n), c.to_composition_as_set, inv_fun := λ (c : composition_as_set n), c.to_composition, left_inv := _, right_inv := _}