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 : α × Equiv.Perm α // σx.2 σx.1 = σx.1 } ≃ (x : α) × Equiv.Perm ↑{x}ᶜ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Imo1987Q1.card_fixed_points (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype.card { σx : α × Equiv.Perm α // σx.2 σx.1 = σx.1 } = Fintype.card α * (Fintype.card α - 1).factorial

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.

Equations

• Imo1987Q1.fiber α k = {σ : Equiv.Perm α | Fintype.card ↑(Function.fixedPoints ⇑σ) = k}

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

Equations

• Imo1987Q1.instFintypeElemPermFiber α = id inferInstance

@[simp]

theorem Imo1987Q1.mem_fiber (α : Type u_1) [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {k : ℕ} : σ ∈ 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.

Equations

• Imo1987Q1.p α k = Fintype.card ↑(Imo1987Q1.fiber α k)

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

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.

Equations

• One or more equations did not get rendered due to their size.

theorem Imo1987Q1.main_fintype (α : Type u_1) [Fintype α] [DecidableEq α] : ∑ k ∈ Finset.range (Fintype.card α + 1), k * p α k = Fintype.card α * (Fintype.card α - 1).factorial

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

theorem Imo1987Q1.main₀ (n : ℕ) : ∑ k ∈ Finset.range (n + 1), k * p (Fin n) k = n * (n - 1).factorial

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

theorem Imo1987Q1.main {n : ℕ} (hn : 1 ≤ n) : ∑ k ∈ Finset.range (n + 1), k * p (Fin n) k = n.factorial

Main statement for permutations of Fin n.