Erdős Problem 899

Reference: erdosproblems.com/899

theorem Erdos899.erdos_899 : True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun (N : ℕ) => ↑((A - A).interIcc 1 N).ncard / ↑(A.interIcc 1 N).ncard) Filter.atTop = ⊤

Let $A\subseteq\mathbb{N}$ be an infinite set such that $|A\cap \{1, ..., N\}| = o(N)$. Is it true that $$ \limsup_{N\to\infty}\frac{|(A - A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} = \infty? $$

The answer is yes, proved by Ruzsa [Ru78].

[Ru78] Ruzsa, I. Z., On the cardinality of {$A+A$}\ and {$A-A$}. (1978), 933--938.