Formalization of IMO 1987, Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (fixed_points σ) 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.

source

def imo1987_q1.fixed_points_equiv (α : Type u_1) [fintype α] [decidable_eq α] :

{σ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}ᶜ).

Equations

imo1987_q1.fixed_points_equiv α = ((equiv.set_prod_equiv_sigma (λ (σx : α × equiv.perm α), ⇑(σx.snd) σx.fst = σx.fst)).trans (equiv.sigma_congr_right (λ (x : α), equiv.set.of_eq _))).trans (equiv.sigma_congr_right (λ (x : α), equiv.set.compl (equiv.refl ↥{x})))

source

theorem imo1987_q1.card_fixed_points (α : Type u_1) [fintype α] [decidable_eq α] :

fintype.card {σx // ⇑(σx.snd) σx.fst = σx.fst} = fintype.card α * (fintype.card α - 1).factorial

source

@[protected, instance]

def imo1987_q1.fiber.fintype (α : Type u_1) [fintype α] [decidable_eq α] (k : ℕ) :

fintype ↥(imo1987_q1.fiber α k)

source

def imo1987_q1.fiber (α : Type u_1) [fintype α] [decidable_eq α] (k : ℕ) :

set (equiv.perm α)

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

Equations

imo1987_q1.fiber α k = {σ : equiv.perm α | fintype.card ↥(function.fixed_points ⇑σ) = k}

Instances for ↥imo1987_q1.fiber

imo1987_q1.fiber.fintype

source

@[simp]

theorem imo1987_q1.mem_fiber (α : Type u_1) [fintype α] [decidable_eq α] {σ : equiv.perm α} {k : ℕ} :

σ ∈ imo1987_q1.fiber α k ↔ fintype.card ↥(function.fixed_points ⇑σ) = k

source

def imo1987_q1.p (α : Type u_1) [fintype α] [decidable_eq α] (k : ℕ) :

ℕ

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

Equations

imo1987_q1.p α k = fintype.card ↥(imo1987_q1.fiber α k)

source

def imo1987_q1.fixed_points_equiv' (α : Type u_1) [fintype α] [decidable_eq α] :

(Σ (k : fin (fintype.card α + 1)) (σ : ↥(imo1987_q1.fiber α ↑k)), ↥(function.fixed_points ⇑(σ.val))) ≃ {σx // ⇑(σx.snd) σx.fst = σx.fst}

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

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

Equations

imo1987_q1.fixed_points_equiv' α = {to_fun := λ (p : Σ (k : fin (fintype.card α + 1)) (σ : ↥(imo1987_q1.fiber α ↑k)), ↥(function.fixed_points ⇑(σ.val))), ⟨(↑(p.snd.snd), ↑(p.snd.fst)), _⟩, inv_fun := λ (p : {σx // ⇑(σx.snd) σx.fst = σx.fst}), ⟨⟨fintype.card ↥(function.fixed_points ⇑(p.val.snd)) (subtype.fintype (λ (x : α), x ∈ function.fixed_points ⇑(p.val.snd))), _⟩, ⟨⟨p.val.snd, _⟩, ⟨p.val.fst, _⟩⟩⟩, left_inv := _, right_inv := _}

source

theorem imo1987_q1.main_fintype (α : Type u_1) [fintype α] [decidable_eq α] :

(finset.range (fintype.card α + 1)).sum (λ (k : ℕ), k * imo1987_q1.p α k) = fintype.card α * (fintype.card α - 1).factorial

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

source

theorem imo1987_q1.main₀ (n : ℕ) :

(finset.range (n + 1)).sum (λ (k : ℕ), k * imo1987_q1.p (fin n) k) = n * (n - 1).factorial

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

source

theorem imo1987_q1.main {n : ℕ} (hn : 1 ≤ n) :

(finset.range (n + 1)).sum (λ (k : ℕ), k * imo1987_q1.p (fin n) k) = n.factorial

Main statement for permutations of fin n.