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

Ruzsa [Ru17] proves that, if a∗(x)=max⁡A∩[1,x]a^*(x)=\max A \cap [1,x] and AA and BB satisfy the conditions in the problem then (after possibly changing the roles of AA and BB) A(x)B(x)−x>(1−o(1))a∗(x)A(x).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
∀ (A B : Set ℕ),  A.Infinite →    B.Infinite →      Erdos785.IsExactAdditiveComplement A B →        (∀ ε > 0,            ∀ᶠ (x : ℕ) in Filter.atTop,              (1 - ε) * ↑(Erdos785.aStar A x) / ↑(Erdos785.counting A x) <                ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) ∨          ∀ ε > 0,            ∀ᶠ (x : ℕ) in Filter.atTop,              (1 - ε) * ↑(Erdos785.aStar B x) / ↑(Erdos785.counting B x) <                ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x
SolvedStatement only, no proof