Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2019P5

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Finset.Sort
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Rat.Star
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Positivity.Basic
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Zify

public section


/-!
# International Mathematical Olympiad 2019, Problem 5

Let n be a positive integer. Harry has n coins lined up on his desk, which can
show either heads or tails. He does the following operation: if there are k > 0
coins which show heads, then he flips the kth coin over; otherwise he stops the
process. (For example, the process starting with THT would be THT → HHT → HTT
→ TTT, which takes three steps.)

Prove the process will always terminate, and determine the average number of
steps this takes over all 2ⁿ configurations.
-/

namespace Imo2019P5

open Finset

/-- The number of coins showing heads in a configuration of `n` coins.
A configuration is a function `Fin n → Bool`, where `c i = true` means that
the `i`-th coin from the left (starting the count at `0`) shows heads. -/
def numHeads {n : ℕ} (c : Fin n → Bool) : ℕ :=
  (univ.filter fun i ↦ c i).card

/-- The index of the coin that Harry flips in configuration `c`: the `k`-th
coin from the left, where `k` is the number of heads. -/
def flipIx {n : ℕ} (c : Fin n → Bool) (h : numHeads c ≠ 0) : Fin n :=
  ⟨numHeads c - 1, by
    have h1 : numHeads c ≤ n := (card_le_univ _).trans (by simp)
    lia⟩

/-- One step of Harry's process: if there are `k > 0` heads, flip the `k`-th
coin from the left; otherwise (all coins show tails) do nothing. -/
def step {n : ℕ} (c : Fin n → Bool) : Fin n → Bool :=
  if h : numHeads c = 0 then c else Function.update c (flipIx c h) (!c (flipIx c h))

/-- The sum of the 1-based positions of the coins showing heads. -/
def weightedSum {n : ℕ} (c : Fin n → Bool) : ℕ :=
  ∑ i : Fin n, (i.val + 1) * (if c i then 1 else 0)

/-- The measure of a configuration: twice the sum of the 1-based positions of
the heads minus the square of the number of heads. We will show that this is
a nonnegative integer (see `meas_nonneg`) which drops by exactly one at each
step (see `step_meas`), hence it equals the number of steps the process takes. -/
def meas {n : ℕ} (c : Fin n → Bool) : ℤ :=
  2 * (weightedSum c : ℤ) - (numHeads c : ℤ) ^ 2

/-- The number of steps that Harry's process takes starting from
configuration `c`. -/
def L {n : ℕ} (c : Fin n → Bool) : ℕ := (meas c).toNat

/-- The average number of steps over all `2 ^ n` initial configurations. -/
/- determine -/ abbrev averageSteps (n : ℕ) : ℚ := sorry

/-- Part (a): the process always terminates. -/
theorem imo2019_p5_parta (n : ℕ) (c : Fin n → Bool) :
    ∃ m : ℕ, step^[m] c = fun _ ↦ false := sorry

/-- Part (b): the average number of steps over all `2 ^ n` configurations is
`n * (n + 1) / 4`. -/
theorem imo2019_p5_partb (n : ℕ) (hn : 0 < n) :
    (∑ c : Fin n → Bool, (L c : ℚ)) / 2 ^ n = averageSteps n := sorry

end Imo2019P5

File author(s): Kimi K3

This problem has a complete formalized solution.