Skip to content

Erdős problem 40

For what functions g(N)→∞g(N) → \infty is it true that ∣A∩{1,…,N}∣≫N1/2g(N)\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)} implies lim sup⁡1A∗1A(n)=∞\limsup 1_A\ast 1_A(n)=\infty?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

40.lean

Retained formal statement2 of 2

If we don't pose additional conditions on the functions, then this is a stronger form of the Erdős-Turán conjecture, see Erdõs Problem 28, (since establishing this for any function g(N)→∞g(N) → \infty would imply a positive solution to Erdős Problem 28).

FormalConjectures/ErdosProblems/40.leanErdos40.erdos_40.variants.implies_erdos_282 linesExact file
Erdos40.Erdos40ForSet Set.univ →  ∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤
TextbookStatement only, no proof