Set partitions

Partitions of a finite set into blocks: finite partition API, ordered and cyclic set partitions, restricted-growth words, peaks and rises, noncrossing partitions, merging-free and marriageable-singles partitions, genus of a partition, and linear chord diagrams and hypermonopoles.

DefinitionBasic set partition#✓fully proved

A partition \(P\) of \(\{1, \dots, n\}\) is basic when its blocks can be listed without repetition as \(B_1, \dots, B_k\) with \(|B_1| \ge |B_2| \ge \dots \ge |B_k|\) so that \(B_1 \cup \dots \cup B_i = \{1, \dots, |B_1| + \dots + |B_i|\}\) for every \(i\) with \(1 \le i \le k\).

public def IsBasicSetPartition (n : ℕ) (P : Finpartition (Finset.Icc 1 n)) : Prop :=
  ∃ blocks : List (Finset ℕ),
    blocks.Nodup ∧
    blocks.toFinset = P.parts ∧
    (∀ B ∈ blocks, 0 < B.card) ∧
    List.Pairwise (fun earlier later => later.card ≤ earlier.card) blocks ∧
    ∀ i : ℕ, 1 ≤ i → i ≤ blocks.length →
      (blocks.take i).foldl (· ∪ ·) (∅ : Finset ℕ) =
        Finset.Icc 1 (((blocks.take i).map Finset.card).sum)

StructureCallan sequences#✓fully proved

Let \(k\) and \(n\) be natural numbers. Form the blue base set \(\{1, \dots, k\} \cup \{\star_B\}\) and the red base set \(\{1, \dots, n\} \cup \{\star_R\}\), where the blue star \(\star_B\) and the red star \(\star_R\) are new elements. An (unbarred) Callan sequence of size \(k \times n\) consists of a natural number \(m \le n\) together with a sequence of \(m + 1\) pairs \((B_0, R_0), \dots, (B_m, R_m)\) such that the blue blocks \(B_0, \dots, B_m\) are nonempty subsets of the blue base set and every element of the blue base set lies in exactly one of them, the red blocks \(R_0, \dots, R_m\) are nonempty subsets of the red base set and every element of the red base set lies in exactly one of them, and the last pair contains both stars: \(\star_B \in B_m\) and \(\star_R \in R_m\).

MetaMathlibExt.CallanSequence · 21 lines 
structure CallanSequence (k n : ℕ) where
  /-- Number of ordinary Callan pairs. -/
  m : ℕ
  /-- Pair-count bound from the source definition. -/
  m_le_n : m ≤ n
  /-- Blue blocks indexed by `Fin (m + 1)`. -/
  blue : Fin (m + 1) → Finset (Option (Fin k))
  /-- Red blocks indexed by `Fin (m + 1)`. -/
  red : Fin (m + 1) → Finset (Option (Fin n))
  /-- Every blue block is nonempty. -/
  blue_nonempty : ∀ i, (blue i).Nonempty
  /-- Every red block is nonempty. -/
  red_nonempty : ∀ i, (red i).Nonempty
  /-- The blue blocks partition the blue base set. -/
  blue_covers : ∀ x, ∃! i, x ∈ blue i
  /-- The red blocks partition the red base set. -/
  red_covers : ∀ x, ∃! i, x ∈ red i
  /-- The blue star lies in the extra blue block. -/
  blue_mem_star : (none : Option (Fin k)) ∈ blue (Fin.last m)
  /-- The red star lies in the extra red block. -/
  red_mem_star : (none : Option (Fin n)) ∈ red (Fin.last m)

TheoremGenerating function for set partitions by rises#✓fully proved

