Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1982P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1982, Problem 3

Consider infinite sequences $\{x_n \}$ of positive reals such that $x_0 = 0$ and
$x_0 \geq x_1 \geq x_2 \geq ...$

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

$\frac{x_0^2}{x_1} + \ldots + \frac{x_{n-1}^2}{x_n} \geq 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$
-/

namespace Imo1982Q3

theorem iom1982_p3a {x : ℕ → ℝ} (x_pos : ∀ i, x i > (0 : ℝ))
    (hx₀ : x 0 = (1 : ℝ))
    (hx : ∀ i , x (i + 1) ≤ x i) :
    ∃ N : ℕ, 3.999 ≤ ∑ n : Fin N, (x n)^2 / x (n + 1) := sorry

noncomputable /- determine -/ abbrev sol : ℕ → ℝ := sorry

theorem imo1982_p3b :
    (∀ i, sol i > 0) ∧ (∀ i, sol (i + 1) ≤ sol i) ∧ (sol 0 = 1)
      ∧ ∀ N, ∑ n ∈ Finset.range (N + 1), (sol n ^2 / (sol (n + 1))) < 4 := sorry

end Imo1982Q3

File author(s): Alex Brodbelt

This problem has a complete formalized solution.

The solution was imported from mathlib4.