/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtil
public import FormalConjectures.ErdosProblems.«28»Erdős Problem 40
Reference: erdosproblems.com/40
@[expose] public sectionopen AdditiveCombinatorics Filter Real Setopen scoped Pointwisenamespace Erdos40The 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$.
def Erdos40For (g : ℕ → ℝ) : Prop :=
∀ A : Set ℕ,
(fun N : ℕ ↦ √N / g N) =O[atTop] (fun N ↦ ((A ∩ .Icc 1 N).ncard : ℝ)) →
limsup (fun N ↦ (sumRep A N : ℕ∞)) atTop = ⊤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$?
@[category research open, AMS 11]
theorem erdos_40 :
{g : ℕ → ℝ | Tendsto g atTop atTop ∧ Erdos40For g} = answer(sorry) := ⊢ {g | Tendsto g atTop atTop ∧ Erdos40For g} = sorry
All goals completed! 🐙Is there any function $g(N) → \infty$ such that $$\lvert A\cap {1,\ldots,N}\rvert \gg \frac{N^{1/2}}{g(N)}$$ implies $\limsup 1_A\ast 1_A(n)=\infty$?
This is a weaker form of Erdős Problem 40, which asks for all such $g$. Establishing the implication for even one $g(N) → \infty$ already answers Erdős Problem 28 positively, because a basis of order $2$ satisfies $\lvert A\cap {1,\ldots,N}\rvert \gg N^{1/2}$.
@[category research open, AMS 11]
theorem erdos_40.variants.weaker :
answer(sorry) ↔ ∃ g : ℕ → ℝ, Tendsto g atTop atTop ∧ Erdos40For g := ⊢ True ↔ ∃ g, Tendsto g atTop atTop ∧ Erdos40For g
All goals completed! 🐙Establishing the property in Erdős Problem 40 for any one function $g(N) → \infty$ implies the Erdős-Turán conjecture, see Erdős Problem 28.
g:ℕ → ℝhg:Tendsto g atTop atToph_erdos_40:Erdos40For gA:Set ℕhA:(A + A)ᶜ.Finiten:ℕhn:∀ i ∈ (A + A)ᶜ, i ≤ nN:ℕhN:2 * n + 2 ≤ NhgN:1 ≤ g Nk:ℕ := (A ∩ Icc 1 N).ncardB:Set ℕ := insert 0 (A ∩ Icc 1 N)hB:B.Finitehmem:∀ a ∈ A, a ≤ N → a ∈ Bhsub:Icc (n + 1) N ⊆ B + Bhcard:N - n ≤ (k + 1) ^ 2hcard':N ≤ n + (k + 1) ^ 2hk:1 ≤ khcardR:↑N ≤ ↑n + (↑k + 1) ^ 2hNR:2 * ↑n + 2 ≤ ↑NhkR:1 ≤ ↑khsqrt:√↑N ≤ 4 * ↑k⊢ √↑N / g N ≤ 4 * ↑(A ∩ Icc 1 N).ncard
All goals completed! 🐙end Erdos40