Erdős Problem 245

Reference: erdosproblems.com/245

theorem erdos_245 : (∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun (N : ℕ) => ↑(Set.bdd✝ A N).ncard / ↑N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun (N : ℕ) => ↑(Set.bdd✝ (A + A) N).ncard / ↑(Set.bdd✝ A N).ncard) Filter.atTop) ↔ True

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 erdos_245.variants.exists_limit (A : Set ℕ) (h_inf : A.Infinite) (hf : Filter.Tendsto (fun (N : ℕ) => ↑(Set.bdd✝ A N).ncard / ↑N) Filter.atTop (nhds 0)) : ∃ (α : EReal), Filter.Tendsto (fun (N : ℕ) => ↑(Set.bdd✝ (A + A) N).ncard / ↑(Set.bdd✝ A N).ncard) Filter.atTop (nhds α)

Let $A\subseteq\mathbb{N}$ be an infinite set such that $|A\cap \{1, ..., N\}| = o(N)$. Determine whether there exists a limit to $$ \frac{|(A + A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} $$ as $N\to\infty$.

theorem erdos_245.variants.two (A : Set ℕ) (h_inf : A.Infinite) (hf : Filter.Tendsto (fun (N : ℕ) => ↑(Set.bdd✝ A N).ncard / ↑N) Filter.atTop (nhds 0)) : 2 ≤ Filter.limsup (fun (N : ℕ) => ↑(Set.bdd✝ (A + A) N).ncard / ↑(Set.bdd✝ A 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. $$