Erdős problem 785 · problems.science

Let $A,B\subseteq \mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\lvert A\cap [1,x]\rvert$ and similarly for $B(x)$ . Is it true that if $A(x)B(x)\sim x$ then $A(x)B(x)-x\to \infty$ as $x\to \infty$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

10 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

785.lean

Retained formal statement8 of 10

Ruzsa [Ru17] proves that, if $a^*(x)=\max A \cap [1,x]$ and $A$ and $B$ satisfy the conditions in the problem then (after possibly changing the roles of $A$ and $B$ ) $A(x)B(x)-x > (1-o(1))\frac{a^*(x)}{A(x)}.$

FormalConjectures/ErdosProblems/785.leanErdos785.erdos_785.variants.ruzsa_lower_bound12 linesExact file

1∀ (A B : Set ℕ),2  A.Infinite →3    B.Infinite →4      Erdos785.IsExactAdditiveComplement A B →5        (∀ ε > 0,6            ∀ᶠ (x : ℕ) in Filter.atTop,7              (1 - ε) * ↑(Erdos785.aStar A x) / ↑(Erdos785.counting A x) <8                ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) ∨9          ∀ ε > 0,10            ∀ᶠ (x : ℕ) in Filter.atTop,11              (1 - ε) * ↑(Erdos785.aStar B x) / ↑(Erdos785.counting B x) <12                ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x

SolvedStatement only, no proof

Sources

Search problems.science