Erdős problem 43
If Sidon sets satisfy , must , where is the largest Sidon-set size in - and can the bound be improved by a fixed proportion when ?
Sources
FormalConjectures/ErdosProblems/
43.lean
Retained formal statement
If and are equal-sized Sidon sets in with , can the bound be improved to for some constant ?
The answer is no; the Erdős Problems page records a negative answer due to Barreto.
False ↔ ∃ c > 0, ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A B : Finset ℕ), A ⊆ Finset.Icc 1 N → B ⊆ Finset.Icc 1 N → IsSidon ↑A → IsSidon ↑B → A.card = B.card → (A - A) ∩ (B - B) = {0} → ↑(A.card.choose 2 + B.card.choose 2) ≤ (1 - c + o N) * ↑((Erdos43.f N).choose 2)SolvedStatement only, no proof