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 statement5 of 10

This is sharp, as Chen and Fang [ChFa11] also proved that there exist such $A$ and $B$ with $\limsup_{x\to \infty}\frac{A(x)B(x)}{x}=\frac{3}{2}$ for which $A(x)B(x)-x=1$ for infinitely many $x$ .

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

1∃ A B,2  A.Infinite ∧3    B.Infinite ∧4      IsAdditiveComplement A B ∧5        Filter.limsup (fun x => ↑(↑(Erdos785.counting A x) * ↑(Erdos785.counting B x)) / ↑↑x) Filter.atTop = ↑(3 / 2) ∧6          ∃ᶠ (x : ℕ) in Filter.atTop, ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x = 1

SolvedStatement only, no proof

Sources

Search problems.science