Green's Open Problems #84

### What is the conjecture
https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.84

(Solved) Is there a function $f : \{1, ..., N\} \to \{-1, 1\}$ with $|\hat{f}(\theta)| \geq c\sqrt{N}$ for all $\theta$?

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11
* ams-42

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Read problem 84 in the linked open-problems.pdf and inspect the formal-conjectures repository to understand how conjecture statements are represented in Lean. The work is done when this solved conjecture has been added in the repository's established format and categorized consistently with the listed AMS subjects.

Written by the indexing model from the issue text.