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 Sidon sets in with , is it true that
The answer is no; the Erdős Problems page notes that this follows from the solution to Erdős Problem 42.
False ↔ ∃ C, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A B : Finset ℕ), A ⊆ Finset.Icc 1 N → B ⊆ Finset.Icc 1 N → IsSidon ↑A → IsSidon ↑B → (A - A) ∩ (B - B) = {0} → ↑(A.card.choose 2 + B.card.choose 2) ≤ ↑((Erdos43.f N).choose 2) + CSolvedStatement only, no proof