EGMO 2023 Problem 1

There are $n \ge 3$ positive real numbers $a_1, a_2, ..., a_n$. For each $1 \le i \le n$ we let $b_i = \frac{a_{i-1} + a_{i+1}}{a_i}$ (here we define $a_0$ to be $a_n$ and $a_{n+1}$ to be $a_1$). Assume that for all $i$ and $j$ in the range $1$ to $n$, we have $a_i \le a_j$ if and only if $b_i ≤ b_j$. Prove that $a_1 = a_2 = ... = a_n$.

_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Data.Real.Basic

theorem solution (n : ℕ) [NeZero n] (hn : n ≥ 3) (a : Fin n → ℝ) (ha : ∀ i, a i > 0) 
    (b : Fin n → ℝ) (hb : ∀ i, b i = (a (i - 1) + a (i + 1)) / (a i)) 
    (h : ∀ i j, a i ≤ a j ↔ b i ≤ b j) : ∀ i j, a i = a j := by
  sorry

Submit Solution

Login to submit a solution.

Recent Submissions