Skip to content

Erdős problem 899

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}∣=∞? \limsup_{N\to\infty}\frac{|(A - A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} = \infty?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

899.lean

Retained formal statement1 of 1

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}∣=∞? \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+AA+A}\ and {A−AA-A}_. (1978), 933--938.

FormalConjectures/ErdosProblems/899.leanErdos899.erdos_8995 linesExact file
True ↔  ∀ (A : Set ℕ),    A.Infinite →      Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) →        Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤
SolvedStatement only, no proof