Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2015P6

module

public import Mathlib.Algebra.BigOperators.Field
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.PSeries

public section


/-!
# USA Mathematical Olympiad 2015, Problem 6

Fix $0 < \lambda < 1$, and let $A$ be a multiset of positive integers. Let
$A_n = \{a \in A : a \le n\}$. Assume that for every $n \in \mathbb{N}$, the
multiset $A_n$ contains at most $n\lambda$ numbers. Show that there are
infinitely many $n \in \mathbb{N}$ for which the sum of the elements in $A_n$
is at most $\frac{n(n+1)}{2}\lambda$.
-/

namespace Usa2015P6

theorem usa2015_p6 {lam : ℝ} (hlam : 0 < lam ∧ lam < 1) (A : ℕ → ℕ)
    (hA : ∀ n : ℕ, ∑ m ∈ Finset.Icc 1 n, (A m : ℝ) ≤ lam * n) :
    Set.Infinite
      {n : ℕ | ∑ m ∈ Finset.Icc 1 n, m * (A m : ℝ) ≤ lam * n * (n + 1) / 2} := sorry

end Usa2015P6

File author(s): Kimi K3

This problem has a complete formalized solution.