Erdős Problem 152

#TODO: Formalize the corresponding conjecture for infinite Sidon sets.

References:

• erdosproblems.com/152
• [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.

noncomputable def Erdos152.f (n : ℕ) : ℕ

Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n.

Equations

• Erdos152.f n = ⨅ (A : ↑{A : Set ℕ | A.ncard = n ∧ IsSidon A}), {s : ℕ | s - 1 ∉ ↑A + ↑A ∧ s ∈ ↑A + ↑A ∧ s + 1 ∉ ↑A + ↑A}.ncard

theorem Erdos152.erdos_152 : sorry ↔ Filter.Tendsto f Filter.atTop Filter.atTop

Must lim f n = ∞?

theorem Erdos152.erdos_152.square : sorry ↔ (fun (n : ℕ) => ↑n ^ 2) =O[Filter.atTop] fun (n : ℕ) => ↑(f n)

Must f n ≫ n ^ 2?