Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2010P6

import Mathlib

/-!
# International Mathematical Olympiad 2010, Problem 6

Let a₁, a₂, a₃, ... be a sequence of positive real numbers. Suppose that for some
positive integer s, we have
    aₙ = max{aₖ + aₙ₋ₖ | 1 ≤ k ≤ n − 1}
for all n > s. Prove that there exist positive integers l and N, with l ≤ s and
such that aₙ = aₗ + aₙ₋ₗ for all n ≥ N.
-/

namespace Imo2010P6


theorem imo2010_p6 {a : ℕ+ → ℝ} {s : ℕ+}
  (h : ∀ n > s, a n = Finset.max ((Finset.Icc 1 (n-1)).image (fun k ↦ a k + a (n - k)))) :
  ∃ l N : ℕ+, (l ≤ s ∧ ∀ n ≥ N, a n = a l + a (n - l)) := sorry

end Imo2010P6

File author(s): Markus Rydh

This problem has a complete formalized solution.