Formalization of IMO 1987, Q1

Let $p_{n, k}$ be the number of permutations of a set of cardinality n ≥ 1 that fix exactly k elements. Prove that $∑_{k=0}^n k p_{n,k}=n!$.

To prove this identity, we show that both sides are equal to the cardinality of the set {(x : α, σ : Perm α) | σ x = x}, regrouping by card (fixedPoints σ) for the left hand side and by x for the right hand side.

The original problem assumes n ≥ 1. It turns out that a version with n * (n - 1)! in the RHS holds true for n = 0 as well, so we first prove it, then deduce the original version in the case n ≥ 1.

def Imo1987Q1.fixedPointsEquiv (α : Type u_1) [DecidableEq α] : { σx // ↑σx.snd σx.fst = σx.fst } ≃ (x : α) × Equiv.Perm ↑{x}ᶜ

The set of pairs (x : α, σ : Perm α) such that σ x = x is equivalent to the set of pairs (x : α, σ : Perm {x}ᶜ).

theorem Imo1987Q1.card_fixed_points (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype.card { σx // ↑σx.snd σx.fst = σx.fst } = Fintype.card α * Nat.factorial (Fintype.card α - 1)

def Imo1987Q1.fiber (α : Type u_1) [Fintype α] [DecidableEq α] (k : ℕ) : Set (Equiv.Perm α)

Given α : Type _ and k : ℕ, fiber α k is the set of permutations of α with exactly k fixed points.

instance Imo1987Q1.instFintypeElemPermFiber (α : Type u_1) [Fintype α] [DecidableEq α] {k : ℕ} : Fintype ↑(Imo1987Q1.fiber α k)

@[simp]

theorem Imo1987Q1.mem_fiber (α : Type u_1) [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {k : ℕ} : σ ∈ Imo1987Q1.fiber α k ↔ Fintype.card ↑(Function.fixedPoints ↑σ) = k

def Imo1987Q1.p (α : Type u_1) [Fintype α] [DecidableEq α] (k : ℕ) : ℕ

p α k is the number of permutations of α with exactly k fixed points.

def Imo1987Q1.fixedPointsEquiv' (α : Type u_1) [Fintype α] [DecidableEq α] : (k : Fin (Fintype.card α + 1)) × (σ : ↑(Imo1987Q1.fiber α ↑k)) × ↑(Function.fixedPoints ↑↑σ) ≃ { σx // ↑σx.snd σx.fst = σx.fst }

The set of triples (k ≤ card α, σ ∈ fiber α k, x ∈ fixedPoints σ) is equivalent to the set of pairs (x : α, σ : Perm α) such that σ x = x. The equivalence sends (k, σ, x) to (x, σ) and (x, σ) to (card (fixedPoints σ), σ, x).

It is easy to see that the cardinality of the LHS is given by ∑ k : Fin (card α + 1), k * p α k.

theorem Imo1987Q1.main_fintype (α : Type u_1) [Fintype α] [DecidableEq α] : (Finset.sum (Finset.range (Fintype.card α + 1)) fun k => k * Imo1987Q1.p α k) = Fintype.card α * Nat.factorial (Fintype.card α - 1)

Main statement for any (α : Type _) [Fintype α].

theorem Imo1987Q1.main₀ (n : ℕ) : (Finset.sum (Finset.range (n + 1)) fun k => k * Imo1987Q1.p (Fin n) k) = n * Nat.factorial (n - 1)

Main statement for permutations of Fin n, a version that works for n = 0.

theorem Imo1987Q1.main {n : ℕ} (hn : 1 ≤ n) : (Finset.sum (Finset.range (n + 1)) fun k => k * Imo1987Q1.p (Fin n) k) = Nat.factorial n

Main statement for permutations of Fin n.