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 #

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 : 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)

theorem Composition.ext {n : } (x : Composition n) (y : Composition n) (blocks : x.blocks = y.blocks) :
x = y
theorem Composition.ext_iff {n : } (x : Composition n) (y : Composition n) :
x = y x.blocks = y.blocks
structure Composition (n : ) :
  • blocks : List

    List of positive integers summing to n

  • blocks_pos : ∀ {i : }, i s.blocks0 < i

    Proof of positivity for blocks

  • blocks_sum : List.sum s.blocks = n

    Proof that blocks sums to n

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

Instances For
    theorem CompositionAsSet.ext_iff {n : } (x : CompositionAsSet n) (y : CompositionAsSet n) :
    x = y x.boundaries = y.boundaries
    theorem CompositionAsSet.ext {n : } (x : CompositionAsSet n) (y : CompositionAsSet n) (boundaries : x.boundaries = y.boundaries) :
    x = y
    structure CompositionAsSet (n : ) :
    • boundaries : Finset (Fin (Nat.succ n))

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

    • zero_mem : 0 s.boundaries

      Proof that 0 is a member of boundaries

    • getLast_mem : Fin.last n s.boundaries

      Last element of the composition

    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.

    Instances For

      Compositions #

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

      @[reducible]

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

      Instances For

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

        Instances For
          theorem Composition.sum_blocksFun {n : } (c : Composition n) :
          (Finset.sum Finset.univ fun i => Composition.blocksFun c i) = n
          @[simp]
          theorem Composition.one_le_blocks {n : } (c : Composition n) {i : } (h : i c.blocks) :
          1 i
          @[simp]
          theorem Composition.one_le_blocks' {n : } (c : Composition n) {i : } (h : i < Composition.length c) :
          1 List.nthLe c.blocks i h
          @[simp]
          theorem Composition.blocks_pos' {n : } (c : Composition n) (i : ) (h : i < Composition.length c) :
          0 < List.nthLe c.blocks i h
          def Composition.sizeUpTo {n : } (c : Composition n) (i : ) :

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

          Instances For

            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.

            Instances For
              @[simp]
              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.

              Instances For

                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.

                Instances For

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

                  Instances For
                    @[simp]
                    theorem Composition.index_exists {n : } (c : Composition n) {j : } (h : j < n) :

                    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.

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

                    Instances For

                      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.

                      Instances For
                        theorem Composition.disjoint_range {n : } (c : Composition n) {i₁ : Fin (Composition.length c)} {i₂ : Fin (Composition.length c)} (h : i₁ i₂) :

                        The embeddings of different blocks of a composition are disjoint.

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

                        Instances For
                          theorem Composition.blocksFun_congr {n₁ : } {n₂ : } (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin (Composition.length c₁)) (i₂ : Fin (Composition.length c₂)) (hn : n₁ = n₂) (hc : c₁.blocks = c₂.blocks) (hi : i₁ = i₂) :
                          theorem Composition.sigma_eq_iff_blocks_eq {c : (n : ) × Composition n} {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 #

                          The composition made of blocks all of size 1.

                          Instances For
                            @[simp]
                            @[simp]
                            theorem Composition.ones_embedding {n : } (i : Fin (Composition.length (Composition.ones n))) (h : 0 < Composition.blocksFun (Composition.ones n) i) :
                            ↑(Composition.embedding (Composition.ones n) i) { val := 0, isLt := h } = { val := i, isLt := (_ : i < n) }
                            theorem Composition.eq_ones_iff {n : } {c : Composition n} :
                            c = Composition.ones n ∀ (i : ), i c.blocksi = 1
                            theorem Composition.ne_ones_iff {n : } {c : Composition n} :
                            c Composition.ones n i, i c.blocks 1 < i

                            The composition Composition.single #

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

                            The composition made of a single block of size n.

                            Instances For
                              @[simp]
                              theorem Composition.single_blocks {n : } (h : 0 < n) :
                              (Composition.single n h).blocks = [n]
                              @[simp]
                              theorem Composition.single_embedding {n : } (h : 0 < n) (i : Fin 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.

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

                              Auxiliary for List.splitWrtComposition.

                              Equations
                              Instances For
                                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.

                                Instances For
                                  @[simp]

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

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

                                  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.

                                  @[simp]

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

                                  @[simp]
                                  theorem List.splitWrtComposition_join {α : Type u_1} (L : List (List α)) (c : Composition (List.length (List.join L))) (h : List.map List.length L = c.blocks) :

                                  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.

                                  Instances For

                                    Number of blocks in a CompositionAsSet.

                                    Instances For
                                      theorem CompositionAsSet.lt_length {n : } (c : CompositionAsSet n) (i : Fin (CompositionAsSet.length c)) :
                                      i + 1 < Finset.card c.boundaries
                                      def CompositionAsSet.boundary {n : } (c : CompositionAsSet n) :
                                      Fin (Finset.card c.boundaries) ↪o Fin (n + 1)

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

                                      Instances For
                                        @[simp]
                                        theorem CompositionAsSet.boundary_zero {n : } (c : CompositionAsSet n) :
                                        ↑(CompositionAsSet.boundary c) { val := 0, isLt := (_ : 0 < Finset.card c.boundaries) } = 0

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

                                        Instances For

                                          List of the sizes of the blocks in a CompositionAsSet.

                                          Instances For
                                            theorem CompositionAsSet.blocks_partial_sum {n : } (c : CompositionAsSet n) {i : } (h : i < Finset.card c.boundaries) :
                                            List.sum (List.take i (CompositionAsSet.blocks c)) = ↑(↑(CompositionAsSet.boundary c) { val := i, isLt := h })

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

                                            Instances For

                                              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.

                                              Equivalence between Composition n and CompositionAsSet n.

                                              Instances For