Ben Green's Open Problem 33

References:

• [Gr24] Ben Green's Open Problem 33
• [CaHa20] Caprace, Pierre-Emmanuel, and Pierre de la Harpe. "Groups with irreducibly unfaithful subsets for unitary representations." Confluentes Mathematici 12.1 (2020): 31-68.
• [CrLe07] Croot, Ernie, and Vsevolod F. Lev. "Open problems in additive combinatorics." Additive combinatorics 43.207-233 (2007): 1.

theorem Green33.green_33 : True ↔ ∀ (ε : ℝ), 0 < ε → ∃ᶠ (q : ℕ+) in Filter.atTop, ∃ (A : Finset (ZMod ↑q)), A + A = Finset.univ ∧ |↑A.card / √↑↑q - √2| < ε

Are there infinitely many $q$ for which there is a set $A \subset \mathbb{Z}/q\mathbb{Z}$, $|A| = (\sqrt{2} + o(1))q^{1/2}$, with $A + A = \mathbb{Z}/q\mathbb{Z}$? [Gr24]

theorem Green33.green_33.sanity_sq_bound (q : ℕ+) (A : Finset (ZMod ↑q)) (hA : A + A = Finset.univ) : ↑q ≤ A.card ^ 2

Trivial lower bound: if $A + A = \mathbb{Z}/q\mathbb{Z}$, then $|A|^2 \geq q$, since the sumset $A + A$ has at most $|A|^2$ elements.