Bell permutations and weak excedances

TheoremWeak excedances of Bell permutations of the second kind#✓fully proved

Let \(n \ge 1\) and \(k\) be natural numbers, and write \([n] = \{0, \dots, n-1\}\). A function \(f : [n] \to [n]\) is a restricted growth function if for every \(i\), every \(j < f(i)\) equals \(f(i_0)\) for some \(i_0 < i\). Its Bell permutation is the product of transpositions \((0\ f(0))(1\ f(1)) \cdots (n-1\ f(n-1))\), composed so that the rightmost factor acts first, where \((i\ i)\) denotes the identity. A weak excedance of a permutation \(\sigma\) of \([n]\) is an index \(i\) with \(i \le \sigma(i)\). Then the number of permutations of \([n]\) that are the Bell permutation of some restricted growth function and have exactly \(k\) weak excedances is the Stirling number of the second kind \(S(n, k)\).

theorem bell_perm_second_kind_weakExcedance_eq_stirlingSecond
    (n k : ℕ) (hn : 0 < n) :
    let IsRGF : (Fin n → Fin n) → Prop :=
      fun f => ∀ i : Fin n, ∀ j : Fin n, j.val < (f i).val →
        ∃ i₀ : Fin n, i₀.val < i.val ∧ f i₀ = j;
    let bellPerm : (Fin n → Fin n) → Equiv.Perm (Fin n) :=
      fun f => ((List.finRange n).map fun i => Equiv.swap i (f i)).prod;
    let numWeak : Equiv.Perm (Fin n) → ℕ :=
      fun σ => Fintype.card {i : Fin n // i ≤ σ i};
    Nat.card {σ : Equiv.Perm (Fin n) //
      ∃ f : Fin n → Fin n, IsRGF f ∧ bellPerm f = σ ∧ numWeak σ = k} =
      Nat.stirlingSecond n k

Sources

• Fufa Beyene, Jörgen Backelin, Roberto Mantaci, and Samuel A. Fufa, "Set Partitions and Other Bell Number Enumerated Objects," Journal of Integer Sequences 26 (2023), Article 23.1.8, Corollary, item 1, lines 283–290, https://cs.uwaterloo.ca/journals/JIS/VOL26/Beyene/beyene13.tex

TheoremBell numbers count permutations with increasing weak excedance letters#✓fully proved

A position \(i\) is a weak excedance of a permutation \(\sigma\) when \(i \le \sigma(i)\). For every \(n\), the number of permutations \(\sigma\) of \(\{0, 1, \dots, n-1\}\) such that \(\sigma(i) < \sigma(j)\) whenever \(i < j\) are both weak excedances of \(\sigma\) is the Bell number \(B_n\).

public theorem bell_count_perm_increasing_weakExcedance_letters (n : ℕ) :
    Fintype.card { σ : Equiv.Perm (Fin n) //
      ∀ i j : Fin n, i < j → i ≤ σ i → j ≤ σ j → σ i < σ j } = Nat.bell n

Sources

• Fufa Beyene, Jörgen Backelin, Roberto Mantaci, and Samuel A. Fufa, "Set Partitions and Other Bell Number Enumerated Objects," Journal of Integer Sequences 26 (2023), Article 23.1.8, Theorem, lines 434–436, https://cs.uwaterloo.ca/journals/JIS/VOL26/Beyene/beyene13.tex

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.