Green's Open Problem 9

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [BlSi20] Bloom, Thomas F., and Olof Sisask. "Breaking the logarithmic barrier in Roth's theorem on arithmetic progressions." arXiv preprint arXiv:2007.03528 (2020).

noncomputable def Green9.r (k N : ℕ) : ℕ

The quantity $r_k(N)$, defined as the size of the largest subset of $\{1, \dots, N\}$ without non-trivial $k$-term arithmetic progressions.

Equations

• Green9.r k N = Finset.maxAPFreeCard k (Finset.Icc 1 N)

theorem Green9.green_9_i : (fun (N : ℕ) => ↑(r 3 N)) =O[Filter.atTop] fun (N : ℕ) => ↑N * Real.log ↑N ^ (-10)

Problem 9 (i): is $r_3(N) \ll N(\log N)^{-10}$?

Solved in [BlSi20].

theorem Green9.green_9_ii : sorry ↔ ∃ c > 0, (fun (N : ℕ) => ↑(r 5 N)) =O[Filter.atTop] fun (N : ℕ) => ↑N * Real.log ↑N ^ (-c)

Problem 9 (ii): is $r_5(N) \ll N(\log N)^{-c}$?

theorem Green9.green_9_iii : sorry ↔ ∃ c > 0, (fun (n : ℕ) => ↑(Finset.maxAPFreeCard 4 Finset.univ)) =O[Filter.atTop] fun (n : ℕ) => (5 ^ n) ^ (1 - c)

Problem 9 (iii): is $r_4(\mathbf{F}_5^n) \ll N^{1-c}$, where $N=5^n$?