Erdős Problem 329: Maximum Density of Sidon Sets

Reference: erdosproblems.com/329

noncomputable def Erdos329.sqrtPartialDensity (A : Set ℕ) (N : ℕ) : ℝ

The partial density of a Sidon set A up to N, normalized by dividing by √N instead of N. This measures how close the set comes to the optimal density for Sidon sets.

Equations

• Erdos329.sqrtPartialDensity A N = ↑(A ∩ Set.Icc 1 N).ncard / √↑N

noncomputable def Erdos329.sidonUpperDensity (A : Set ℕ) : ℝ

The upper density of a Sidon set A, normalized by √N.

Equations

• Erdos329.sidonUpperDensity A = Filter.limsup (fun (N : ℕ) => Erdos329.sqrtPartialDensity A N) Filter.atTop

theorem Erdos329.erdos_329 : sSup {x : ℝ | ∃ (A : Set ℕ) (_ : IsSidon A), sidonUpperDensity A = x} = sorry

Erdős Problem 329. Let A ⊆ ℕ be a Sidon set. How large can lim sup_{N → ∞} |A ∩ {1,…,N}| / N^{1/2} be?

theorem Erdos329.erdos_329.lower_bound : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A ≥ 1 / 2

Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is at least 1 / 2.

theorem Erdos329.kruckeberg_1961 : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A = 1 / √2

Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound.

[Kr61] Krückeberg, Fritz, $B\sb{2}$-Folgen und verwandte Zahlenfolgen. J. Reine Angew. Math. (1961), 53-60.

theorem Erdos329.erdos_turan_1941 (A : Set ℕ) : IsSidon A → sidonUpperDensity A ≤ 1

Erdős and Turán [ErTu41] proved the upper bound of 1.

[ErTu41] Erdős, P. and Turán, P., On a problem of Sidon in additive number theory, and on some related problems. J. London Math. Soc. (1941), 212-215.

def Erdos329.IsPerfectDifferenceSet (D : Set ℕ) (n : ℕ) : Prop

A perfect difference set modulo n is a set D such that the map (a, b) ↦ a - b from D.offDiag to {x : ZMod n | x ≠ 0} is a bijection.

Equations

• Erdos329.IsPerfectDifferenceSet D n = Set.BijOn (fun (x : ℕ × ℕ) => match x with | (a, b) => ↑a - ↑b) D.offDiag {x : ZMod n | x ≠ 0}

theorem Erdos329.erdos_329.of_sub_perfectDifferenceSet : (∀ (A : Finset ℕ), IsSidon A → ∃ (D : Set ℕ) (n : ℕ), ↑A ⊆ D ∧ IsPerfectDifferenceSet D n) → sSup {x : ℝ | ∃ (A : Set ℕ) (_ : IsSidon A), sidonUpperDensity A = x} = 1

If any finite Sidon set can be embedded in a perfect difference set, then the maximum density would be 1.

theorem Erdos329.erdos_329.converse_implication : sSup {x : ℝ | ∃ (A : Set ℕ) (_ : IsSidon A), sidonUpperDensity A = x} = 1 → ∀ (A : Finset ℕ), IsSidon A → ∃ (D : Set ℕ) (n : ℕ), ↑A ⊆ D ∧ IsPerfectDifferenceSet D n

The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set.

Related results and examples

theorem Erdos329.squares_are_sidon : IsSidon {x : ℕ | ∃ (n : ℕ), n ^ 2 = x}

The set of squares {n^2 | n : ℕ} is a Sidon set.

theorem Erdos329.squares_sidon_density : sidonUpperDensity {x : ℕ | ∃ (n : ℕ), n ^ 2 = x} = 0

The set of squares has upper density 0.

theorem Erdos329.exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A

It is possible to construct a Sidon set with positive density.