IMO 1982 Q3

Consider infinite sequences $\{x_n\}$ of positive reals such that $x_0 = 1$ and $x_0 \ge x_1 \ge x_2 \ge \ldots$

a) Prove that for every such sequence there is an $n \ge 1$ such that:

$$\frac{x_0^2}{x_1} + \ldots + \frac{x_{n-1}^2}{x_n} \ge 3.999$$

b) Find such a sequence such that for all $n$:

$$\frac{x_0^2}{x_1} + \ldots + \frac{x_{n-1}^2}{x_n} < 4$$

The solution is based on Solution 1 from the Art of Problem Solving website. For part a, we use Sedrakyan's lemma to show the sum is bounded below by $\frac{4n}{n + 1}$, which can be made arbitrarily close to $4$ by taking large $n$. For part b, we show the sequence $x_n = 2^{-n}$ satisfies the desired inequality.

theorem Imo1982Q3.le_avg {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x) : ∑ k ∈ Finset.range (n + 1), x k ≤ (∑ k ∈ Finset.range n, x k) * (1 + 1 / ↑n)

x n is at most the average of all previous terms in the sequence.

This is expressed here with ∑ k ∈ range n, x k added to both sides.

theorem Imo1982Q3.ineq {x : ℕ → ℝ} {n : ℕ} (hn : n ≠ 0) (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ (k : ℕ), 0 < x k) : 4 * ↑n / (↑n + 1) ≤ ∑ k ∈ Finset.range (n + 1), x k ^ 2 / x (k + 1)

The main inequality used for part a.

theorem imo1982_q3a {x : ℕ → ℝ} (hx : Antitone x) (h0 : x 0 = 1) (hp : ∀ (k : ℕ), 0 < x k) : ∃ (n : ℕ), 3.999 ≤ ∑ k ∈ Finset.range n, x k ^ 2 / x (k + 1)

Part a of the problem is solved by n = 4000.

theorem imo1982_q3b : ∃ (x : ℕ → ℝ), Antitone x ∧ x 0 = 1 ∧ (∀ (k : ℕ), 0 < x k) ∧ ∀ (n : ℕ), ∑ k ∈ Finset.range n, x k ^ 2 / x (k + 1) < 4

Part b of the problem is solved by x k = (1 / 2) ^ k.