Skip to content

Erdős problem 40

Start work

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 statement1 of 2

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?

FormalConjectures/ErdosProblems/40.leanErdos40.erdos_401 lineExact file
Erdos40.Erdos40ForSet sorry
OpenStatement only, no proof