Erdős Problem 142

Reference: erdosproblems.com/142

theorem Erdos142.erdos_142 (k : ℕ) : (fun (N : ℕ) => ↑(Erdos142.r✝ k N)) =Θ[Filter.atTop] sorry

Prove an asymptotic formula for $r_k(N)$, the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression.

theorem Erdos142.erdos_142.variants.lower (k : ℕ) : (fun (N : ℕ) => ↑(Erdos142.r✝ k N)) =o[Filter.atTop] fun (N : ℕ) => ↑N / Real.log ↑N

Show that $r_k(N)=o_k(N/\log N)$, where $r_k(N)$ the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression.

theorem Erdos142.erdos_142.variants.upper (k : ℕ) : (fun (N : ℕ) => ↑(Erdos142.r✝ k N)) =O[Filter.atTop] sorry

Find functions $f_k$, such that $r_k(N)=O_k(f_k)$, where $r_k(N)$ the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression.

theorem Erdos142.erdos_142.variants.three : (fun (N : ℕ) => ↑(Erdos142.r✝ 3 N)) =Θ[Filter.atTop] sorry

Prove an asymptotic formula for $r_3(N)$, the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $3$-term arithmetic progression.