Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1985P5

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.BigOperators

public section


/-!
# USA Mathematical Olympiad 1985, Problem 5

0 < a₁ ≤ a₂ ≤ a₃ ≤ ⋯ is an unbounded sequence of integers. Let bₙ = m if aₘ is the
first member of the sequence to equal or exceed n. Given that a₁₉ = 85, what is the
maximum possible value of a₁ + a₂ + ⋯ + a₁₉ + b₁ + b₂ + ⋯ + b₈₅?
-/

namespace Usa1985P5

/-- The first index `i` (0-based) such that `n ≤ a i`. This exists because `a` is
unbounded. The problem's `bₙ` is `c a hu n + 1` (the 1-based index). -/
noncomputable abbrev c (a : ℕ → ℕ) (hu : ∀ n, ∃ i, n ≤ a i) (n : ℕ) : ℕ :=
  Nat.find (hu n)

/- determine -/ abbrev solution : ℕ := sorry

theorem usa1985_p5 :
    IsGreatest { s : ℕ | ∃ (a : ℕ → ℕ) (_ : Monotone a) (_ : 0 < a 0)
        (hu : ∀ n, ∃ i, n ≤ a i), a 18 = 85 ∧
        s = ∑ i ∈ Finset.range 19, a i + ∑ j ∈ Finset.range 85, (c a hu (j + 1) + 1) }
      solution := sorry

end Usa1985P5

File author(s): Kimi K3

This problem has a complete formalized solution.