Erdős Problem 245

Reference: erdosproblems.com/245

theorem Erdos245.erdos_245 : True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun (N : ℝ) => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun (N : ℝ) => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 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\}|} \geq 3? $$

The answer is yes, proved by Freiman [Fr73].

[Fr73] Fre\u{\i}man, G. A., Foundations of a structural theory of set addition. (1973), vii+108.

theorem Erdos245.erdos_245.variants.two (A : Set ℕ) (h_inf : A.Infinite) (hf : Filter.Tendsto (fun (N : ℝ) => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0)) : 2 ≤ Filter.limsup (fun (N : ℝ) => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTop

Let $A\subseteq\mathbb{N}$ be an infinite set such that $|A\cap \{1, ..., N\}| = o(N)$. Then $$ \limsup_{N\to\infty}\frac{|(A + A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} \geq 2. $$