Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1980P2

module

public import Mathlib.Algebra.Order.Archimedean.Real.Basic
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Order.Lattice.Nat
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1980, Problem 2

Find the maximum possible number of three term arithmetic progressions
in a monotone sequence of n distinct reals.
-/

namespace Usa1980P2

open Finset

/-!
### Formalization notes

A monotone sequence of *distinct* reals is strictly monotone, and reversing a strictly
decreasing sequence gives a strictly increasing one with the same number of three-term
arithmetic progressions, so we only consider sequences `a : ℕ → ℝ` that are strictly
increasing on `Set.Iio n`.  Three indices `i < j < k` form an arithmetic progression
iff `a i + a k = 2 * a j`, and we count the progressions by their middle index `j`.
-/

/- determine -/ abbrev answer (n : ℕ) : ℕ := sorry

theorem usa1980_p2 (n : ℕ) :
    IsGreatest {m : ℕ | ∃ a : ℕ → ℝ, StrictMonoOn a (Set.Iio n) ∧ m = apCount n a}
      (answer n) := sorry

end Usa1980P2

File author(s): Kimi K3

This problem has a complete formalized solution.