Ben Green's Open Problem 81

Let $A$ be a set of size $n$ integers. Is there some absolute constant $c > 0$ and $\theta$ such that $\sum_{a \in A} \cos(a \theta) \leq - c \sqrt{n}$?

References:

• [Ben Green's Open Problem 81](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.11 Problem 81)
• erdosproblems.com/510

theorem Green81.green_81 : sorry ↔ ∃ (c : ℝ) (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ (θ : ℝ), ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N