mathlib3 documentation

mathlib-archive / imo.imo1987_q1

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.

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
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
@[protected, instance]
def imo1987_q1.fiber (α : Type u_1) [fintype α] [decidable_eq α] (k : ) :

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

Equations
Instances for imo1987_q1.fiber
@[simp]
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
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
theorem imo1987_q1.main_fintype (α : Type u_1) [fintype α] [decidable_eq α] :

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

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.

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.