Skip to content

Erdős problem 337

Let ANA\subseteq \mathbb{N} be an additive basis (of any finite order) such that A{1,,N}=o(N)\lvert A\cap \{1,\ldots,N\}\rvert=o(N). Is it true that limN(A+A){1,,N}A{1,,N}=? \lim_{N\to \infty}\frac{\lvert (A+A)\cap \{1,\ldots,N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty?

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

337.lean

Retained formal statement1 of 4

Let ANA\subseteq \mathbb{N} be an additive basis (of any finite order) such that A{1,,N}=o(N)\lvert A\cap \{1,\ldots,N\}\rvert=o(N). Is it true that limN(A+A){1,,N}A{1,,N}=? \lim_{N\to \infty}\frac{\lvert (A+A)\cap \{1,\ldots,N\}\rvert} {\lvert A\cap \{1,\ldots,N\}\rvert}=\infty?

The answer is no, and a counterexample was provided by Turjányi [Tu84]. This was generalised (to the replacement of A+AA+A by the hh-fold sumset hAhA for any h2h\geq 2) by Ruzsa and Turjányi [RT85].

"Additive basis" is Set.IsAsymptoticAddBasis: some finite hh has hAhA containing every sufficiently large integer. The exact notion Set.IsAddBasis, which asks that hAhA be all of N\mathbb{N}, would force 0,1A0, 1 \in A 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 xx through x\lfloor x\rfloor, where the counting functions here are indexed by N:NN : \mathbb{N}.

FormalConjectures/ErdosProblems/337.leanErdos337.erdos_3375 linesExact file
False  ∀ (A : Set ℕ),    A.IsAsymptoticAddBasis      ((fun N => ↑(ASet.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) →        Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(ASet.Icc 1 N).ncard) Filter.atTop Filter.atTop
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page