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.blocksFun : 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.blocksFun 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.
• splitWrtComposition_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

References

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

structure Composition (n : ℕ) : Type

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

• blocks : List ℕ

  List of positive integers summing to n

• blocks_pos {i : ℕ} : i ∈ self.blocks → 0 < i

  Proof of positivity for blocks

• blocks_sum : self.blocks.sum = n

  Proof that blocks sums to n

theorem Composition.ext_iff {n : ℕ} {x y : Composition n} : x = y ↔ x.blocks = y.blocks

theorem Composition.ext {n : ℕ} {x y : Composition n} (blocks : x.blocks = y.blocks) : x = y

def instDecidableEqComposition.decEq {n✝ : ℕ} (x✝ x✝¹ : Composition n✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqComposition {n✝ : ℕ} : DecidableEq (Composition n✝)

structure CompositionAsSet (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 CompositionAsSet n.

• boundaries : Finset (Fin n.succ)

  Combinatorial viewpoint on a composition of n as consecutive integers {0, ..., n-1}

• zero_mem : 0 ∈ self.boundaries

  Proof that 0 is a member of boundaries

• getLast_mem : Fin.last n ∈ self.boundaries

  Last element of the composition

theorem CompositionAsSet.ext {n : ℕ} {x y : CompositionAsSet n} (boundaries : x.boundaries = y.boundaries) : x = y

theorem CompositionAsSet.ext_iff {n : ℕ} {x y : CompositionAsSet n} : x = y ↔ x.boundaries = y.boundaries

def instDecidableEqCompositionAsSet.decEq {n✝ : ℕ} (x✝ x✝¹ : CompositionAsSet n✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqCompositionAsSet {n✝ : ℕ} : DecidableEq (CompositionAsSet n✝)

@[implicit_reducible]

instance instInhabitedCompositionAsSet {n : ℕ} : Inhabited (CompositionAsSet n)

Compositions

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

@[implicit_reducible]

instance Composition.instToString (n : ℕ) : ToString (Composition n)

@[reducible, inline]

abbrev Composition.length {n : ℕ} (c : Composition n) : ℕ

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

theorem Composition.blocks_length {n : ℕ} (c : Composition n) : c.blocks.length = c.length

def Composition.blocksFun {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.

@[simp]

theorem Composition.ofFn_blocksFun {n : ℕ} (c : Composition n) : List.ofFn c.blocksFun = c.blocks

@[simp]

theorem Composition.sum_blocksFun {n : ℕ} (c : Composition n) : ∑ i : Fin c.length, c.blocksFun i = n

@[simp]

theorem Composition.blocksFun_mem_blocks {n : ℕ} (c : Composition n) (i : Fin c.length) : c.blocksFun i ∈ c.blocks

theorem Composition.one_le_blocks {n : ℕ} (c : Composition n) {i : ℕ} (h : i ∈ c.blocks) : 1 ≤ i

theorem Composition.blocks_le {n : ℕ} (c : Composition n) {i : ℕ} (h : i ∈ c.blocks) : i ≤ n

@[simp]

theorem Composition.one_le_blocks' {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length) : 1 ≤ c.blocks[i]

@[simp]

theorem Composition.blocks_pos' {n : ℕ} (c : Composition n) (i : ℕ) (h : i < c.length) : 0 < c.blocks[i]

@[simp]

theorem Composition.one_le_blocksFun {n : ℕ} (c : Composition n) (i : Fin c.length) : 1 ≤ c.blocksFun i

@[simp]

theorem Composition.blocksFun_le {n : ℕ} (c : Composition n) (i : Fin c.length) : c.blocksFun i ≤ n

@[simp]

theorem Composition.length_le {n : ℕ} (c : Composition n) : c.length ≤ n

@[simp]

theorem Composition.blocks_eq_nil {n : ℕ} (c : Composition n) : c.blocks = [] ↔ n = 0

theorem Composition.length_eq_zero {n : ℕ} (c : Composition n) : c.length = 0 ↔ n = 0

@[simp]

theorem Composition.length_pos_iff {n : ℕ} (c : Composition n) : 0 < c.length ↔ 0 < n

theorem Composition.length_pos_of_pos {n : ℕ} (c : Composition n) : 0 < n → 0 < c.length

Alias of the reverse direction of Composition.length_pos_iff.

def Composition.sizeUpTo {n : ℕ} (c : Composition n) (i : ℕ) : ℕ

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

@[simp]

theorem Composition.sizeUpTo_zero {n : ℕ} (c : Composition n) : c.sizeUpTo 0 = 0

theorem Composition.sizeUpTo_ofLength_le {n : ℕ} (c : Composition n) (i : ℕ) (h : c.length ≤ i) : c.sizeUpTo i = n

@[simp]

theorem Composition.sizeUpTo_length {n : ℕ} (c : Composition n) : c.sizeUpTo c.length = n

theorem Composition.sizeUpTo_le {n : ℕ} (c : Composition n) (i : ℕ) : c.sizeUpTo i ≤ n

theorem Composition.sizeUpTo_succ {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length) : c.sizeUpTo (i + 1) = c.sizeUpTo i + c.blocks[i]

theorem Composition.sizeUpTo_succ' {n : ℕ} (c : Composition n) (i : Fin c.length) : c.sizeUpTo (↑i + 1) = c.sizeUpTo ↑i + c.blocksFun i

theorem Composition.sizeUpTo_strict_mono {n : ℕ} (c : Composition n) {i : ℕ} (h : i < c.length) : c.sizeUpTo i < c.sizeUpTo (i + 1)

theorem Composition.monotone_sizeUpTo {n : ℕ} (c : Composition n) : Monotone c.sizeUpTo

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 CompositionAsSet n.

@[simp]

theorem Composition.boundary_zero {n : ℕ} (c : Composition n) : c.boundary 0 = 0

@[simp]

theorem Composition.boundary_last {n : ℕ} (c : Composition n) : c.boundary (Fin.last c.length) = Fin.last n

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 CompositionAsSet n.

theorem Composition.card_boundaries_eq_succ_length {n : ℕ} (c : Composition n) : c.boundaries.card = c.length + 1

def Composition.toCompositionAsSet {n : ℕ} (c : Composition n) : CompositionAsSet n

To c : Composition n, one can associate a CompositionAsSet n by registering the leftmost point of each block, and adding a virtual point at the right of the last block.

theorem Composition.orderEmbOfFin_boundaries {n : ℕ} (c : Composition n) : c.boundaries.orderEmbOfFin ⋯ = c.boundary

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

def Composition.embedding {n : ℕ} (c : Composition n) (i : Fin c.length) : Fin (c.blocksFun i) ↪o Fin n

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

@[simp]

theorem Composition.coe_embedding {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)) : ↑((c.embedding i) j) = c.sizeUpTo ↑i + ↑j

theorem Composition.index_exists {n : ℕ} (c : Composition n) {j : ℕ} (h : j < n) : ∃ (i : ℕ), j < c.sizeUpTo (i + 1) ∧ i < c.length

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

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.

theorem Composition.lt_sizeUpTo_index_succ {n : ℕ} (c : Composition n) (j : Fin n) : ↑j < c.sizeUpTo ↑(c.index j).succ

theorem Composition.sizeUpTo_index_le {n : ℕ} (c : Composition n) (j : Fin n) : c.sizeUpTo ↑(c.index j) ≤ ↑j

def Composition.invEmbedding {n : ℕ} (c : Composition n) (j : Fin n) : Fin (c.blocksFun (c.index j))

Mapping an element j of Fin n to the element in the block containing it, identified with Fin (c.blocksFun (c.index j)) through the canonical increasing bijection.

@[simp]

theorem Composition.coe_invEmbedding {n : ℕ} (c : Composition n) (j : Fin n) : ↑(c.invEmbedding j) = ↑j - c.sizeUpTo ↑(c.index j)

@[simp]

theorem Composition.embedding_comp_inv {n : ℕ} (c : Composition n) (j : Fin n) : (c.embedding (c.index j)) (c.invEmbedding j) = j

theorem Composition.mem_range_embedding_iff {n : ℕ} (c : Composition n) {j : Fin n} {i : Fin c.length} : j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

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.

theorem Composition.mem_range_embedding {n : ℕ} (c : Composition n) (j : Fin n) : j ∈ Set.range ⇑(c.embedding (c.index j))

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

@[simp]

theorem Composition.index_embedding {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)) : c.index ((c.embedding i) j) = i

theorem Composition.invEmbedding_comp {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)) : ↑(c.invEmbedding ((c.embedding i) j)) = ↑j

def Composition.blocksFinEquiv {n : ℕ} (c : Composition n) : (i : Fin c.length) × Fin (c.blocksFun i) ≃ Fin n

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

theorem Composition.blocksFun_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₁.blocksFun i₁ = c₂.blocksFun i₂

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

def Composition.ones (n : ℕ) : Composition n

The composition made of blocks all of size 1.

@[implicit_reducible]

instance Composition.instInhabited {n : ℕ} : Inhabited (Composition n)

@[simp]

theorem Composition.ones_length (n : ℕ) : (ones n).length = n

@[simp]

theorem Composition.ones_blocks (n : ℕ) : (ones n).blocks = List.replicate n 1

@[simp]

theorem Composition.ones_blocksFun (n : ℕ) (i : Fin (ones n).length) : (ones n).blocksFun i = 1

@[simp]

theorem Composition.ones_sizeUpTo (n i : ℕ) : (ones n).sizeUpTo i = min i n

@[simp]

theorem Composition.ones_embedding {n : ℕ} (i : Fin (ones n).length) (h : 0 < (ones n).blocksFun i) : ((ones n).embedding i) ⟨0, h⟩ = ⟨↑i, ⋯⟩

theorem Composition.eq_ones_iff {n : ℕ} {c : Composition n} : c = ones n ↔ ∀ i ∈ c.blocks, i = 1

theorem Composition.ne_ones_iff {n : ℕ} {c : Composition n} : c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i

theorem Composition.eq_ones_iff_length {n : ℕ} {c : Composition n} : c = ones n ↔ c.length = n

theorem Composition.eq_ones_iff_le_length {n : ℕ} {c : Composition n} : c = ones n ↔ n ≤ c.length

The composition Composition.single

def Composition.single (n : ℕ) (h : 0 < n) : Composition n

The composition made of a single block of size n.

@[simp]

theorem Composition.single_length {n : ℕ} (h : 0 < n) : (single n h).length = 1

@[simp]

theorem Composition.single_blocks {n : ℕ} (h : 0 < n) : (single n h).blocks = [n]

@[simp]

theorem Composition.single_blocksFun {n : ℕ} (h : 0 < n) (i : Fin (single n h).length) : (single n h).blocksFun i = n

@[simp]

theorem Composition.single_embedding {n : ℕ} (h : 0 < n) (i : Fin n) : ((single n h).embedding 0) i = i

theorem Composition.eq_single_iff_length {n : ℕ} (h : 0 < n) {c : Composition n} : c = single n h ↔ c.length = 1

theorem Composition.ne_single_iff {n : ℕ} (hn : 0 < n) {c : Composition n} : c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n

def Composition.cast {n m : ℕ} (c : Composition m) (hmn : m = n) : Composition n

Change n in (c : Composition n) to a propositionally equal value.

@[simp]

theorem Composition.cast_blocks {n m : ℕ} (c : Composition m) (hmn : m = n) : (c.cast hmn).blocks = c.blocks

@[simp]

theorem Composition.cast_rfl {n : ℕ} (c : Composition n) : c.cast ⋯ = c

theorem Composition.cast_heq {n m : ℕ} (c : Composition m) (hmn : m = n) : c.cast hmn ≍ c

theorem Composition.cast_eq_cast {n m : ℕ} (c : Composition m) (hmn : m = n) : c.cast hmn = cast ⋯ c

def Composition.append {n m : ℕ} (c₁ : Composition m) (c₂ : Composition n) : Composition (m + n)

Append two compositions to get a composition of the sum of numbers.

@[simp]

theorem Composition.append_blocks {n m : ℕ} (c₁ : Composition m) (c₂ : Composition n) : (c₁.append c₂).blocks = c₁.blocks ++ c₂.blocks

def Composition.reverse {n : ℕ} (c : Composition n) : Composition n

Reverse the order of blocks in a composition.

@[simp]

theorem Composition.reverse_blocks {n : ℕ} (c : Composition n) : c.reverse.blocks = c.blocks.reverse

@[simp]

theorem Composition.reverse_reverse {n : ℕ} (c : Composition n) : c.reverse.reverse = c

theorem Composition.reverse_involutive {n : ℕ} : Function.Involutive reverse

theorem Composition.reverse_bijective {n : ℕ} : Function.Bijective reverse

theorem Composition.reverse_injective {n : ℕ} : Function.Injective reverse

theorem Composition.reverse_surjective {n : ℕ} : Function.Surjective reverse

@[simp]

theorem Composition.reverse_inj {n : ℕ} {c₁ c₂ : Composition n} : c₁.reverse = c₂.reverse ↔ c₁ = c₂

@[simp]

theorem Composition.reverse_ones {n : ℕ} : (ones n).reverse = ones n

@[simp]

theorem Composition.reverse_single {n : ℕ} (hn : 0 < n) : (single n hn).reverse = single n hn

@[simp]

theorem Composition.reverse_eq_ones {n : ℕ} {c : Composition n} : c.reverse = ones n ↔ c = ones n

@[simp]

theorem Composition.reverse_eq_single {n : ℕ} {hn : 0 < n} {c : Composition n} : c.reverse = single n hn ↔ c = single n hn

theorem Composition.reverse_append {n m : ℕ} (c₁ : Composition m) (c₂ : Composition n) : (c₁.append c₂).reverse = (c₂.reverse.append c₁.reverse).cast ⋯

@[irreducible]

def Composition.recOnSingleAppend {motive : (n : ℕ) → Composition n → Sort u_1} {n : ℕ} (c : Composition n) (zero : motive 0 (ones 0)) (single_append : (k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((single (k + 1) ⋯).append c)) : motive n c

Induction (recursion) principle on c : Composition _ that corresponds to the usual induction on the list of blocks of c.

def Composition.recOnAppendSingle {motive : (n : ℕ) → Composition n → Sort u_1} {n : ℕ} (c : Composition n) (zero : motive 0 (ones 0)) (append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))) : motive n c

