Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1999P2

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1999, Problem 2

Let n ≥ 2 be a fixed integer. Find the least constant C such that

  ∑_{i < j} xᵢxⱼ(xᵢ² + xⱼ²) ≤ C (∑ i, xᵢ)⁴

for all non-negative real numbers x₁, ..., xₙ.
-/

namespace Imo1999P2

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

theorem imo1999_p2 (n : ℕ) (hn : 2 ≤ n) :
    IsLeast
      {c : ℝ | ∀ x : Fin n → ℝ, (∀ i, 0 ≤ x i) →
        ∑ i, ∑ j ∈ Finset.Ioi i, x i * x j * ((x i) ^ 2 + (x j) ^ 2) ≤
          c * (∑ i, x i) ^ 4}
      C := sorry

end Imo1999P2

This problem does not yet have a complete formalized solution.