Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2009P4

module

public import Mathlib.Algebra.Order.Star.Real

public section


/-!
# USA Mathematical Olympiad 2009, Problem 4

For n ≥ 2, let a₁, a₂, ..., aₙ be positive real numbers such that

  (a₁ + a₂ + ... + aₙ) (1/a₁ + 1/a₂ + ... + 1/aₙ) ≤ (n + 1/2)².

Prove that max(a₁, a₂, ..., aₙ) ≤ 4 min(a₁, a₂, ..., aₙ).
-/

namespace Usa2009P4

theorem usa2009_p4 {n : ℕ} (hn : 2 ≤ n) (a : Fin n → ℝ) (ha : ∀ i, 0 < a i)
    (h : (∑ i, a i) * (∑ i, 1 / a i) ≤ ((n : ℝ) + 1 / 2) ^ 2) :
    (Finset.univ.image a).max' (Finset.image_nonempty.mpr ⟨⟨0, by lia⟩, Finset.mem_univ _⟩)
      ≤ 4 * (Finset.univ.image a).min'
          (Finset.image_nonempty.mpr ⟨⟨0, by lia⟩, Finset.mem_univ _⟩) := sorry

end Usa2009P4

File author(s): Kimi K3

This problem has a complete formalized solution.