Erdős problem 337
Let be an additive basis (of any finite order) such that . Is it true that
Sources
FormalConjectures/ErdosProblems/
337.lean
Retained formal statement
Ruzsa and Turjányi do prove (under the same hypotheses) that and conjecture that the same should be true with in the numerator.
∀ (A : Set ℕ), A.IsAsymptoticAddBasis → ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) → Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 (2 * N)).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTopOpenStatement only, no proof