Erdős Problem 156

References:

• erdosproblems.com/156
• [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.
• [Ru98b] Ruzsa, Imre Z., A small maximal Sidon set. Ramanujan J. (1998), 55-58.

noncomputable def Erdos156.minMaximalSidonSet (N : ℕ) : ℕ

The size of the smallest maximal Sidon set in $\{1, \dots, N\}$.

Equations

• Erdos156.minMaximalSidonSet N = sInf ↑(Finset.image Finset.card ({A ∈ (Finset.Icc 1 N).powerset | (↑A).IsMaximalSidonSetIn N}))

theorem Erdos156.erdos_156 : sorry ↔ (fun (N : ℕ) => ↑(minMaximalSidonSet N)) =O[Filter.atTop] fun (N : ℕ) => ↑N ^ (1 / 3)

Does there exist a maximal Sidon set $A\subset \{1,\ldots,N\}$ of size $O(N^{1/3})$?

A question of Erdős, Sárközy, and Sós [ESS94].

theorem Erdos156.greedySidonSet_isSidon (n : ℕ) : IsSidon ↑(Finset.greedySidonBelow n)

theorem Erdos156.erdos_156.variants.greedy_lower_bound : (fun (N : ℕ) => ↑N ^ (1 / 3)) =O[Filter.atTop] fun (N : ℕ) => ↑(Finset.greedySidonBelow N).card

It is easy to prove that the greedy construction of a maximal Sidon set in $\{1,\ldots,N\}$ has size $\gg N^{1/3}$.

theorem Erdos156.erdos_156.variants.ruzsa_upper_bound : (fun (N : ℕ) => ↑(minMaximalSidonSet N)) =O[Filter.atTop] fun (N : ℕ) => (↑N * Real.log ↑N) ^ (1 / 3)

Ruzsa [Ru98b] constructed a maximal Sidon set of size $\ll (N\log N)^{1/3}$.