Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2010P3

module

public import Mathlib.Algebra.Order.Star.Real

public section


/-!
# USA Mathematical Olympiad 2010, Problem 3

The 2010 positive real numbers $a_1, a_2, \ldots, a_{2010}$ satisfy the inequality
$a_i a_j \le i + j$ for all $1 \le i < j \le 2010$. Determine, with proof, the largest
possible value of the product $a_1 a_2 \cdots a_{2010}$.
-/

namespace Usa2010P3

/- determine -/ abbrev answer : ℝ := sorry

theorem usa2010_p3 :
    IsGreatest {x : ℝ | ∃ a : ℕ → ℝ,
      (∀ i, i < 2010 → 0 < a i) ∧
      (∀ i j : ℕ, i < j → j < 2010 → a i * a j ≤ (i : ℝ) + 1 + ((j : ℝ) + 1)) ∧
      x = ∏ i ∈ Finset.range 2010, a i} answer := sorry

end Usa2010P3

File author(s): Kimi K3

This problem has a complete formalized solution.