Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2008P5

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Analysis.Normed.Field.Basic

public section


/-!
# USA Mathematical Olympiad 2008, Problem 5

Three nonnegative real numbers r₁, r₂, r₃ are written on a blackboard.
These numbers have the property that there exist integers a₁, a₂, a₃,
not all zero, satisfying a₁r₁ + a₂r₂ + a₃r₃ = 0. We are permitted to
perform the following operation: find two numbers x, y on the
blackboard with x ≤ y, then erase y and write y − x in its place.
Prove that after a finite number of such operations, we can end up
with at least one 0 on the blackboard.
-/

namespace Usa2008P5

/-- One legal operation of the game: choose two distinct positions `i` and `j`
with `r j ≤ r i`, erase the number `r i` and write `r i - r j` in its place. -/
abbrev Step (r r' : Fin 3 → ℝ) : Prop :=
  ∃ i j : Fin 3, i ≠ j ∧ r j ≤ r i ∧ r' = Function.update r i (r i - r j)

theorem usa2008_p5 (r : Fin 3 → ℝ) (hr : ∀ i, 0 ≤ r i)
    (a : Fin 3 → ℤ) (ha : a ≠ 0) (hsum : ∑ i, (a i : ℝ) * r i = 0) :
    ∃ r' : Fin 3 → ℝ, Relation.ReflTransGen Step r r' ∧ ∃ i, r' i = 0 := sorry

end Usa2008P5

File author(s): Kimi K3

This problem has a complete formalized solution.