Erdős problem 139

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)$ .

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

139.lean

Retained formal statement1 of 1

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)$ .

FormalConjectures/ErdosProblems/139.leanErdos139.erdos_1391 lineExact file

1∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

SolvedStatement only, no proof