Ben Green's Open Problem 2

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [Er65] P. Erdős. Extremal problems in number theory, In Proc. Sympos. Pure Math., Vol. VIII, pages 181–189. Amer. Math. Soc., Providence, R.I., 1965.
• [Sa21] Sanders, Tom. "The Erdős–Moser Sum-free Set Problem." Canadian Journal of Mathematics 73.1 (2021): 63-107.
• [Ru05] I. Z. Ruzsa, Sum-avoiding subsets. Ramanujan J., 9 (2005) (1-2):77–82.
• [Ch71] S. L. G. Choi. On a combinatorial problem in number theory. Proc. London Math. Soc. (3), 23:629–642, 1971. doi:10.1112/plms/s3-23.4.629.
• [BSS00] A. Baltz, T. Schoen, and A. Srivastav. Probabilistic construction of small strongly sum-free sets via large Sidon sets. Colloq. Math., 86(2):171–176, 2000. doi:10.4064/cm-86-2-171-176.

def Green2.restrictedSumset (S : Finset ℤ) : Finset ℤ

The restricted sumset of a set $S$, denoted $S \hat{+} S$, is the set $\lbrace s_1 + s_2 : s_1, s_2 \in S, s_1 \neq s_2 \rbrace$.

Equations

• Green2.restrictedSumset S = Finset.image (fun (p : ℤ × ℤ) => p.1 + p.2) S.offDiag

def Green2.maxRestrictedSumAvoidingSubsetSize (A : Finset ℤ) : ℕ

We define the construction from [Sa21, p1] as $M(A) := \max \{|S| : S \subseteq A \text{ and } (S \hat{+} S) \cap A = \varnothing \}$.

Equations

• Green2.maxRestrictedSumAvoidingSubsetSize A = {S ∈ A.powerset | Disjoint (Green2.restrictedSumset S) A}.sup Finset.card

theorem Green2.green_2 : sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset ℤ), A.card = n → ↑(maxRestrictedSumAvoidingSubsetSize A) ≥ Real.log ↑n ^ 100

Let $A \subset \mathbf{Z}$ be a set of $n$ integers. Is there a set $S \subset A$ of size $(\log n)^{100}$ such that the restricted sumset$S \hat{+} S$ is disjoint from $A$?

theorem Green2.green_2_lower_bound_sanders : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset ℤ), A.card = n → ↑(maxRestrictedSumAvoidingSubsetSize A) ≥ Real.log ↑n ^ (1 + c)

From [Sa21] it is known that there is always such an S with $|S| \gt (\log |A|)^{1+c}$.

theorem Green2.green_2_upper_bound_erdos : ∃ (C : ℝ), ∀ (A : Finset ℤ), ↑(maxRestrictedSumAvoidingSubsetSize A) ≤ ↑A.card / 3 + C

From [Er65] it is known that $M(A) \le \frac{1}{3}|A| + O(1)$.

theorem Green2.green_2_upper_bound_choi : ∃ (o : ℕ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), ∀ (A : Finset ℤ), ↑(maxRestrictedSumAvoidingSubsetSize A) ≤ ↑A.card ^ (2 / 5 + o A.card)

From [Ch71] it is known that $M(A) \le |A|^{2/5 + o(1)}$.

theorem Green2.green_2_upper_bound_ruzsa : ∃ C > 0, ∀ (A : Finset ℤ), ↑(maxRestrictedSumAvoidingSubsetSize A) < Real.exp (C * √(Real.log ↑A.card))

From [Ru05] the best-known upper bound is $|S| \lt e^{C \sqrt{\log |A|}}$.