Erdős Problem 142

Reference: erdosproblems.com/142

@[reducible, inline]

noncomputable abbrev Erdos142.r (k N : ℕ) : ℕ

Equations

• Erdos142.r = Set.IsAPOfLengthFree.maxCard

theorem Erdos142.erdos_142 (k : ℕ) : (fun (N : ℕ) => ↑(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 : ℕ) (hk : 1 < k) : (fun (N : ℕ) => ↑(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 : ℕ) => ↑(r k N)) ≪ 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 : ℕ) => ↑(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.