Green's Open Problem 51

References:

• [Gr24] Green's Open Problems
• [Gr13] B. J. Green, Restriction and Kakeya phenomena, notes from a 2003 course. Available at http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf
• [Sa11] Sanders, Tom. "Green's sumset problem at density one half." Acta Arithmetica 146.1 (2011): 91-101.
• [Gr02] Green, Ben. "Arithmetic progressions in sumsets." Geometric & Functional Analysis GAFA 12.3 (2002): 584-597.
• [Ruz91] Ruzsa, Imre Z. "Arithmetic progressions in sumsets." Acta Arithmetica 60.2 (1991): 191-202.

noncomputable def Green51.guaranteedMaxCosetDim (n : ℕ) (α : ℝ) : ℕ

The largest dimension of a coset guaranteed to be contained in $2A$ for $A \subseteq \mathbb{F}_2^n$ with density $\alpha$.

Equations

• Green51.guaranteedMaxCosetDim n α = sInf {x : ℕ | ∃ (A : Finset (𝔽₂ n)) (_ : ↑A.dens ≥ α), maxCosetDim (ZMod 2) (𝔽₂ n) ↑(A + A) = x}

theorem Green51.green_51 : sorry = guaranteedMaxCosetDim

Suppose that $A \subset \mathbb{F}_2^n$ is a set of density $\alpha$. What is the largest size of coset guaranteed to be contained in $2A$?

We phrase this by asking for the exact function $F(\alpha, n)$ giving the maximum dimension of a guaranteed coset.

theorem Green51.green_51.lower (α : ℝ) : 0 < α → α ≤ 1 → ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, c * ↑n ≤ ↑(guaranteedMaxCosetDim n α)

It is known that $A + A$ must contain a coset of dimension $\gg_\alpha n$ [Gr13].

theorem Green51.green_51.upper : ∃ α > 0, α ≤ 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(guaranteedMaxCosetDim n α) < ↑n - √↑n

It is known that $A + A$ need not contain a coset of dimension $n - \sqrt{n}$ [Gr13].

theorem Green51.green_51.one_half : sorry ↔ ∀ (k : ℝ), 0 < k → ∃ (c : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ α > 1 / 2 - k / √↑n, α ≤ 1 → n ≤ guaranteedMaxCosetDim n α + c

Suppose that $A \subset \mathbb{F}_2^n$ has density $\alpha > 1/2 - C/\sqrt{n}$. Does $A + A$ contain a subspace of co-dimension $O_C(1)$? [Sa11, Question 5.1]

noncomputable def Green51.guaranteedMaxAPLength (N : ℕ) (α : ℝ) : ℕ

The largest length of an arithmetic progression guaranteed to be contained in $A+A$ for $A \subseteq \{1, \dots, N\}$ with density $\alpha$.

Equations

• Green51.guaranteedMaxAPLength N α = sInf {x : ℕ | ∃ (A : Finset ℕ) (_ : A ⊆ Finset.Icc 1 N) (_ : α * ↑N ≤ ↑A.card), sSup {l : ℕ | ∃ s ⊆ ↑A + ↑A, s.IsAPOfLength ↑l} = x}

theorem Green51.green_51.lower_ap (α : ℝ) : 0 < α → α ≤ 1 → ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, Real.exp (c * Real.log ↑N ^ (1 / 2)) ≤ ↑(guaranteedMaxAPLength N α)

It is known that $A + A$ must contain an arithmetic progression of length $\sim \exp(c (\log N)^{1/2})$ [Gr02].

theorem Green51.green_51.upper_ap (α : ℝ) : 0 < α → α < 1 / 2 → ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(guaranteedMaxAPLength N α) ≤ Real.exp (c * Real.log ↑N ^ (2 / 3))

It is known that $A + A$ need not contain an arithmetic progression of length $\sim \exp(c (\log N)^{2/3})$ [Ruz91].