Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1981P2

import Mathlib

namespace Imo1981P2

/-!
# International Mathematical Olympiad 1981, Problem 2

Let $1 \le r \le n$ and consider all subsets of $r$ elements of the set $\{ 1, 2, \ldots , n \}$.
Each of these subsets has a smallest member. Let $F(n,r)$ denote the arithmetic mean of these smallest numbers; prove that
\[ F(n,r) = \frac{n+1}{r+1}. \]
-/

open Finset

variable (n r : ℕ)

def arith_mean (ms : Multiset ℕ) : ℚ := ms.sum / ms.card

def F : ℚ := arith_mean <| ((Icc 1 n).powersetCard r).val.map (fun s => s.min.getD 0)


theorem imo1981_p2 (rpos : 1 ≤ r) (hrn : r ≤ n) : F n r = (n+1)/(r+1) := sorry

end Imo1981P2

File author(s): Constantin Seebach

This problem has a complete formalized solution.