Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1975P5

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Tactic.CancelDenoms.Core
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1975, Problem 5

A pack of n cards, including three aces, is well shuffled. Cards are turned
over in turn. Show that the expected number of cards that must be turned over
to reach the second ace is (n+1)/2.

## Formalization notes

We model the well-shuffled pack by the set of positions occupied by the three
aces, which is uniformly distributed over the 3-element subsets of
`{1, ..., n}`. The number of cards that must be turned over to reach the
second ace is then the middle (second-smallest) of the three ace positions,
and the expected number of cards is the average of this quantity over all
3-element subsets.
-/

namespace Usa1975P5

open Finset

/-- The sample space: the 3-element subsets of the positions `{1, ..., n}`;
each such subset records the positions of the three aces in the pack. -/
def aceSets (n : ℕ) : Finset (Finset ℕ) := (Icc 1 n).powersetCard 3

/-- Reflection of the pack about its middle: the card in position `x`
of a pack of `n` cards moves to position `n + 1 - x`. -/
def reflect (n x : ℕ) : ℕ := n + 1 - x

/-- The minimum of a set of naturals, defaulting to `0` for the empty set. -/
def minD (S : Finset ℕ) : ℕ := (S.min).untopD 0

/-- The maximum of a set of naturals, defaulting to `0` for the empty set. -/
def maxD (S : Finset ℕ) : ℕ := (S.max).unbotD 0

/-- The middle element of a 3-element set of natural numbers, computed as
the sum minus the minimum minus the maximum. When `S` is the set of ace
positions, this is the number of cards turned over to reach the second ace. -/
def mid (S : Finset ℕ) : ℤ :=
  (∑ x ∈ S, (x : ℤ)) - (minD S : ℤ) - (maxD S : ℤ)

/-- The expected number of cards that must be turned over to reach the
second ace. -/
/- determine -/ abbrev expected (n : ℕ) : ℚ := sorry

theorem usa1975_p5 (n : ℕ) (hn : 3 ≤ n) :
    (∑ S ∈ aceSets n, (mid S : ℚ)) / n.choose 3 = expected n := sorry

end Usa1975P5

File author(s): Kimi K3

This problem has a complete formalized solution.