mathlib documentation

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 #

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

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

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 #

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

source
theorem composition.ext_iff {n : ℕ} (x y : composition n) :
x = y ↔ x.blocks = y.blocks
source
@[ext]
structure composition (n : ℕ) :
Type

A composition of n is a list of positive integers summing to n.

Instances for composition
source
theorem composition.ext {n : ℕ} (x y : composition n) (h : x.blocks = y.blocks) :
x = y
source
@[ext]
structure composition_as_set (n : ℕ) :
Type

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.

Instances for composition_as_set
source
theorem composition_as_set.ext_iff {n : ℕ} (x y : composition_as_set n) :
x = y ↔ x.boundaries = y.boundaries
source
theorem composition_as_set.ext {n : ℕ} (x y : composition_as_set n) (h : x.boundaries = y.boundaries) :
x = y
source
@[protected, instance]
def composition_as_set.inhabited {n : ℕ} :
inhabited (composition_as_set n)
Equations

Compositions #

A composition of an integer n is a decomposition n = i₀ + ... + i_{k-1} of n into a sum of positive integers.

source
@[protected, instance]
def composition.has_to_string (n : ℕ) :
has_to_string (composition n)
Equations
source
@[reducible]
def composition.length {n : ℕ} (c : composition n) :
ℕ

The length of a composition, i.e., the number of blocks in the composition.

Equations
source
theorem composition.blocks_length {n : ℕ} (c : composition n) :
c.blocks.length = c.length
source
def composition.blocks_fun {n : ℕ} (c : composition n) :
fin c.length → ℕ

The blocks of a composition, seen as a function on fin c.length. When composing analytic functions using compositions, this is the main player.

Equations
source
theorem composition.of_fn_blocks_fun {n : ℕ} (c : composition n) :
list.of_fn c.blocks_fun = c.blocks
source
theorem composition.sum_blocks_fun {n : ℕ} (c : composition n) :
finset.univ.sum (λ (i : fin c.length), c.blocks_fun i) = n
source
theorem composition.blocks_fun_mem_blocks {n : ℕ} (c : composition n) (i : fin c.length) :
c.blocks_fun i ∈ c.blocks
source
@[simp]
theorem composition.one_le_blocks {n : ℕ} (c : composition n) {i : ℕ} (h : i ∈ c.blocks) :
1 ≤ i
source
@[simp]
theorem composition.one_le_blocks' {n : ℕ} (c : composition n) {i : ℕ} (h : i < c.length) :
1 ≤ c.blocks.nth_le i h
source
@[simp]
theorem composition.blocks_pos' {n : ℕ} (c : composition n) (i : ℕ) (h : i < c.length) :
0 < c.blocks.nth_le i h
source
theorem composition.one_le_blocks_fun {n : ℕ} (c : composition n) (i : fin c.length) :
1 ≤ c.blocks_fun i
source
theorem composition.length_le {n : ℕ} (c : composition n) :
c.length ≤ n
source
theorem composition.length_pos_of_pos {n : ℕ} (c : composition n) (h : 0 < n) :
0 < c.length
source
def composition.size_up_to {n : ℕ} (c : composition n) (i : ℕ) :
ℕ

The sum of the sizes of the blocks in a composition up to i.

Equations
source
@[simp]
theorem composition.size_up_to_zero {n : ℕ} (c : composition n) :
c.size_up_to 0 = 0
source
theorem composition.size_up_to_of_length_le {n : ℕ} (c : composition n) (i : ℕ) (h : c.length ≤ i) :
c.size_up_to i = n
source
@[simp]
theorem composition.size_up_to_length {n : ℕ} (c : composition n) :
c.size_up_to c.length = n
source
theorem composition.size_up_to_le {n : ℕ} (c : composition n) (i : ℕ) :
c.size_up_to i ≤ n
source
theorem composition.size_up_to_succ {n : ℕ} (c : composition n) {i : ℕ} (h : i < c.length) :
c.size_up_to (i + 1) = c.size_up_to i + c.blocks.nth_le i h
source
theorem composition.size_up_to_succ' {n : ℕ} (c : composition n) (i : fin c.length) :
c.size_up_to (↑i + 1) = c.size_up_to ↑i + c.blocks_fun i
source
theorem composition.size_up_to_strict_mono {n : ℕ} (c : composition n) {i : ℕ} (h : i < c.length) :
c.size_up_to i < c.size_up_to (i + 1)
source
theorem composition.monotone_size_up_to {n : ℕ} (c : composition n) :
monotone c.size_up_to
source
def composition.boundary {n : ℕ} (c : composition n) :
fin (c.length + 1) ↪o fin (n + 1)

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.

