Erdős Problem 44: Extending Sidon Sets

Reference: erdosproblems.com/44

theorem Erdos44.maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) : ↑(Finset.Icc 1 N).maxSidonSubsetCard ≤ 2 * √↑N

The maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.

theorem Erdos44.erdos_44 : (∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (A ∪ B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card) ↔ sorry

Erdős Problem 44: Let N ≥ 1 and A ⊆ {1,…,N} be a Sidon set. Is it true that, for any ε > 0, there exist M = M(ε) and B ⊆ {N+1,…,M} such that A ∪ B ⊆ {1,…,M} is a Sidon set of size at least (1−ε)M^{1/2}?

This problem asks whether any Sidon set can be extended to achieve a density arbitrarily close to the optimal density for Sidon sets.

theorem Erdos44.erdos_44.variant : (∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon A → ∀ ε > 0, ∀ M ≥ N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (A ∪ B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card) ↔ sorry

A variant considering the extension to any larger range.

theorem Erdos44.erdos_44.empty_start : (∀ ε > 0, ∃ (M : ℕ), ∃ A ⊆ Finset.Icc 1 M, IsSidon A ∧ (1 - ε) * √↑M ≤ ↑A.card) ↔ sorry

The case where we start with an empty set (constructing large Sidon sets).

theorem Erdos44.erdos_44.constructive : (∃ (f : ℝ → ℕ), ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon A → ∀ ε > 0, ∃ M ≤ f ε, ∃ B ⊆ Finset.Icc (N + 1) M, N < M ∧ IsSidon (A ∪ B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card) ↔ sorry

A constructive version asking for explicit bounds on M in terms of ε.

Related results and examples

theorem Erdos44.example_sidon_set : IsSidon {1, 2, 4, 8, 13}

The set {1, 2, 4, 8, 13} is a Sidon set in {1, ..., 13}.

theorem Erdos44.sidon_set_lower_bound (N : ℕ) (hN : 1 ≤ N) : ∃ A ⊆ Finset.Icc 1 N, IsSidon A ∧ N.sqrt / 2 ≤ A.card

For any N, there exists a Sidon set of size at least √N/2.

theorem Erdos44.greedy_sidon_construction (N : ℕ) (hN : 1 ≤ N) : ∃ A ⊆ Finset.Icc 1 N, IsSidon A ∧ A.card ≥ N.sqrt

The greedy construction gives a Sidon set of size approximately √N.