IMO 2015 A1 #
Let $F$ be a totally ordered field. Let $(a_n)_{n ≥ 0}$ be a sequence of positive elements of $F$ such that for any $k ∈ ℕ$, $$ a_{k + 1} ≥ \frac{(k + 1) a_k}{a_k^2 + k}. $$ Prove that for every $n ≥ 2$, $$ a_0 + a_1 + … + a_{n - 1} ≥ n. $$
Solution #
We follow the official solution.
theorem
IMOSL.IMO2015A1.general_result
{R : Type u_1}
{n : ℕ}
[CommSemiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
[ExistsAddOfLE R]
{a b : ℕ → R}
(ha : ∀ (k : ℕ), a k > 0)
(hb : ∀ (k : ℕ), b k ≥ 0)
(hab : ∀ (k : ℕ), b (k + 1) ≤ a k + b k)
(hab0 : ∀ (k : ℕ), a k * b k = ↑k)
(hn : n ≥ 2)
:
A version of the statement to be proved that is free of division.
theorem
IMOSL.IMO2015A1.final_solution
{F : Type u_1}
{n : ℕ}
[Semifield F]
[LinearOrder F]
[IsStrictOrderedRing F]
[ExistsAddOfLE F]
{a : ℕ → F}
(ha : ∀ (k : ℕ), a k > 0)
(ha0 : ∀ (k : ℕ), ↑(k + 1) * a k / (a k ^ 2 + ↑k) ≤ a (k + 1))
(hn : n ≥ 2)
:
Final solution