Induction (recursion) principle on c : Composition _ that corresponds to the reverse induction on the list of blocks of c.

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.blocksFun 0, ..., c.blocksFun (c.length-1). This is inverse to the join operation.

def List.splitWrtCompositionAux {α : Type u_1} : List α → List ℕ → List (List α)

Auxiliary for List.splitWrtComposition.

def List.splitWrtComposition {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.

theorem List.splitWrtCompositionAux_cons {α : Type u_1} (l : List α) (n : ℕ) (ns : List ℕ) : l.splitWrtCompositionAux (n :: ns) = take n l :: (drop n l).splitWrtCompositionAux ns

theorem List.length_splitWrtCompositionAux {α : Type u_1} (l : List α) (ns : List ℕ) : (l.splitWrtCompositionAux ns).length = ns.length

@[simp]

theorem List.length_splitWrtComposition {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) : (l.splitWrtComposition c).length = c.length

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

theorem List.map_length_splitWrtCompositionAux {α : Type u_1} {ns : List ℕ} {l : List α} : ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns

theorem List.map_length_splitWrtComposition {α : Type u_1} (l : List α) (c : Composition l.length) : map length (l.splitWrtComposition 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.

theorem List.length_pos_of_mem_splitWrtComposition {α : Type u_1} {l l' : List α} {c : Composition l.length} (h : l' ∈ l.splitWrtComposition c) : 0 < l'.length

theorem List.sum_take_map_length_splitWrtComposition {α : Type u_1} (l : List α) (c : Composition l.length) (i : ℕ) : (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

theorem List.getElem_splitWrtCompositionAux {α : Type u_1} (l : List α) (ns : List ℕ) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length) : (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)

theorem List.getElem_splitWrtComposition' {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) {i : ℕ} (hi : i < (l.splitWrtComposition c).length) : (l.splitWrtComposition c)[i] = drop (c.sizeUpTo i) (take (c.sizeUpTo (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.sizeUpTo i and c.sizeUpTo (i+1), i.e., the indices in the i-th block of the composition.

theorem List.getElem_splitWrtComposition {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) (i : ℕ) (h : i < (l.splitWrtComposition c).length) : (l.splitWrtComposition c)[i] = drop (c.sizeUpTo i) (take (c.sizeUpTo (i + 1)) l)

theorem List.flatten_splitWrtCompositionAux {α : Type u_1} {ns : List ℕ} {l : List α} : ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l

@[simp]

theorem List.flatten_splitWrtComposition {α : Type u_1} (l : List α) (c : Composition l.length) : (l.splitWrtComposition c).flatten = l

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

@[simp]

theorem List.splitWrtComposition_flatten {α : Type u_1} (L : List (List α)) (c : Composition L.flatten.length) (h : map length L = c.blocks) : L.flatten.splitWrtComposition c = L

If one joins a list of lists and then splits the flattening 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.

def compositionAsSetEquiv (n : ℕ) : CompositionAsSet 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.

@[implicit_reducible]

instance compositionAsSetFintype (n : ℕ) : Fintype (CompositionAsSet n)

theorem compositionAsSet_card (n : ℕ) : Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

theorem CompositionAsSet.boundaries_nonempty {n : ℕ} (c : CompositionAsSet n) : c.boundaries.Nonempty

theorem CompositionAsSet.card_boundaries_pos {n : ℕ} (c : CompositionAsSet n) : 0 < c.boundaries.card

def CompositionAsSet.length {n : ℕ} (c : CompositionAsSet n) : ℕ

Number of blocks in a CompositionAsSet.

theorem CompositionAsSet.card_boundaries_eq_succ_length {n : ℕ} (c : CompositionAsSet n) : c.boundaries.card = c.length + 1

theorem CompositionAsSet.length_lt_card_boundaries {n : ℕ} (c : CompositionAsSet n) : c.length < c.boundaries.card

theorem CompositionAsSet.lt_length {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length) : ↑i + 1 < c.boundaries.card

theorem CompositionAsSet.lt_length' {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length) : ↑i < c.boundaries.card

def CompositionAsSet.boundary {n : ℕ} (c : CompositionAsSet n) : Fin c.boundaries.card ↪o Fin (n + 1)

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

@[simp]

theorem CompositionAsSet.boundary_zero {n : ℕ} (c : CompositionAsSet n) : c.boundary ⟨0, ⋯⟩ = 0

@[simp]

theorem CompositionAsSet.boundary_length {n : ℕ} (c : CompositionAsSet n) : c.boundary ⟨c.length, ⋯⟩ = Fin.last n

def CompositionAsSet.blocksFun {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length) : ℕ

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

theorem CompositionAsSet.blocksFun_pos {n : ℕ} (c : CompositionAsSet n) (i : Fin c.length) : 0 < c.blocksFun i

def CompositionAsSet.blocks {n : ℕ} (c : CompositionAsSet n) : List ℕ

List of the sizes of the blocks in a CompositionAsSet.

@[simp]

theorem CompositionAsSet.blocks_length {n : ℕ} (c : CompositionAsSet n) : c.blocks.length = c.length

theorem CompositionAsSet.blocks_partial_sum {n : ℕ} (c : CompositionAsSet n) {i : ℕ} (h : i < c.boundaries.card) : (List.take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)

theorem CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq {n : ℕ} (c : CompositionAsSet n) {j : Fin (n + 1)} : j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (List.take i c.blocks).sum = ↑j

theorem CompositionAsSet.blocks_sum {n : ℕ} (c : CompositionAsSet n) : c.blocks.sum = n

def CompositionAsSet.toComposition {n : ℕ} (c : CompositionAsSet n) : Composition n

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

Equivalence between compositions and compositions as sets

In this section, we explain how to go back and forth between a Composition and a CompositionAsSet, by showing that their blocks and length and boundaries correspond to each other, and construct an equivalence between them called compositionEquiv.

@[simp]

theorem Composition.toCompositionAsSet_length {n : ℕ} (c : Composition n) : c.toCompositionAsSet.length = c.length

@[simp]

theorem CompositionAsSet.toComposition_length {n : ℕ} (c : CompositionAsSet n) : c.toComposition.length = c.length

@[simp]

theorem Composition.toCompositionAsSet_blocks {n : ℕ} (c : Composition n) : c.toCompositionAsSet.blocks = c.blocks

@[simp]

theorem CompositionAsSet.toComposition_blocks {n : ℕ} (c : CompositionAsSet n) : c.toComposition.blocks = c.blocks

@[simp]

theorem CompositionAsSet.toComposition_boundaries {n : ℕ} (c : CompositionAsSet n) : c.toComposition.boundaries = c.boundaries

@[simp]

theorem Composition.toCompositionAsSet_boundaries {n : ℕ} (c : Composition n) : c.toCompositionAsSet.boundaries = c.boundaries

def compositionEquiv (n : ℕ) : Composition n ≃ CompositionAsSet n

Equivalence between Composition n and CompositionAsSet n.

@[implicit_reducible]

instance compositionFintype (n : ℕ) : Fintype (Composition n)

theorem composition_card (n : ℕ) : Fintype.card (Composition n) = 2 ^ (n - 1)