Erdős problem 337
Let be an additive basis (of any finite order) such that . Is it true that
Sources
FormalConjectures/ErdosProblems/
337.lean
Let be an additive basis (of any finite order) such that . Is it true that
The answer is no, and a counterexample was provided by Turjányi [Tu84]. This was generalised (to the replacement of by the -fold sumset for any ) by Ruzsa and Turjányi [RT85].
"Additive basis" is Set.IsAsymptoticAddBasis: some finite has containing every sufficiently large integer. The exact notion Set.IsAddBasis, which asks that be all of , would force and is not the class these results are about.
The linked file states the basis hypothesis as ∃ N₀, Set.Ici N₀ ⊆ iterated_sumset A k and indexes both counting functions by a real through , where the counting functions here are indexed by .
False ↔ ∀ (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 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTop