Ben Green's Open Problem 16

References:

• Ben Green's Open Problem 16
• [Ruzsa](I. Z. Ruzsa, Solving a linear equation in a set of integers. I. Acta Arith. 65 (1993), no. 3, 259–282.)
• [Schoen and Sisask](T. Schoen and O. Sisask, Roth’s theorem for four variables and additive structures in sums of sparse sets Forum of Mathematics, Sigma (2016), Vol. 4, e5, 28 pages.)
• [Yufei Zhao](Via Personal Communication with Ben Green)

def Green16.SolutionFree (A : Finset ℕ) : Prop

A set has no solution to $x + 3y = 2z + 2w$ in distinct elements.

Equations

• Green16.SolutionFree A = ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, ∀ w ∈ A, [x, y, z, w].Nodup → x + 3 * y ≠ 2 * z + 2 * w

noncomputable def Green16.f (N : ℕ) : ℕ

The maximum size of a solution-free subset of $[N]$.

Equations

• Green16.f N = sSup {k : ℕ | ∃ A ⊆ Finset.range (N + 1), Green16.SolutionFree A ∧ A.card = k}

theorem Green16.green_16 (N : ℕ) : ∃ A ⊆ Finset.range (N + 1), SolutionFree A ∧ A.card = sorry ∧ MaximalFor (fun (B : Finset ℕ) => B ⊆ Finset.range (N + 1) ∧ SolutionFree B) Finset.card A

What is the largest subset of $[N]$ with no solution to $x + 3y = 2z + 2w$ in distinct integers $x, y, z, w$?

theorem Green16.green_16_lower_bound : (fun (N : ℕ) => ↑N ^ (1 / 2)) =O[Filter.atTop] fun (N : ℕ) => ↑(f N)

From [Ruzsa] $f(N) \gg N^{1/2}$.

theorem Green16.green_16_upper_bound : ∃ c > 0, (fun (N : ℕ) => ↑(f N)) =O[Filter.atTop] fun (N : ℕ) => ↑N * Real.exp (-c * Real.log ↑N ^ (1 / 7))

From [Schoen and Sisask] $f(N) \ll N \cdot e^{-c(\log N)^{1/7}}$.

theorem Green16.green_16_conjectured_lower_bound : ∃ c > 0, (fun (N : ℕ) => ↑N * Real.exp (-c * Real.log ↑N ^ (1 / 7))) =O[Filter.atTop] fun (N : ℕ) => ↑(f N)

$f(N) \gg N \cdot e^{-c(\log N)^{1/7}}$.

def Green16.ZhaoSolutionFree (A : Finset ℕ) : Prop

A set has no nontrivial solution to $x + 2y + 3z = x' + 2y' + 3z'$.

Equations

• Green16.ZhaoSolutionFree A = ∀ (x y z x' y' z' : ℕ), x ∈ A → y ∈ A → z ∈ A → x' ∈ A → y' ∈ A → z' ∈ A → x + 2 * y + 3 * z = x' + 2 * y' + 3 * z' → x = x' ∧ y = y' ∧ z = z'

noncomputable def Green16.g (N : ℕ) : ℕ

The maximum size of a Zhao-solution-free subset of $[N]$.

Equations

• Green16.g N = sSup {k : ℕ | ∃ A ⊆ Finset.range (N + 1), Green16.ZhaoSolutionFree A ∧ A.card = k}

theorem Green16.zhao_question : ∃ (h : ℕ → ℝ), Filter.Tendsto h Filter.atTop (nhds 0) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(g N) ≥ ↑N ^ (1 / 3 - h N)

From [Yufei Zhao]: Is there a subset of $\{1, \ldots, N\}$ of size $N^{1/3 - o(1)}$ with no nontrivial solutions to $x + 2y + 3z = x' + 2y' + 3z'$?