Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1987P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.Normed.Ring.Lemmas
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Positivity.Basic

public section


/-!
# International Mathematical Olympiad 1987, Problem 3

Let $x_1, x_2, \ldots, x_n$ be real numbers satisfying
$x_1^2 + x_2^2 + \cdots + x_n^2 = 1$. Prove that for every integer $k \geq 2$
there are integers $a_1, a_2, \ldots, a_n$, not all zero, such that
$|a_i| \leq k - 1$ for all $i$, and
$$|a_1 x_1 + a_2 x_2 + \cdots + a_n x_n| \leq \frac{(k - 1)\sqrt{n}}{k^n - 1}.$$
-/

namespace Imo1987P3

theorem imo1987_p3 {n : ℕ} (hn : 0 < n) (x : Fin n → ℝ) (hx : ∑ i, x i ^ 2 = 1)
    {k : ℕ} (hk : 2 ≤ k) :
    ∃ a : Fin n → ℤ, (∀ i, |a i| ≤ (k : ℤ) - 1) ∧ (∃ i, a i ≠ 0) ∧
      |∑ i, (a i : ℝ) * x i| ≤ ((k : ℝ) - 1) * Real.sqrt n / ((k : ℝ) ^ n - 1) := sorry

end Imo1987P3

File author(s): Kimi K3

This problem has a complete formalized solution.