Number of Sidon sets

DefinitionSidon subsets of \(\{1, \dots, N\}\)#✓fully proved

For a natural number \(N\), this is the finite family of all subsets of \(\{1, \dots, N\}\) that are Sidon sets of natural numbers, including the empty set and the singletons.

noncomputable def sidonSubsetsUpTo (N : ℕ) : Finset (Finset ℕ) :=
  (Finset.Icc 1 N).powerset.filter fun S => (S : Set ℕ).IsSidon

Uses 1 · Used by 3

Statement usesSidon set

Used byLargest Sidon subset of \(\{1, \dots, N\}\) (Erdős Problem 861) · Erdős Problem 861, second question · Erdős Problem 861, first question

DefinitionLargest Sidon subset of \(\{1, \dots, N\}\) (Erdős Problem 861)#✓fully proved

For a natural number \(N\), \(f(N)\) is the largest cardinality of a Sidon subset of \(\{1, \dots, N\}\).

noncomputable def maxSidonSize (N : ℕ) : ℕ :=
  (sidonSubsetsUpTo N).sup Finset.card

Uses 1 · Used by 2

Statement usesSidon subsets of \(\{1, \dots, N\}\)

Used byErdős Problem 861, second question · Erdős Problem 861, first question

DefinitionErdős Problem 861, first question#✓fully proved

Let \(A(N)\) be the number of Sidon subsets of \(\{1, \dots, N\}\), including the empty set and the singletons, and let \(f(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). The statement is that \(A(N) / 2^{f(N)} \to \infty\) as \(N \to \infty\).

def sidonCountOverTwoPowMaxDiverges : Prop :=
  Filter.Tendsto (fun N : ℕ => ((sidonSubsetsUpTo N).card : ℝ) / 2 ^ maxSidonSize N)
    Filter.atTop Filter.atTop

Uses 2 · Used by 1

Statement usesLargest Sidon subset of \(\{1, \dots, N\}\) (Erdős Problem 861) · Sidon subsets of \(\{1, \dots, N\}\)

Used byErdős Problem 861, first question: positive answer

DefinitionErdős Problem 861, second question#✓fully proved

Let \(A(N)\) be the number of Sidon subsets of \(\{1, \dots, N\}\), including the empty set and the singletons, and let \(f(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). The statement is that \(\log_2 A(N) / f(N) \to 1\) as \(N \to \infty\), that is, \(A(N) = 2^{(1 + o(1)) f(N)}\).

def sidonCountExponentAsymptotic : Prop :=
  Filter.Tendsto (fun N : ℕ => Real.logb 2 (sidonSubsetsUpTo N).card / maxSidonSize N)
    Filter.atTop (nhds 1)

Uses 2 · Used by 1

Statement usesLargest Sidon subset of \(\{1, \dots, N\}\) (Erdős Problem 861) · Sidon subsets of \(\{1, \dots, N\}\)

Used byErdős Problem 861, second question: negative answer

TheoremErdős Problem 861, first question: positive answer#●ready to prove

Let \(A(N)\) be the number of Sidon subsets of \(\{1, \dots, N\}\), including the empty set and the singletons, and let \(f(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). Then \(A(N) / 2^{f(N)} \to \infty\) as \(N \to \infty\).

Saxton and Thomason proved \(A(N) \ge 2^{(1.16 + o(1)) \sqrt{N}}\) (Theorem 2.11), and \(f(N) \sim \sqrt{N}\), so \(A(N) / 2^{f(N)} \ge 2^{(0.16 + o(1)) \sqrt{N}} \to \infty\).

public theorem_wanted sidonCountOverTwoPowMaxDiverges_holds : sidonCountOverTwoPowMaxDiverges

Sources

• T. F. Bloom, Erdős Problems, Problem #861, https://www.erdosproblems.com/861 (status SOLVED); resolution: D. Saxton and A. Thomason, Hypergraph containers, Invent. Math. (2015), 925-992, arXiv:1204.6595 (lower bound); Y. Kohayakawa, S. J. Lee, V. Rödl and W. Samotij, The number of Sidon sets and the maximum size of Sidon sets contained in a sparse random set of integers, Random Structures Algorithms (2015), 1-25 (upper bound), Saxton-Thomason Theorem 2.11: there are between 2^{(1.16 + o(1)) √n} and 2^{(55 + o(1)) √n} Sidon subsets of [n], the lower bound answering negatively whether there are only 2^{(1 + o(1)) √n}; erdosproblems.com/861: f(N) ∼ N^{1/2}, both questions are settled, the first positively and the second negatively, and 2^{1.16 f(N)} ≤ A(N) ≤ 2^{6.442 f(N)} for large N, https://arxiv.org/abs/1204.6595.

Uses 1

Statement usesErdős Problem 861, first question

TheoremErdős Problem 861, second question: negative answer#●ready to prove

Let \(A(N)\) be the number of Sidon subsets of \(\{1, \dots, N\}\), including the empty set and the singletons, and let \(f(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). Then the ratio \(\log_2 A(N) / f(N)\) does not tend to \(1\) as \(N \to \infty\); that is, \(A(N) = 2^{(1 + o(1)) f(N)}\) fails.

Saxton and Thomason proved \(A(N) \ge 2^{(1.16 + o(1)) \sqrt{N}}\) (Theorem 2.11), and \(f(N) \sim \sqrt{N}\), so \(\log_2 A(N) / f(N) \ge 1.16 + o(1)\).

public theorem_wanted sidonCountExponentAsymptotic_refuted : ¬ sidonCountExponentAsymptotic

Sources

• T. F. Bloom, Erdős Problems, Problem #861, https://www.erdosproblems.com/861 (status SOLVED); resolution: D. Saxton and A. Thomason, Hypergraph containers, Invent. Math. (2015), 925-992, arXiv:1204.6595 (lower bound); Y. Kohayakawa, S. J. Lee, V. Rödl and W. Samotij, The number of Sidon sets and the maximum size of Sidon sets contained in a sparse random set of integers, Random Structures Algorithms (2015), 1-25 (upper bound), Saxton-Thomason Theorem 2.11: there are between 2^{(1.16 + o(1)) √n} and 2^{(55 + o(1)) √n} Sidon subsets of [n], the lower bound answering negatively whether there are only 2^{(1 + o(1)) √n}; erdosproblems.com/861: f(N) ∼ N^{1/2}, both questions are settled, the first positively and the second negatively, and 2^{1.16 f(N)} ≤ A(N) ≤ 2^{6.442 f(N)} for large N, https://arxiv.org/abs/1204.6595.

Uses 1

Statement usesErdős Problem 861, second question

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.