Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1997P3

import Mathlib.Algebra.Group.Submonoid.Membership
import Mathlib.Data.Real.Sign
import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1997, Problem 3

Let $x_1, x_2, \dots, x_n$ be real numbers satisfying the conditions
$|x_1 + x_2 + \cdots + x_n| = 1$ and
$|x_i| ≤ \frac{n+1}2$ for $i = 1, 2, \dots, n$. Show that there exists
a permutation $y_1, y_2, \dots, y_n$ of $x_1, x_2, \dots, x_n$ such
that $|y_1 + 2y_2 + \cdots + ny_n| ≤ \frac{n+1}2$.
-/

namespace Imo1997P3

theorem imo1997_p3 {n : ℕ} {x : Fin n → ℝ} (hx₁ : |∑ i, x i| = 1)
    (hx₂ : ∀ i, |x i| ≤ (n + 1) / 2) :
    ∃ p : Equiv.Perm (Fin n), |∑ i, (i + 1) * x (p i)| ≤ (n + 1) / 2 := sorry

end Imo1997P3

File author(s): Jeremy Tan

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo1997Q3.lean.