Stirling permutations

DefinitionStirling permutations#✓fully proved

Let \(n\) be a natural number. A word \(w = w_1 w_2 \cdots w_{2n}\) of natural numbers is a Stirling permutation of order \(n\) if every letter lies in \(\{1, \dots, n\}\), each \(i \in \{1, \dots, n\}\) occurs exactly twice, and every letter strictly between the two occurrences of \(i\) is greater than \(i\).

def IsStirlingPermutation (n : ℕ) (w : Fin (2 * n) → ℕ) : Prop :=
  (∀ k, w k ∈ Finset.Icc 1 n) ∧
  (∀ v ∈ Finset.Icc 1 n,
    Finset.card (Finset.univ.filter (fun k => w k = v)) = 2) ∧
  ∀ i ∈ Finset.Icc 1 n, ∀ a b c : Fin (2 * n),
    a < b → b < c → w a = i → w c = i → i < w b

Used by 27

Used byExtremely lucky Stirling permutations are counted by the Catalan numbers · Counting extremely unlucky Stirling permutations · Stirling permutations with \(n\) nonzero displacements · Extremely lucky Stirling permutations are determined by their displacements · Extremely lucky Stirling permutations and Dyck words · Unlucky cars of an extremely lucky Stirling permutation · Admissible lucky sets · Number of cars with zero displacement · The first preference bounds the lucky cars · Basic properties of lucky cars · Characterization of extremely lucky Stirling permutations · Characterization of extremely unlucky Stirling permutations · Left-to-right minima of a Stirling permutation sit at odd positions · Parking before the second lucky car · When the penultimate car is lucky · Stirling permutations whose second lucky car is \(n\) · A second lucky car beyond \(n\) is odd · Preference of the second lucky car · Total displacement of a Stirling permutation is invariant under rearrangement · Total displacement of a Stirling permutation · The map \(\varphi\) is a bijection from type \(B\) set partitions onto flattened Stirling permutations · Number of flattened Stirling permutations · Counting flattened Stirling permutations by runs · Maximum number of runs of a flattened Stirling permutation · Flattened Stirling permutations and type \(B\) set partitions · The word of a type \(B\) set partition is a flattened Stirling permutation · The set of Stirling permutations

DefinitionThe set of Stirling permutations#✓fully proved

For a natural number \(n\), \(Q_n\) is the set of all Stirling permutations of order \(n\), viewed as words \(w_1 w_2 \cdots w_{2n}\) of natural numbers.

def StirlingPermSet (n : ℕ) : Set (Fin (2 * n) → ℕ) :=
  {w | IsStirlingPermutation n w}

Uses 1

Statement usesStirling permutations

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.