Erdős Problem 40

Reference: erdosproblems.com/40

def Erdos40.Erdos40For (g : ℕ → ℝ) : Prop

The predicate for a function $g\colon\mathbb{N} → \mathbb{R})$ that $$\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}$$ implies $\limsup 1_A\ast 1_A(n)=\infty$.

Equations

• One or more equations did not get rendered due to their size.

def Erdos40.Erdos40 (G : (ℕ → ℝ) → Prop) : Prop

Given a set of functions $\mathbb{N} → \mathbb{R})$, we assert that for all $g$ in that set, if $g(N) → \infty$ then $$\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}$$ implies $\limsup 1_A\ast 1_A(n)=\infty$.

Equations

• Erdos40.Erdos40 G = ∀ (g : ℕ → ℝ), G g → Filter.Tendsto g Filter.atTop Filter.atTop → Erdos40.Erdos40For g

theorem Erdos40.erdos_40 : Erdos40 sorry

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$?

theorem Erdos40.erdos_28_of_erdos_40 (h_erdos_40 : Erdos40 fun (x : ℕ → ℝ) => True) (A : Set ℕ) (h : (A + A)ᶜ.Finite) : Filter.limsup (fun (n : ℕ) => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

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).