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 $\frac{1}{t}\sum_{1\leq i<t}(s_{i+1}-s_i)^2$ as $A$ ranges over all Sidon sets of size $n$, where $A+A=\{s_1<\cdots<s_t\}$.

Equations

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

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

Let $A$ be a finite Sidon set and $A+A=\{s_1<\cdots<s_t\}$. Is it true that $$\frac{1}{t}\sum_{1\leq i<t}(s_{i+1}-s_i)^2 \to \infty$$ as $\lvert A\rvert\to \infty$?