Erdős Problem 158

References:

• erdosproblems.com/158
• [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.

def B2 (g : ℕ) (A : Set ℕ) : Prop

A set A ⊆ ℕ is said to be a B₂[g] set if for all n, the equation a + a' = n, a ≤ a', a, a' ∈ A has at most g solutions. This is defined in [ESS94].

Equations

• B2 g A = ∀ (n : ℕ), {x : ℕ × ℕ | x.1 + x.2 = n ∧ x.1 ≤ x.2 ∧ x.1 ∈ A ∧ x.2 ∈ A}.encard ≤ ↑g

@[simp]

theorem b2_one {A : Set ℕ} : B2 1 A ↔ IsSidon A

A set is B₂[1] iff it is Sidon.

theorem Erdos158.erdos_158.B22 : sorry ↔ ∀ (A : Set ℕ), A.Infinite → B2 2 A → Filter.liminf (fun (N : ℕ) => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) Filter.atTop = 0

Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

theorem Erdos158.erdos_158.isSidon' {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) : Filter.liminf (fun (N : ℕ) => ENNReal.ofReal (↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2) * Real.log ↑N ^ (1 / 2))) Filter.atTop < ⊤

Let A be an infinite Sidon set. Then liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) * (log N) ^ (1 / 2) < ∞. This is proved in [ESS94].

theorem Erdos158.erdos_158.isSidon {A : Set ℕ} (hAinf : A.Infinite) (hAsid : IsSidon A) : Filter.liminf (fun (N : ℕ) => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) Filter.atTop = 0

As a corollary of erdos_158.isSidon', we can prove that liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0 for any infinite Sidon set A.