Erdős problem 40 · problems.science

For what functions $g(N) → \infty$ is it true that $\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}$ implies $\limsup 1_A\ast 1_A(n)=\infty$ ?

Sources

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

2 retained statements2415f78e850a

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) → \infty$ would imply a positive solution to Erdős Problem 28).

FormalConjectures/ErdosProblems/40.leanErdos40.erdos_40.variants.implies_erdos_282 linesExact file

1Erdos40.Erdos40ForSet Set.univ →2  ∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

TextbookStatement only, no proof

Sources

Search problems.science