Fix \(k \ge 1\). For \(n, r \ge 0\) let \(a_{n,r}\) be the number of words \(\pi = \pi_1 \cdots \pi_n\) on the alphabet \(\{0, \dots, k-1\}\) that use every letter, satisfy the restricted growth condition that each \(\pi_i\) is at most the number of distinct letters among \(\pi_1, \dots, \pi_{i-1}\), and have exactly \(r\) rises (the source's \(2\)-rises), that is, positions \(i < n\) with \(\pi_i < \pi_{i+1}\). These words encode the partitions of \([n]\) into \(k\) blocks. Then, in the ring \(\mathbb{Q}[[x, y]]\) of formal power series,

\[\sum_{n, r \ge 0} a_{n,r}\, x^n y^r = \frac{x^k y^{k-1} (1-y)^k}{\prod_{j=1}^{k} \bigl((1 - x + xy)^j - y\bigr)}.\]
MetaMathlibExt.setPartition_twoRise_ordinaryGeneratingFunction · 16 lines 
theorem setPartition_twoRise_ordinaryGeneratingFunction
    (k : ℕ) (hk : 1 ≤ k) :
    let x : MvPowerSeries (Fin 2) ℚ := MvPowerSeries.X 0
    let y : MvPowerSeries (Fin 2) ℚ := MvPowerSeries.X 1
    ((fun d : Fin 2 →₀ ℕ =>
        (Fintype.card {π : Fin (d 0) → Fin k //
          Function.Surjective π ∧
            (∀ i : Fin (d 0),
              (π i).val ≤
                ((Finset.univ.filter fun j : Fin (d 0) => j < i).image π).card) ∧
            (Finset.univ.filter fun p : Fin (d 0) × Fin (d 0) =>
              p.2.val = p.1.val + 1 ∧ π p.1 < π p.2).card = d 1} : ℚ)) :
      MvPowerSeries (Fin 2) ℚ) =
      x ^ k * y ^ (k - 1) * ((1 : MvPowerSeries (Fin 2) ℚ) - y) ^ k *
        (∏ j ∈ Finset.Icc 1 k,
          (((1 : MvPowerSeries (Fin 2) ℚ) - x + x * y) ^ j - y))⁻¹
Sources

DefinitionMerging-free partitions#✓fully proved

Let \(n\) be a natural number. A finite sequence \((B_1, \dots, B_m)\) of subsets of \(\{0, 1, \dots, n-1\}\) is a merging-free partition when the sets \(B_i\) are nonempty, pairwise disjoint and cover \(\{0, 1, \dots, n-1\}\); their minima increase strictly, \(\min B_1 < \min B_2 < \dots < \min B_m\); and \(\max B_i > \min B_{i+1}\) for every \(i < m\).

def IsMergingFreePartition (n : ℕ) (P : List (Finset (Fin n))) : Prop :=
  (∀ B ∈ P, B.Nonempty) ∧
    P.Pairwise (fun B C => B ∩ C = ∅) ∧
    (∀ x, ∃ B ∈ P, x ∈ B) ∧
    P.Pairwise (fun B C =>
      ∃ mB ∈ B, ∃ mC ∈ C,
        (∀ b ∈ B, mB ≤ b) ∧ (∀ c ∈ C, mC ≤ c) ∧ mB < mC) ∧
    P.IsChain (fun B C =>
      ∃ mC ∈ C, ∃ mB ∈ B,
        (∀ c ∈ C, mC ≤ c) ∧ (∀ b ∈ B, b ≤ mB) ∧ mC < mB)

DefinitionOrdered set partitions of a finite set#✓fully proved

For a finite set \(V\), a list \((B_1, \dots, B_k)\) of finite sets is an ordered set partition (set composition) of \(V\) when every block \(B_i\) is nonempty and contained in \(V\), the blocks are pairwise disjoint, and \(B_1 \cup \dots \cup B_k = V\).

Equivalently, an ordered set partition of \(V\) is a structure of the composite species of lists of nonempty sets on \(V\).

def IsOrderedSetPartition {α : Type*} [DecidableEq α] (V : Finset α)
    (blocks : List (Finset α)) : Prop :=
  (∀ B ∈ blocks, B.Nonempty) ∧
    (∀ B ∈ blocks, B ⊆ V) ∧
    blocks.Pairwise (fun A B => Disjoint A B) ∧
    V = blocks.foldl (· ∪ ·) ∅

TheoremRestricted-growth word generating function#✓fully proved

Fix \(k \ge 0\). A word \(u_1 u_2 \cdots u_n\) in the letters \(1, \dots, k\) is a restricted-growth word if for every \(i\), either \(u_i = 1\) or \(u_i \le u_j + 1\) for some \(j < i\) (so a nonempty such word begins with \(1\)). For \(d = (d_1, \dots, d_k) \in \mathbb{N}^k\), let \(r(d)\) be the number of restricted-growth words in which each letter \(a\) occurs exactly \(d_a + 1\) times. Then, in the ring of formal power series in \(x_1, \dots, x_k\) over \(\mathbb{Q}\),

\[\sum_{d} r(d)\, x_1^{d_1} \cdots x_k^{d_k} = \prod_{j=1}^{k} (1 - x_1 - \cdots - x_j)^{-1}.\]

Proof: Decompose restricted-growth words by their first letter to obtain a coefficient recurrence, lift it to multivariate power series, and iterate power-series inverse cancellation. The combinatorial route follows Ehrenborg, Hedmark, and Hettle, Theorem 1.

public theorem restricted_growth_word_monomial_generating_function
    (k : ℕ) :
    ((fun d : Fin k →₀ ℕ =>
      (Nat.card {
        u : Fin (k + d.sum fun _ m => m) → Fin k //
          (∀ i, (u i : ℕ) = 0 ∨
            ∃ j, j < i ∧ (u i : ℕ) ≤ (u j : ℕ) + 1) ∧
          ∀ a, Nat.card {i : Fin (k + d.sum fun _ m => m) // u i = a} = d a + 1
      } : ℚ)) : MvPowerSeries (Fin k) ℚ) =
      (∏ j : Fin k,
        (1 - ∑ i ∈ Finset.Iic j, MvPowerSeries.X i)⁻¹ : MvPowerSeries (Fin k) ℚ)
Sources
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.