Green's Open Problem 27

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [Be23] Bedert, Benjamin. "On unique sums in Abelian groups." Combinatorica 44.2 (2024): 269-298.
• [St76] Straus, E. G. "Differences of residues (mod p)." Journal of Number Theory 8.1 (1976): 40-42.

noncomputable def Green27.m (p : ℕ) : ℝ

This is $m(p)$ in [Be23]: the size of the smallest set $A \subset \mathbb{Z} / p\mathbb{Z}$ (with at least two elements) for which no element in the sumset $A + A$ has a unique representation.

Equations

• Green27.m p = sInf {x : ℝ | ∃ (A : Finset (ZMod p)) (_ : 2 ≤ A.card) (_ : HasNoUniqueRepresentation A), ↑A.card = x}

def Green27.primesAtTop : Filter ℕ

atTop restricted to prime numbers.

Equations

• Green27.primesAtTop = Filter.atTop ⊓ Filter.principal {p : ℕ | Nat.Prime p}

noncomputable def Green27.lowerBest (p : ℕ) : ℝ

Best-known lower bound [Be23, Theorem 3].

Equations

• Green27.lowerBest p = √(Real.log (Real.log (Real.log ↑p))) / Real.log (Real.log (Real.log (Real.log ↑p))) * Real.log ↑p

noncomputable def Green27.upperBest (p : ℕ) : ℝ

Best-known upper bound [Be23, Theorem 5].

Equations

• Green27.upperBest p = Real.log ↑p ^ 2

theorem Green27.green_27.equivalent : Asymptotics.IsEquivalent primesAtTop sorry m

What is the size of the smallest set $A \subset \mathbb{Z} / p\mathbb{Z}$ (with at least two elements) for which no element in the sumset $A + A$ has a unique representation?

theorem Green27.green_27.lower : have ans := sorry; lowerBest =o[primesAtTop] ans ∧ ans =O[primesAtTop] m

Propose a better lower bound along primes.

theorem Green27.green_27.upper : have ans := sorry; ans =o[primesAtTop] upperBest ∧ m =O[primesAtTop] ans

Propose a better upper bound along primes.

theorem Green27.green_27.variants.lower_be23 : ∃ (ω : ℕ → ℝ), Filter.Tendsto ω primesAtTop Filter.atTop ∧ ∀ᶠ (p : ℕ) in primesAtTop, ω p * Real.log ↑p ≤ m p

We have $m(p) \geq \omega(p) \log p$ for some function $\omega(p)$ tending to infinity [Be23, Theorem 3].

theorem Green27.green_27.variants.upper_be23 : m =O[primesAtTop] upperBest

Upper bound: $m(p) \ll (\log p)^2$ [Be23, Theorem 5].

theorem Green27.green_27.variants.previous_lower : (fun (p : ℕ) => Real.log ↑p) =O[primesAtTop] m

Previous best-known lower bound $\log p \ll m(p)$ from [St76].

theorem Green27.green_27.variants.previous_upper : m =O[primesAtTop] fun (p : ℕ) => √↑p

Previous best-known upper bound $m(p) \ll \sqrt{p}$ from [Be23].