Documentation

FormalConjectures.ErdosProblems.«899»

Erdős Problem 899 #

Reference: erdosproblems.com/899

def Set.bdd (A : Set ) (N : ) :

If A is a set of natural numbers and N : ℕ, then bdd A N is the set { n ∈ A | 1 ≤ n ≤ N }.

Equations
Instances For
    theorem erdos_899 :
    (∀ (A : Set ), A.InfiniteFilter.Tendsto (fun (N : ) => (A.bdd N).ncard / N) Filter.atTop (nhds 0)Filter.Tendsto (fun (N : ) => ((A - A).bdd N).ncard / (A.bdd N).ncard) Filter.atTop 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\}|} = \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.