Skip to content

Erdős problem 785

Start work

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

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

785.lean

Retained formal statement4 of 10

Chen and Fang [ChFa10] proved the stronger statement that A(x)B(x)−x→∞A(x)B(x)-x\to \infty if AA and BB are infinite sets such that A+BA+B contains all large integers and lim sup⁡x→∞A(x)B(x)x<54.\limsup_{x\to \infty}\frac{A(x)B(x)}{x}<\frac{5}{4}. They later [ChFa14] improved 5/45/4 to 3−3≈1.2683-\sqrt{3}\approx 1.268.

FormalConjectures/ErdosProblems/785.leanErdos785.erdos_785.variants.chen_fang_limsup6 linesExact file
∀ (A B : Set ℕ),  A.Infinite →    B.Infinite →      IsAdditiveComplement A B →        Filter.limsup (fun x => ↑(↑(Erdos785.counting A x) * ↑(Erdos785.counting B x)) / ↑↑x) Filter.atTop < ↑(3 - √3) →          Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop
SolvedStatement only, no proof