Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2000P3

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Finset.Max
public import Mathlib.Data.Set.Finite.Lattice
public import Mathlib.Order.ConditionallyCompleteLattice.Indexed

public section


/-!
# International Mathematical Olympiad 2000, Problem 3

Let n ≥ 2 be a positive integer and λ a positive real number. Initially there are n fleas
on a horizontal line, not all at the same point. We define a move as choosing two fleas at
some points A and B, with A to the left of B, and letting the flea from A jump over the
flea from B to the point C so that BC/AB = λ.

Determine all values of λ such that, for any point M on the line and for any initial
position of the n fleas, there exists a sequence of moves that will take them all to
the right of M.
-/

namespace Imo2000P3

open Finset

/-- A single move with jump ratio `lam`: flea `i`, sitting at some point `A = x i`,
jumps over flea `j` at `B = x j` (with `A` to the left of `B`) and lands at the point
`C = B + lam * (B - A)`, so that `BC / AB = lam`. All other fleas stay put. -/
def Move (lam : ℝ) {n : ℕ} (x y : Fin n → ℝ) : Prop :=
  ∃ i j, x i < x j ∧ y = Function.update x i (x j + lam * (x j - x i))

/-- `Reachable lam x y` means that configuration `y` can be reached from configuration
`x` by a finite sequence of moves with jump ratio `lam`. -/
def Reachable (lam : ℝ) {n : ℕ} (x y : Fin n → ℝ) : Prop :=
  Relation.ReflTransGen (Move lam) x y

/-- The property of `lam` in the problem: starting from any initial configuration in
which the fleas are not all at the same point, for every point `M` on the line there is
a finite sequence of moves taking all the fleas strictly to the right of `M`. -/
def AllRightOf {n : ℕ} (lam : ℝ) : Prop :=
  ∀ x : Fin n → ℝ, (∃ i j, x i ≠ x j) → ∀ M : ℝ,
    ∃ y : Fin n → ℝ, Reachable lam x y ∧ ∀ i, M < y i

/- determine -/ abbrev solution_set (n : ℕ) : Set ℝ := sorry

theorem imo2000_p3 (n : ℕ) (hn : 2 ≤ n) (lam : ℝ) :
    lam ∈ solution_set n ↔ (0 < lam ∧ AllRightOf (n := n) lam) := sorry

end Imo2000P3

File author(s): Kimi K3

This problem has a complete formalized solution.