IMO 1997 Q3

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$.

Solution

For a permutation $π$ let $S(π) = \sum_{i=1}^n i x_{π(i)}$. We wish to show that there exists $π$ with $|S(π)| ≤ \frac{n+1}2$.

Suppose the contrary, that all permutations satisfy $\frac{n+1}2 < |S(π)|$. Then we note that for two permutations $π, π'$ differing by a swap of adjacent elements, say $x_k$ and $x_{k+1}$, $|S(π) - S(π')| = |x_k - x_{k+1}| ≤ n + 1$. This being the size of the interval $[-\frac{n+1}/2, \frac{n+1}/2]$ forbidden to the $|S(π)|$, $S(π)$ and $S(π')$ must be on the same side of said interval, i.e. they have the same sign. By induction all the $S(\pi)$ have the same sign.

But now consider the identity permutation $1$ and the reverse permutation $R$. We have $|S(1) + S(R)| = |(1 + n)x_1 + \cdots + (n + 1)x_n| = (n + 1)|x_1 + \cdots + x_n| = n + 1$. Since $S(1)$ and $S(R)$ have the same sign yet are strictly larger than $\frac{n+1}2$ in absolute value, $|S(1) + S(R)| > n + 1$, which yields a contradiction. Therefore the initial assumption that all permutations satisfy $\frac{n+1}2 < |S(π)|$ must be false; the result follows.

def Imo1997Q3.S {n : ℕ} (x : Fin n → ℝ) (p : Equiv.Perm (Fin n)) : ℝ

The sum $x_1 + 2x_2 + \cdots + nx_n$ mentioned in the problem.

Equations

• Imo1997Q3.S x p = ∑ i : Fin n, (↑↑i + 1) * x (p i)

theorem Imo1997Q3.sign_eq_of_abs_sub_le {a b c : ℝ} (ha : c / 2 < |a|) (hb : c / 2 < |b|) (hc : 0 < c) (hs : |a - b| ≤ c) : SignType.sign a = SignType.sign b

theorem Imo1997Q3.lt_abs_add_of_sign_eq {a b c : ℝ} (ha : c / 2 < |a|) (hb : c / 2 < |b|) (hc : 0 < c) (hs : SignType.sign a = SignType.sign b) : c < |a + b|

theorem Imo1997Q3.sign_eq_of_contra {n : ℕ} {x : Fin (n + 1) → ℝ} (hx₂ : ∀ (i : Fin (n + 1)), |x i| ≤ (↑(n + 1) + 1) / 2) (h : ∀ (p : Equiv.Perm (Fin (n + 1))), (↑(n + 1) + 1) / 2 < |S x p|) (p : Equiv.Perm (Fin (n + 1))) : SignType.sign (S x 1) = SignType.sign (S x p)

For fixed nonempty x, assuming the opposite of what is to be proven, the signs of S x p are all the same.

theorem Imo1997Q3.S_one_add_S_revPerm {n : ℕ} {x : Fin n → ℝ} (hx₁ : |∑ i : Fin n, x i| = 1) : |S x 1 + S x Fin.revPerm| = ↑n + 1

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