Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2000P6

module

public import Mathlib.Algebra.Order.Star.Real

public section


/-!
# USA Mathematical Olympiad 2000, Problem 6

Let a₁, b₁, a₂, b₂, ..., aₙ, bₙ be nonnegative real numbers.
Prove that

  ∑ᵢⱼ min(aᵢaⱼ, bᵢbⱼ) ≤ ∑ᵢⱼ min(aᵢbⱼ, aⱼbᵢ),

where each sum is taken over all n² pairs (i, j).
-/

namespace Usa2000P6

theorem usa2000_p6 (n : ℕ) (a b : Fin n → ℝ) (ha : ∀ i, 0 ≤ a i) (hb : ∀ i, 0 ≤ b i) :
    ∑ i, ∑ j, min (a i * a j) (b i * b j) ≤
    ∑ i, ∑ j, min (a i * b j) (a j * b i) := sorry

end Usa2000P6

File author(s): Kimi K3

This problem has a complete formalized solution.