Documentation

FormalConjectures.ErdosProblems.«42»

Erdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets #

Reference: erdosproblems.com/42

This problem asks whether maximal Sidon sets can coexist with other Sidon sets that have disjoint difference sets (apart from 0).

source
theorem Erdos42.erdos_42 :
(∀ M ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}) ↔ sorry

Erdős Problem 42: Let M ≥ 1 and N be sufficiently large in terms of M. Is it true that for every maximal Sidon set A ⊆ {1,…,N} there is another Sidon set B ⊆ {1,…,N} of size M such that (A - A) ∩ (B - B) = {0}?

source
theorem Erdos42.erdos_42.constructive :
(∃ (f : ℕ → ℕ), ∀ (M N : ℕ), 1 ≤ M → f M ≤ N → ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}) ↔ sorry

A variant asking for explicit bounds on how large N needs to be in terms of M.

This version provides a constructive function f such that for all M ≥ 1 and N ≥ f(M), every maximal Sidon set A ⊆ {1,…,N} has another Sidon set B ⊆ {1,…,N} of size M with disjoint difference sets (apart from 0).

source
theorem Erdos42.example_maximal_sidon :
{1, 2, 4}.IsMaximalSidonSetIn 4

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

source
theorem Erdos42.example_difference_set :
{1, 2, 4} - {1, 2, 4} = {0, 1, 2, 3}

The difference set of {1, 2, 4} is {0, 1, 2, 3}.

source
theorem Erdos42.maximal_sidon_contains_zero (A : Set ℕ) (N : ℕ) (hN : 1 ≤ N) (hA : A.IsMaximalSidonSetIn N) :
0 ∈ A - A

For any maximal Sidon set, the difference set contains 0.