Equations
source
@[simp]
theorem composition.boundary_zero {n : ℕ} (c : composition n) :
⇑(c.boundary) 0 = 0
source
@[simp]
theorem composition.boundary_last {n : ℕ} (c : composition n) :
⇑(c.boundary) (fin.last c.length) = fin.last n
source
def composition.boundaries {n : ℕ} (c : composition n) :
finset (fin (n + 1))

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
source
theorem composition.card_boundaries_eq_succ_length {n : ℕ} (c : composition n) :
c.boundaries.card = c.length + 1
source
def composition.to_composition_as_set {n : ℕ} (c : composition n) :
composition_as_set n

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
source
theorem composition.order_emb_of_fin_boundaries {n : ℕ} (c : composition n) :
c.boundaries.order_emb_of_fin _ = c.boundary

The canonical increasing bijection between fin (c.length + 1) and c.boundaries is exactly c.boundary.

source
def composition.embedding {n : ℕ} (c : composition n) (i : fin c.length) :
fin (c.blocks_fun i) ↪o fin n

Embedding the i-th block of a composition (identified with fin (c.blocks_fun i)) into fin n at the relevant position.

Equations
source
@[simp]
theorem composition.coe_embedding {n : ℕ} (c : composition n) (i : fin c.length) (j : fin (c.blocks_fun i)) :
↑(⇑(c.embedding i) j) = c.size_up_to ↑i + ↑j
source
theorem composition.index_exists {n : ℕ} (c : composition n) {j : ℕ} (h : j < n) :
∃ (i : ℕ), j < c.size_up_to i.succ ∧ i < c.length

index_exists asserts there is some i with j < c.size_up_to (i+1). In the next definition index we use nat.find to produce the minimal such index.

source
def composition.index {n : ℕ} (c : composition n) (j : fin n) :
fin c.length

c.index j is the index of the block in the composition c containing j.

Equations
source
theorem composition.lt_size_up_to_index_succ {n : ℕ} (c : composition n) (j : fin n) :
↑j < c.size_up_to ↑((c.index j).succ)
source
theorem composition.size_up_to_index_le {n : ℕ} (c : composition n) (j : fin n) :
c.size_up_to ↑(c.index j) ≤ ↑j
source
def composition.inv_embedding {n : ℕ} (c : composition n) (j : fin n) :
fin (c.blocks_fun (c.index j))

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
source
@[simp]
theorem composition.coe_inv_embedding {n : ℕ} (c : composition n) (j : fin n) :
↑(c.inv_embedding j) = ↑j - c.size_up_to ↑(c.index j)
source
theorem composition.embedding_comp_inv {n : ℕ} (c : composition n) (j : fin n) :
⇑(c.embedding (c.index j)) (c.inv_embedding j) = j
source
theorem composition.mem_range_embedding_iff {n : ℕ} (c : composition n) {j : fin n} {i : fin c.length} :
j ∈ set.range ⇑(c.embedding i) ↔ c.size_up_to ↑i ≤ ↑j ∧ ↑j < c.size_up_to ↑i.succ
source
theorem composition.disjoint_range {n : ℕ} (c : composition n) {i₁ i₂ : fin c.length} (h : i₁ ≠ i₂) :
disjoint (set.range ⇑(c.embedding i₁)) (set.range ⇑(c.embedding i₂))

The embeddings of different blocks of a composition are disjoint.

