Documentation

Mathlib.Combinatorics.Enumerative.Partition

Partitions #

A partition of a natural number n is a way of writing n as a sum of positive integers, where the order does not matter: two sums that differ only in the order of their summands are considered the same partition. This notion is closely related to that of a composition of n, but in a composition of n the order does matter. A summand of the partition is called a part.

Main functions #

Implementation details #

The main motivation for this structure and its API is to show Euler's partition theorem, and related results.

The representation of a partition as a multiset is very handy as multisets are very flexible and already have a well-developed API.

TODO #

Link this to Young diagrams.

Tags #

Partition

References #

https://en.wikipedia.org/wiki/Partition_(number_theory)

theorem Nat.Partition.ext {n : } (x : n.Partition) (y : n.Partition) (parts : x.parts = y.parts) :
x = y
theorem Nat.Partition.ext_iff {n : } (x : n.Partition) (y : n.Partition) :
x = y x.parts = y.parts
structure Nat.Partition (n : ) :

A partition of n is a multiset of positive integers summing to n.

  • parts : Multiset

    positive integers summing to n

  • parts_pos : ∀ {i : }, i self.parts0 < i

    proof that the parts are positive

  • parts_sum : self.parts.sum = n

    proof that the parts sum to n

Instances For
    theorem Nat.Partition.parts_pos {n : } (self : n.Partition) {i : } :
    i self.parts0 < i

    proof that the parts are positive

    theorem Nat.Partition.parts_sum {n : } (self : n.Partition) :
    self.parts.sum = n

    proof that the parts sum to n

    Equations
    @[simp]
    theorem Nat.Partition.ofComposition_parts (n : ) (c : Composition n) :
    (Nat.Partition.ofComposition n c).parts = c.blocks
    def Nat.Partition.ofComposition (n : ) (c : Composition n) :
    n.Partition

    A composition induces a partition (just convert the list to a multiset).

    Equations
    Instances For
      @[simp]
      theorem Nat.Partition.ofSums_parts (n : ) (l : Multiset ) (hl : l.sum = n) :
      (Nat.Partition.ofSums n l hl).parts = Multiset.filter (fun (x : ) => x 0) l
      def Nat.Partition.ofSums (n : ) (l : Multiset ) (hl : l.sum = n) :
      n.Partition

      Given a multiset which sums to n, construct a partition of n with the same multiset, but without the zeros.

      Equations
      Instances For
        def Nat.Partition.ofMultiset (l : Multiset ) :
        l.sum.Partition

        A Multiset induces a partition on its sum.

        Equations
        Instances For
          def Nat.Partition.indiscrete (n : ) :
          n.Partition

          The partition of exactly one part.

          Equations
          Instances For
            instance Nat.Partition.instInhabited {n : } :
            Inhabited n.Partition
            Equations
            @[simp]
            theorem Nat.Partition.indiscrete_parts {n : } (hn : n 0) :
            @[simp]
            @[simp]
            theorem Nat.Partition.count_ofSums_of_ne_zero {n : } {l : Multiset } (hl : l.sum = n) {i : } (hi : i 0) :

            The number of times a positive integer i appears in the partition ofSums n l hl is the same as the number of times it appears in the multiset l. (For i = 0, Partition.non_zero combined with Multiset.count_eq_zero_of_not_mem gives that this is 0 instead.)

            theorem Nat.Partition.count_ofSums_zero {n : } {l : Multiset } (hl : l.sum = n) :
            instance Nat.Partition.instFintype (n : ) :
            Fintype n.Partition

            Show there are finitely many partitions by considering the surjection from compositions to partitions.

            Equations
            def Nat.Partition.odds (n : ) :
            Finset n.Partition

            The finset of those partitions in which every part is odd.

            Equations
            Instances For
              def Nat.Partition.distincts (n : ) :
              Finset n.Partition

              The finset of those partitions in which each part is used at most once.

              Equations
              Instances For
                def Nat.Partition.oddDistincts (n : ) :
                Finset n.Partition

                The finset of those partitions in which every part is odd and used at most once.

                Equations
                Instances For