Erdős Problem 153

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

References:

• erdosproblems.com/153
• [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 Erdos153.f (n : ℕ) : ℝ

Define f n to be the minimum of ∑ (i : Set.Ico 1 ((A + A).card), (s i - s (i - 1)) ^ 2 / n as A ranges over all Sidon sets of size n, where s is an order embedding from Fin n into A.

Equations

• Erdos153.f n = ⨅ (A : ↑{A : Finset ℕ | A.card = n ∧ IsSidon A}), have s := (↑A + ↑A).orderIsoOfFin ⋯; ∑ i : ↑(Set.Ico 1 (↑A + ↑A).card), (↑↑(s ⟨↑i, ⋯⟩) - ↑↑(s ⟨↑i - 1, ⋯⟩)) ^ 2 / ↑n

theorem Erdos153.erdos_153 : sorry ↔ Filter.Tendsto f Filter.atTop Filter.atTop

Must lim f n = ∞?