Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2026P1

import Mathlib.Tactic
import Compfiles.Usa1981P5

/-!
# USA Mathematical Olympiad 2026, Problem 1

Fix an integer n ≥ 2. For which real numbers x is
  ⌊nx⌋ - ∑_{k=1}^n ⌊kx⌋/k
maximal, and what is the maximal value that this expression can take?
-/

namespace Usa2026P1

open Real
open Finset

noncomputable def f (n : ℕ) (x : ℝ) : ℝ :=
  (⌊(n : ℝ) * x⌋ : ℝ) - ∑ k ∈ Icc 1 n, (⌊(k : ℝ) * x⌋ : ℝ) / (k : ℝ)

noncomputable /- determine -/ abbrev solution_value : ℕ → ℝ := sorry

theorem usa2026_p1 (n : ℕ) (hn : 2 ≤ n) :
  (∀ x : ℝ, f n x ≤ solution_value n) ∧
  (∃ x : ℝ, f n x = solution_value n) := sorry

end Usa2026P1

File author(s): Daniel Liao

This problem has a complete formalized solution.