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

Narkiewicz [Na59] proved that, under the given assumptions (and perhaps swapping AA and BB) we must have A(2x)/A(x)→1A(2x)/A(x)\to 1 and B(2x)/B(x)→2B(2x)/B(x)\to 2.

FormalConjectures/ErdosProblems/785.leanErdos785.erdos_785.variants.narkiewicz8 linesExact file
∀ (A B : Set ℕ),  A.Infinite →    B.Infinite →      Erdos785.IsExactAdditiveComplement A B →        Filter.Tendsto (fun x => ↑(Erdos785.counting A (2 * x)) / ↑(Erdos785.counting A x)) Filter.atTop (nhds 1) ∧            Filter.Tendsto (fun x => ↑(Erdos785.counting B (2 * x)) / ↑(Erdos785.counting B x)) Filter.atTop (nhds 2) ∨          Filter.Tendsto (fun x => ↑(Erdos785.counting B (2 * x)) / ↑(Erdos785.counting B x)) Filter.atTop (nhds 1) ∧            Filter.Tendsto (fun x => ↑(Erdos785.counting A (2 * x)) / ↑(Erdos785.counting A x)) Filter.atTop (nhds 2)
SolvedStatement only, no proof