Permutation statistics and cycle structure

Descents, peaks, major index, left-to-right maxima, fixed points and derangements, cycle counts and the smallest cycle of a random permutation, products of cyclic permutations, Stirling and flattened Stirling permutations, Josephus permutations and permutation-guessing puzzles.

TheoremA sum rule for derangements#●ready to prove

For every natural number \(p\), \(\sum_{n=0}^{p} n\, D(n) = \lfloor (p + 1)!/e \rfloor\), where \(D(n)\) is the number of derangements of \(n\) objects.

public theorem_wanted sum_mul_numDerangements_eq_floor (p : ℕ) :
    ((∑ n ∈ Finset.range (p + 1), n * numDerangements n : ℕ) : ℤ) =
      ⌊((p + 1).factorial : ℝ) / Real.exp 1⌋
Sources
  • Jean-Christophe Pain, A Sum Rule for Derangements, INTEGERS 25 (2025), Article A84, Theorem 1.

TheoremZagier's formula for products of two cyclic permutations#✓fully proved

Let \(n\) and \(k\) be integers with \(n \ge 1\) and \(1 \le k \le n\). Call a permutation of an \(n\)-element set cyclic when it has exactly one cycle, fixed points counted as cycles. Write \(c(n+1, k)\) for the unsigned Stirling number of the first kind, the number of permutations of \(n + 1\) elements with exactly \(k\) cycles. If \(\sigma\) and \(\tau\) are chosen independently and uniformly among the cyclic permutations of an \(n\)-element set, then the probability that \(\sigma\tau\) has exactly \(k\) cycles, fixed points included, is

\[\frac{1 + (-1)^{n-k}}{(n+1)!} \, c(n+1, k).\]

Proof: We formalize the plane-permutation transposition and reflection bijections of Chen and Reidys, arXiv:1502.07674, lines 786-1074, and their specialization to Zagier's recurrence, lines 1167-1370. A generating-polynomial coefficient identity supplies the matching Stirling recurrence; descending induction on the cycle count finishes.

public theorem zagier_probability_product_two_cyclic_permutations
    (n k : ℕ) (hn : 0 < n) (hk : 0 < k) (hkn : k ≤ n) :
    ((Fintype.card {p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) //
        Multiset.card p.1.cycleType + Fintype.card (Function.fixedPoints p.1) = 1 ∧
        Multiset.card p.2.cycleType + Fintype.card (Function.fixedPoints p.2) = 1 ∧
        Multiset.card (p.1 * p.2).cycleType +
            Fintype.card (Function.fixedPoints (p.1 * p.2)) = k}) : ℚ) /
      ((Fintype.card {σ : Equiv.Perm (Fin n) //
          Multiset.card σ.cycleType + Fintype.card (Function.fixedPoints σ) = 1}) : ℚ) ^ 2 =
      (1 + (-1 : ℚ) ^ (n - k)) / Nat.factorial (n + 1) *
        Nat.stirlingFirst (n + 1) k
Sources
Uses 3
Proof usesStirling numbers of the first kind count permutations by cycles · Number of cycles of a permutation · Counting cycles via the cycle type
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.