Documentation

Archive.Imo.Imo1987Q1

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.
Instances For
    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 : ) :

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

    Equations
    Instances For
      @[simp]
      theorem Imo1987Q1.mem_fiber (α : Type u_1) [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {k : } :
      def Imo1987Q1.p (α : Type u_1) [Fintype α] [DecidableEq α] (k : ) :

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

      Equations
      Instances For
        def Imo1987Q1.fixedPointsEquiv' (α : Type u_1) [Fintype α] [DecidableEq α] :
        (k : Fin (Fintype.card α + 1)) × (σ : (Imo1987Q1.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.
        Instances For
          theorem Imo1987Q1.main_fintype (α : Type u_1) [Fintype α] [DecidableEq α] :
          kFinset.range (Fintype.card α + 1), k * Imo1987Q1.p α k = Fintype.card α * (Fintype.card α - 1).factorial

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

          theorem Imo1987Q1.main₀ (n : ) :
          kFinset.range (n + 1), k * Imo1987Q1.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) :
          kFinset.range (n + 1), k * Imo1987Q1.p (Fin n) k = n.factorial

          Main statement for permutations of Fin n.