Documentation

FormalConjectures.ErdosProblems.«139»

Erdős Problem 139 #

Reference: erdosproblems.com/139

source
theorem Erdos139.erdos_139 (k : ℕ) (hk : 1 ≤ k) :
Filter.Tendsto (fun (N : ℕ) => ↑(Erdos139.r✝ k N) / ↑N) Filter.atTop (nhds 0)

Erdős Problem 139: Let $r_k(N)$ be the size of the largest subset of ${1,...,N}$ which does not contain a non-trivial $k$-term arithmetic progression. Prove that $r_k(N) = o(N)$.