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

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

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

    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.

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

        Instances For

          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.