## Compfiles: Catalog Of Math Problems Formalized In Lean

## Usa1981P5

```
import Mathlib.Tactic
/-!
# USA Mathematical Olympiad 1981, Problem 5
Show that for any positive real number x and any nonnegative
integer n,
∑ₖ (⌊kx⌋/k) ≤ ⌊nx⌋
where the sum goes from k = 1 to k = n, inclusive.
-/
namespace Usa1981P5
theorem usa1981_p5 (x : ℝ) (n : ℕ) :
∑ k ∈ Finset.Icc 1 n, ((⌊k * x⌋:ℝ)/k) ≤ ⌊n * x⌋ := sorry
end Usa1981P5
```

File author(s): David Renshaw

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: