Graphical Stirling and Lah numbers

DefinitionTruncated-cycle successor#✓fully proved

Let \(\sigma\) be a permutation of a finite linearly ordered set \(V\) and let \(i, j \in V\). Then \(j\) is the truncated-cycle successor \(\sigma^{(i)}(i)\) of \(i\) when \(j\) is the first of the iterates \(\sigma(i), \sigma^2(i), \dots\) that is at most \(i\): there is an \(m > 0\) with \(\sigma^m(i) = j\) and \(j \le i\), and \(\sigma^{m'}(i) > i\) for every \(m'\) with \(0 < m' < m\).

def TruncatedSucc (σ : Equiv.Perm V) (i j : V) : Prop :=
  ∃ m : ℕ, 0 < m ∧ j ≤ i ∧ (σ ^ m) i = j ∧
    ∀ m' : ℕ, 0 < m' → m' < m → i < (σ ^ m') i
Used by 1
Used by\(k\)-cyclic partition

Definition\(k\)-cyclic partition#✓fully proved

Let \(V\) be a finite linearly ordered set, \(\sigma\) a permutation of \(V\), \(E\) a relation on \(V\) (the directed edges of a labeled graph) and \(k\) a natural number. Then \(\sigma\) is a \(k\)-cyclic partition for \(E\) when \(\sigma\) has exactly \(k\) cycles, fixed points counted as cycles of length one, and for all \(i, j \in V\), if \(j\) is the truncated-cycle successor of \(i\) under \(\sigma\) (the first of \(\sigma(i), \sigma^2(i), \dots\) that is at most \(i\)), then \(E(i, j)\) does not hold.

def IsKCyclicPartition (σ : Equiv.Perm V) (edge : V → V → Prop) (k : ℕ) : Prop :=
  σ.cycleType.card + (Fintype.card V - σ.support.card) = k ∧
    ∀ i j : V, TruncatedSucc σ i j → ¬ edge i j
Sources
Uses 1
Statement usesTruncated-cycle successor

StructureLinear partition of a graph#✓fully proved

Let \(G\) be a simple graph on a vertex type \(V\) and let \(k\) be a natural number. A \(k\)-linear partition of \(G\) is a set of exactly \(k\) blocks, each block a nonempty finite sequence of pairwise distinct vertices, such that every vertex of \(G\) lies in exactly one block and any two consecutive vertices of a block are nonadjacent in \(G\). The blocks themselves are unordered; only the vertices within a block are ordered.

structure LinearPartition {V : Type*} [DecidableEq V] (G : SimpleGraph V) (k : ℕ) where
  blocks : Finset (List V)
  card_eq : blocks.card = k
  nonempty : ∀ L ∈ blocks, L ≠ []
  nodup : ∀ L ∈ blocks, L.Nodup
  covers : ∀ v : V, ∃! L, L ∈ blocks ∧ v ∈ L
  consecutive : ∀ L ∈ blocks, List.IsChain (fun a b => ¬G.Adj a b) L
Sources
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.