Erdős Problem 30

Reference: erdosproblems.com/30

@[reducible, inline]

noncomputable abbrev h (N : ℕ) : ℕ

Let $h(N)$ be the maximum size of a Sidon set in $\{1, \dots, N\}$.

Equations

• h N = (Finset.Icc 1 N).maxSidonSubsetCard

theorem erdos_30 : (∀ ε > 0, (fun (N : ℕ) => ↑(h N) - √↑N) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ ε) ↔ sorry

Is it true that, for every $\varepsilon > 0$, $h(N) = \sqrt N + O_{\varespilon}(N^\varespilon)