Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2012P1

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.Real.Sqrt
public import Mathlib.Data.Fin.Tuple.Sort
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Fib.Basic
public import Mathlib.Tactic.IntervalCases

public section


/-!
# USA Mathematical Olympiad 2012, Problem 1

Find all integers n ≥ 3 such that among any n positive real numbers
a₁, a₂, ..., aₙ with

  max(a₁, a₂, ..., aₙ) ≤ n · min(a₁, a₂, ..., aₙ),

there exist three that are the side lengths of an acute triangle.
-/

namespace Usa2012P1

/-- Three real numbers are the side lengths of an acute triangle iff the strict
triangle inequalities hold and the sum of the squares of any two of them is strictly
greater than the square of the third one. -/
def IsAcuteTriple (x y z : ℝ) : Prop :=
  x + y > z ∧ y + z > x ∧ z + x > y ∧
  x ^ 2 + y ^ 2 > z ^ 2 ∧ y ^ 2 + z ^ 2 > x ^ 2 ∧ z ^ 2 + x ^ 2 > y ^ 2

/-- The property of `n` that the problem asks to characterize: among any `n` positive
real numbers whose maximum is at most `n` times their minimum (here expressed as
`a i ≤ n * a j` for all indices `i j`), some three are the side lengths of an acute
triangle. -/
def IsGood (n : ℕ) : Prop :=
  ∀ a : Fin n → ℝ,
    (∀ i, 0 < a i) →
    (∀ i j, a i ≤ (n : ℝ) * a j) →
    ∃ i j k, i ≠ j ∧ j ≠ k ∧ k ≠ i ∧ IsAcuteTriple (a i) (a j) (a k)

/- determine -/ abbrev solution_set : Set ℕ := sorry

theorem usa2012_p1 (n : ℕ) : 3 ≤ n ∧ IsGood n ↔ n ∈ solution_set := sorry

end Usa2012P1

File author(s): Kimi K3

This problem has a complete formalized solution.