source
theorem composition.mem_range_embedding {n : ℕ} (c : composition n) (j : fin n) :
j ∈ set.range ⇑(c.embedding (c.index j))
source
theorem composition.mem_range_embedding_iff' {n : ℕ} (c : composition n) {j : fin n} {i : fin c.length} :
j ∈ set.range ⇑(c.embedding i) ↔ i = c.index j
source
theorem composition.index_embedding {n : ℕ} (c : composition n) (i : fin c.length) (j : fin (c.blocks_fun i)) :
c.index (⇑(c.embedding i) j) = i
source
theorem composition.inv_embedding_comp {n : ℕ} (c : composition n) (i : fin c.length) (j : fin (c.blocks_fun i)) :
↑(c.inv_embedding (⇑(c.embedding i) j)) = ↑j
source
def composition.blocks_fin_equiv {n : ℕ} (c : composition n) :
(Σ (i : fin c.length), fin (c.blocks_fun i)) ≃ fin n

Equivalence between the disjoint union of the blocks (each of them seen as fin (c.blocks_fun i)) with fin n.

Equations
source
theorem composition.blocks_fun_congr {n₁ n₂ : ℕ} (c₁ : composition n₁) (c₂ : composition n₂) (i₁ : fin c₁.length) (i₂ : fin c₂.length) (hn : n₁ = n₂) (hc : c₁.blocks = c₂.blocks) (hi : ↑i₁ = ↑i₂) :
c₁.blocks_fun i₁ = c₂.blocks_fun i₂
source
theorem composition.sigma_eq_iff_blocks_eq {c c' : Σ (n : ℕ), composition n} :
c = c' ↔ c.snd.blocks = c'.snd.blocks

Two compositions (possibly of different integers) coincide if and only if they have the same sequence of blocks.

The composition composition.ones #

source
def composition.ones (n : ℕ) :
composition n

The composition made of blocks all of size 1.

Equations
source
@[protected, instance]
def composition.inhabited {n : ℕ} :
inhabited (composition n)
Equations
source
@[simp]
theorem composition.ones_length (n : ℕ) :
(composition.ones n).length = n
source
@[simp]
theorem composition.ones_blocks (n : ℕ) :
(composition.ones n).blocks = list.repeat 1 n
source
@[simp]
theorem composition.ones_blocks_fun (n : ℕ) (i : fin (composition.ones n).length) :
(composition.ones n).blocks_fun i = 1
source
@[simp]
theorem composition.ones_size_up_to (n i : ℕ) :
(composition.ones n).size_up_to i = linear_order.min i n
source
@[simp]
theorem composition.ones_embedding {n : ℕ} (i : fin (composition.ones n).length) (h : 0 < (composition.ones n).blocks_fun i) :
⇑((composition.ones n).embedding i) ⟨0, h⟩ = ⟨↑i, _⟩
source
theorem composition.eq_ones_iff {n : ℕ} {c : composition n} :
c = composition.ones n ↔ ∀ (i : ℕ), i ∈ c.blocks → i = 1
source
theorem composition.ne_ones_iff {n : ℕ} {c : composition n} :
c ≠ composition.ones n ↔ ∃ (i : ℕ) (H : i ∈ c.blocks), 1 < i
source
theorem composition.eq_ones_iff_length {n : ℕ} {c : composition n} :
c = composition.ones n ↔ c.length = n
source
theorem composition.eq_ones_iff_le_length {n : ℕ} {c : composition n} :
c = composition.ones n ↔ n ≤ c.length

The composition composition.single #

source
def composition.single (n : ℕ) (h : 0 < n) :
composition n

The composition made of a single block of size n.

Equations
source
@[simp]
theorem composition.single_length {n : ℕ} (h : 0 < n) :
(composition.single n h).length = 1
source
@[simp]
theorem composition.single_blocks {n : ℕ} (h : 0 < n) :
(composition.single n h).blocks = [n]
source
@[simp]
theorem composition.single_blocks_fun {n : ℕ} (h : 0 < n) (i : fin (composition.single n h).length) :
(composition.single n h).blocks_fun i = n
source
@[simp]
theorem composition.single_embedding {n : ℕ} (h : 0 < n) (i : fin n) :
⇑((composition.single n h).embedding ⟨0, _⟩) i = i
source
theorem composition.eq_single_iff_length {n : ℕ} (h : 0 < n) {c : composition n} :
c = composition.single n h ↔ c.length = 1
source
theorem composition.ne_single_iff {n : ℕ} (hn : 0 < n) {c : composition n} :
c ≠ composition.single n hn ↔ ∀ (i : fin c.length), c.blocks_fun i < n

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.

source
def list.split_wrt_composition_aux {α : Type u_1} :
list α → list ℕ → list (list α)

Auxiliary for list.split_wrt_composition.

Equations
source
def list.split_wrt_composition {n : ℕ} {α : Type u_1} (l : list α) (c : composition n) :
list (list α)

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
source
theorem list.split_wrt_composition_aux_cons {α : Type u_1} (l : list α) (n : ℕ) (ns : list ℕ) :
l.split_wrt_composition_aux (n :: ns) = list.take n l :: (list.drop n l).split_wrt_composition_aux ns
source
theorem list.length_split_wrt_composition_aux {α : Type u_1} (l : list α) (ns : list ℕ) :
(l.split_wrt_composition_aux ns).length = ns.length
source
@[simp]
theorem list.length_split_wrt_composition {n : ℕ} {α : Type u_1} (l : list α) (c : composition n) :
(l.split_wrt_composition c).length = c.length

When one splits a list along a composition c, the number of sublists thus created is c.length.

source
theorem list.map_length_split_wrt_composition_aux {α : Type u_1} {ns : list ℕ} {l : list α} :
ns.sum ≤ l.length → list.map list.length (l.split_wrt_composition_aux ns) = ns
source
theorem list.map_length_split_wrt_composition {α : Type u_1} (l : list α) (c : composition l.length) :
list.map list.length (l.split_wrt_composition c) = c.blocks

When one splits a list along a composition c, the lengths of the sublists thus created are given by the block sizes in c.

source
theorem list.length_pos_of_mem_split_wrt_composition {α : Type u_1} {l l' : list α} {c : composition l.length} (h : l' ∈ l.split_wrt_composition c) :
0 < l'.length
source
theorem list.sum_take_map_length_split_wrt_composition {α : Type u_1} (l : list α) (c : composition l.length) (i : ℕ) :
(list.take i (list.map list.length (l.split_wrt_composition c))).sum = c.size_up_to i
source
theorem list.nth_le_split_wrt_composition_aux {α : Type u_1} (l : list α) (ns : list ℕ) {i : ℕ} (hi : i < (l.split_wrt_composition_aux ns).length) :
(l.split_wrt_composition_aux ns).nth_le i hi = list.drop (list.take i ns).sum (list.take (list.take (i + 1) ns).sum l)
source
theorem list.nth_le_split_wrt_composition {n : ℕ} {α : Type u_1} (l : list α) (c : composition n) {i : ℕ} (hi : i < (l.split_wrt_composition c).length) :
(l.split_wrt_composition c).nth_le i hi = list.drop (c.size_up_to i) (list.take (c.size_up_to (i + 1)) l)

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.

source
theorem list.join_split_wrt_composition_aux {α : Type u_1} {ns : list ℕ} {l : list α} :
ns.sum = l.length → (l.split_wrt_composition_aux ns).join = l
source
@[simp]
theorem list.join_split_wrt_composition {α : Type u_1} (l : list α) (c : composition l.length) :
(l.split_wrt_composition c).join = l

If one splits a list along a composition, and then joins the sublists, one gets back the original list.

source
@[simp]
theorem list.split_wrt_composition_join {α : Type u_1} (L : list (list α)) (c : composition L.join.length) (h : list.map list.length L = c.blocks) :
L.join.split_wrt_composition c = L

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.

source
def composition_as_set_equiv (n : ℕ) :
composition_as_set n ≃ finset (fin (n - 1))

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
source
@[protected, instance]
def composition_as_set_fintype (n : ℕ) :
fintype (composition_as_set n)
Equations
source
theorem composition_as_set_card (n : ℕ) :
fintype.card (composition_as_set n) = 2 ^ (n - 1)
source
theorem composition_as_set.boundaries_nonempty {n : ℕ} (c : composition_as_set n) :
c.boundaries.nonempty
source
theorem composition_as_set.card_boundaries_pos {n : ℕ} (c : composition_as_set n) :
0 < c.boundaries.card
source
def composition_as_set.length {n : ℕ} (c : composition_as_set n) :
ℕ

Number of blocks in a composition_as_set.

Equations
source
theorem composition_as_set.card_boundaries_eq_succ_length {n : ℕ} (c : composition_as_set n) :
c.boundaries.card = c.length + 1
source
theorem composition_as_set.length_lt_card_boundaries {n : ℕ} (c : composition_as_set n) :
c.length < c.boundaries.card
source
theorem composition_as_set.lt_length {n : ℕ} (c : composition_as_set n) (i : fin c.length) :
↑i + 1 < c.boundaries.card
source
theorem composition_as_set.lt_length' {n : ℕ} (c : composition_as_set n) (i : fin c.length) :
↑i < c.boundaries.card
source
def composition_as_set.boundary {n : ℕ} (c : composition_as_set n) :
fin c.boundaries.card ↪o fin (n + 1)

Canonical increasing bijection from fin c.boundaries.card to c.boundaries.

Equations
source
@[simp]
theorem composition_as_set.boundary_zero {n : ℕ} (c : composition_as_set n) :
⇑(c.boundary) ⟨0, _⟩ = 0
source
@[simp]
theorem composition_as_set.boundary_length {n : ℕ} (c : composition_as_set n) :
⇑(c.boundary) ⟨c.length, _⟩ = fin.last n
source
def composition_as_set.blocks_fun {n : ℕ} (c : composition_as_set n) (i : fin c.length) :
ℕ

Size of the i-th block in a composition_as_set, seen as a function on fin c.length.

Equations
source
theorem composition_as_set.blocks_fun_pos {n : ℕ} (c : composition_as_set n) (i : fin c.length) :
0 < c.blocks_fun i
source
def composition_as_set.blocks {n : ℕ} (c : composition_as_set n) :
list ℕ

List of the sizes of the blocks in a composition_as_set.

Equations
source
@[simp]
theorem composition_as_set.blocks_length {n : ℕ} (c : composition_as_set n) :
c.blocks.length = c.length
source
theorem composition_as_set.blocks_partial_sum {n : ℕ} (c : composition_as_set n) {i : ℕ} (h : i < c.boundaries.card) :
(list.take i c.blocks).sum = ↑(⇑(c.boundary) ⟨i, h⟩)
source
theorem composition_as_set.mem_boundaries_iff_exists_blocks_sum_take_eq {n : ℕ} (c : composition_as_set n) {j : fin (n + 1)} :
j ∈ c.boundaries ↔ ∃ (i : ℕ) (H : i < c.boundaries.card), (list.take i c.blocks).sum = ↑j
source
theorem composition_as_set.blocks_sum {n : ℕ} (c : composition_as_set n) :
c.blocks.sum = n
source
def composition_as_set.to_composition {n : ℕ} (c : composition_as_set n) :
composition n

Associating a composition n to a composition_as_set n, by registering the sizes of the blocks as a list of positive integers.

Equations

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.

source
@[simp]
theorem composition.to_composition_as_set_length {n : ℕ} (c : composition n) :
c.to_composition_as_set.length = c.length
source
@[simp]
theorem composition_as_set.to_composition_length {n : ℕ} (c : composition_as_set n) :
c.to_composition.length = c.length
source
@[simp]
theorem composition.to_composition_as_set_blocks {n : ℕ} (c : composition n) :
c.to_composition_as_set.blocks = c.blocks
source
@[simp]
theorem composition_as_set.to_composition_blocks {n : ℕ} (c : composition_as_set n) :
c.to_composition.blocks = c.blocks
source
@[simp]
theorem composition_as_set.to_composition_boundaries {n : ℕ} (c : composition_as_set n) :
c.to_composition.boundaries = c.boundaries
source
@[simp]
theorem composition.to_composition_as_set_boundaries {n : ℕ} (c : composition n) :
c.to_composition_as_set.boundaries = c.boundaries
source
def composition_equiv (n : ℕ) :
composition n ≃ composition_as_set n

Equivalence between composition n and composition_as_set n.

Equations
source
@[protected, instance]
def composition_fintype (n : ℕ) :
fintype (composition n)
Equations
source
theorem composition_card (n : ℕ) :
fintype.card (composition n) = 2 ^ (n - 1)