Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1997P6

module

public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Data.Finset.Max
public import Mathlib.Order.Interval.Finset.Nat

public section


/-!
# USA Mathematical Olympiad 1997, Problem 6

Suppose the sequence of nonnegative integers a₁, a₂, ..., a₁₉₉₇ satisfies

  aᵢ + aⱼ ≤ aᵢ₊ⱼ ≤ aᵢ + aⱼ + 1

for all i, j ≥ 1 with i + j ≤ 1997.
Prove that there exists a real number x such that
aₙ = ⌊nx⌋ for all 1 ≤ n ≤ 1997.
-/

namespace Usa1997P6

theorem usa1997_p6 (a : ℕ → ℕ)
    (hlo : ∀ i j : ℕ, 1 ≤ i → 1 ≤ j → i + j ≤ 1997 → a i + a j ≤ a (i + j))
    (hhi : ∀ i j : ℕ, 1 ≤ i → 1 ≤ j → i + j ≤ 1997 → a (i + j) ≤ a i + a j + 1) :
    ∃ x : ℝ, ∀ n : ℕ, 1 ≤ n → n ≤ 1997 → (a n : ℤ) = ⌊(n : ℝ) * x⌋ := sorry

end Usa1997P6

File author(s): Kimi K3

This problem has a complete formalized solution.