Skip to content

Erdős problem 245

Let A⊆NA\subseteq\mathbb{N} be an infinite set such that ∣A∩{1,...,N}∣=o(N)|A\cap \{1, ..., N\}| = o(N). Is it true that lim sup⁡N→∞∣(A+A)∩{1,...,N}∣∣A∩{1,...,N}∣≥3? \limsup_{N\to\infty}\frac{|(A + A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} \geq 3?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

245.lean

Retained formal statement1 of 2

Let A⊆NA\subseteq\mathbb{N} be an infinite set such that ∣A∩{1,...,N}∣=o(N)|A\cap \{1, ..., N\}| = o(N). Is it true that lim sup⁡N→∞∣(A+A)∩{1,...,N}∣∣A∩{1,...,N}∣≥3? \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.

FormalConjectures/ErdosProblems/245.leanErdos245.erdos_2455 linesExact file
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
SolvedStatement only, no proof