Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1999P4

module

public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Ring.Star

public section


/-!
# USA Mathematical Olympiad 1999, Problem 4

Let a₁, a₂, ..., aₙ be a sequence of n > 3 real numbers such that

  a₁ + a₂ + ⋯ + aₙ ≥ n

and

  a₁² + a₂² + ⋯ + aₙ² ≥ n².

Prove that max(a₁, a₂, ..., aₙ) ≥ 2.
-/

namespace Usa1999P4

theorem usa1999_p4 (n : ℕ) (hn : 3 < n) (a : Fin n → ℝ)
    (hsum : (n : ℝ) ≤ ∑ i, a i) (hsq : (n : ℝ) ^ 2 ≤ ∑ i, (a i) ^ 2) :
    ∃ i, 2 ≤ a i := sorry

end Usa1999P4

File author(s): Kimi K3

This problem has a complete formalized solution.