Order patterns of a random permutation

Fix an injective tuple q : Fin k ↪ α in a finite linear order. A permutation σ of α realizes on q the order pattern Tuple.sort (σ ∘ q), the reordering of Fin k that sorts σ ∘ q. Each of the k ! patterns is realized by the same number of permutations, so a uniformly random permutation realizes each one with probability 1 / k !.

Main statements

• Equiv.Perm.factorial_mul_card_sort_comp_eq: k ! * #{σ | sort (σ ∘ q) = ρ} = (card α)!.
• Equiv.Perm.factorial_mul_card_monotone_comp: k ! * #{σ | Monotone (σ ∘ q)} = (card α)!.

Implementation notes

Sorting a reordered injective tuple undoes the reordering, and ρ.viaEmbedding q turns precomposition of q by ρ into postcomposition, so right multiplication by it carries the permutations realizing ρ onto those realizing the identity pattern.

[UPSTREAM] Tuple.sort_comp_perm_of_injective belongs in Mathlib/Data/Fin/Tuple/Sort.lean, the counts in Mathlib/Combinatorics/Enumerative/PermutationPattern.lean.

theorem Tuple.sort_comp_perm_of_injective {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} (hf : Function.Injective f) (σ : Equiv.Perm (Fin n)) : sort (f ∘ ⇑σ) = σ⁻¹ * sort f

Sorting a reordering of an injective tuple undoes the reordering.

theorem Equiv.Perm.factorial_mul_card_sort_comp_eq {α : Type u_1} [LinearOrder α] [Fintype α] [DecidableEq α] {k : ℕ} (q : Fin k ↪ α) (ρ : Perm (Fin k)) : k.factorial * {σ : Perm α | Tuple.sort (⇑σ ∘ ⇑q) = ρ}.card = (Fintype.card α).factorial

Order patterns are uniform: each reordering of Fin k is the order pattern of one permutation in k ! on a fixed injective tuple.

theorem Equiv.Perm.factorial_mul_card_monotone_comp {α : Type u_1} [LinearOrder α] [Fintype α] [DecidableEq α] {k : ℕ} (q : Fin k ↪ α) : k.factorial * {σ : Perm α | Monotone (⇑σ ∘ ⇑q)}.card = (Fintype.card α).factorial

One permutation in k ! leaves a fixed injective tuple in increasing order.