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

noncomputable def rec_max {n : ℕ+} (f : ℕ+ → ℝ) (h : 1 < n) := Finset.max' ((Finset.Icc 1 (n - 1)).image (fun k ↦ f k + f (n - k)))
    (Finset.image_nonempty.mpr (Finset.nonempty_Icc.mpr (PNat.le_sub_one_of_lt h)))

def Rec (s : ℕ+) (f : ℕ+ → ℝ) := ∀ n (h : n > s), f n = rec_max f (PNat.one_lt_of_lt h)

theorem imo2010_p6 {a : ℕ+ → ℝ} {s : ℕ+} : Rec s a → ∃ 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.