Sidon ideal

DefinitionWeak Sidon set#✓fully proved

A set \(A \subseteq \mathbb{N}\) is a weak Sidon set (or well spread) if sums of two distinct elements of \(A\) are distinct: whenever \(a, b, c, d \in A\) satisfy \(a < b\), \(c < d\) and \(a + b = c + d\), then \(a = c\).

public def IsWeakSidonSet (A : Set ℕ) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a < b → c < d → a + b = c + d → a = c
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 11.
Used by 3
Used byWeak Sidon sets split into two Sidon sets · Weak Sidon sets generate the Sidon ideal · Sidon sets are weak Sidon sets

TheoremSidon sets are weak Sidon sets#✓fully proved

Every Sidon set \(A \subseteq \mathbb{N}\) is a weak Sidon set.

public theorem isWeakSidonSet_of_isSidon {A : Set ℕ} (h : A.IsSidon) :
    IsWeakSidonSet A
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definitions 10 and 11.
Uses 2
Statement usesWeak Sidon set · Sidon set

DefinitionIdeal generated by a property#✓fully proved

Let \(P\) be a property of subsets of \(\mathbb{N}\). The ideal generated by \(P\) is the family of all sets \(A \subseteq \mathbb{N}\) that are contained in the union of finitely many sets with property \(P\). The empty union is allowed, so the empty set always belongs to it.

public def generatedIdeal (P : Set ℕ → Prop) : Set (Set ℕ) :=
  {A | ∃ (n : ℕ) (S : Fin n → Set ℕ), (∀ j, P (S j)) ∧ A ⊆ ⋃ j, S j}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 1 (ideals) and Definitions 5, 8 and 13 (ideals generated by a family).
Used by 9
Used byThe almost thin ideal is contained in the Sidon ideal · A Sidon set outside the almost thin ideal · A set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal · Weak Sidon sets generate the Sidon ideal · Generated ideals are closed under subsets · Sets with a property lie in the ideal it generates · Sidon ideal · The Sidon ideal is contained in the lacunary ideal · Generated ideals are closed under unions

TheoremSets with a property lie in the ideal it generates#✓fully proved

Let \(P\) be a property of subsets of \(\mathbb{N}\). Every set \(A \subseteq \mathbb{N}\) with property \(P\) lies in the ideal generated by \(P\), the family of all subsets of finite unions of sets with property \(P\).

public theorem mem_generatedIdeal {P : Set ℕ → Prop} {A : Set ℕ} (h : P A) :
    A ∈ generatedIdeal P
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 1 (ideals).
Uses 1
Statement usesIdeal generated by a property

TheoremGenerated ideals are closed under subsets#✓fully proved

Let \(P\) be a property of subsets of \(\mathbb{N}\). If \(A\) lies in the ideal generated by \(P\) and \(B \subseteq A\), then \(B\) also lies in the ideal generated by \(P\).

public theorem generatedIdeal_of_subset {P : Set ℕ → Prop} {A B : Set ℕ} (hBA : B ⊆ A)
    (hA : A ∈ generatedIdeal P) : B ∈ generatedIdeal P
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 1 (ideals, item 2).
Uses 1
Statement usesIdeal generated by a property

TheoremGenerated ideals are closed under unions#✓fully proved

Let \(P\) be a property of subsets of \(\mathbb{N}\), and consider the ideal generated by \(P\), the family of all subsets of finite unions of sets with property \(P\). If \(A\) and \(B\) lie in this ideal, then so does \(A \cup B\).

public theorem union_mem_generatedIdeal {P : Set ℕ → Prop} {A B : Set ℕ}
    (hA : A ∈ generatedIdeal P) (hB : B ∈ generatedIdeal P) :
    A ∪ B ∈ generatedIdeal P
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 1 (ideals, item 3).
Uses 1
Statement usesIdeal generated by a property

AbbreviationSidon ideal#✓fully proved

The Sidon ideal \(\mathrm{Si}\) is the ideal on \(\mathbb{N}\) generated by the Sidon sets: it consists of all sets \(A \subseteq \mathbb{N}\) contained in a finite union of Sidon subsets of \(\mathbb{N}\).

public abbrev sidonIdeal : Set (Set ℕ) :=
  generatedIdeal Set.IsSidon
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 13.
Uses 2 · Used by 5
Statement usesIdeal generated by a property · Sidon set
Used byThe almost thin ideal is contained in the Sidon ideal · A set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal · Weak Sidon sets generate the Sidon ideal · The Sidon ideal is \(F_\sigma\) · The Sidon ideal is contained in the lacunary ideal

DefinitionGap-lacunary set#✓fully proved

A set \(A \subseteq \mathbb{N}\) is gap-lacunary (called lacunary in the source) if it is infinite and, writing \(A(n)\) for its \(n\)-th element in increasing order (counting from \(n = 0\)), the gaps \(A(n+1) - A(n)\) tend to infinity as \(n \to \infty\).

This differs from Hadamard lacunarity, where consecutive elements grow by a factor at least \(q > 1\).

public def IsGapLacunarySet (A : Set ℕ) : Prop :=
  A.Infinite ∧
    Tendsto (fun n => Nat.nth (· ∈ A) (n + 1) - Nat.nth (· ∈ A) n) atTop atTop
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 4.
Used by 3
Used byA set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal · Gap-lacunary sets are infinite · The Sidon ideal is contained in the lacunary ideal

TheoremGap-lacunary sets are infinite#✓fully proved

Every gap-lacunary set \(A \subseteq \mathbb{N}\) is infinite.

public theorem IsGapLacunarySet.infinite {A : Set ℕ} (h : IsGapLacunarySet A) : A.Infinite
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 4.
Uses 1
Statement usesGap-lacunary set

DefinitionAlmost thin set#✓fully proved

A set \(A \subseteq \mathbb{N}\) is almost thin if it is infinite and, writing \(A(n)\) for its \(n\)-th element in increasing order (counting from \(n = 0\)), there is a real number \(\alpha < 1\) such that \(A(n)/A(n+1) \le \alpha\) for all sufficiently large \(n\).

Since the ratios \(A(n)/A(n+1)\) lie in \([0, 1]\), this is equivalent to \(\limsup_{n \to \infty} A(n)/A(n+1) < 1\).

public def IsAlmostThinSet (A : Set ℕ) : Prop :=
  A.Infinite ∧ ∃ α : ℝ, α < 1 ∧
    ∀ᶠ n in atTop, (Nat.nth (· ∈ A) n : ℝ) / Nat.nth (· ∈ A) (n + 1) ≤ α
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 7.
Used by 3
Used byThe almost thin ideal is contained in the Sidon ideal · A Sidon set outside the almost thin ideal · Almost thin sets are infinite

TheoremAlmost thin sets are infinite#✓fully proved

Every almost thin set \(A \subseteq \mathbb{N}\) is infinite.

public theorem IsAlmostThinSet.infinite {A : Set ℕ} (h : IsAlmostThinSet A) :
    A.Infinite
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 7.
Uses 1
Statement usesAlmost thin set

DefinitionVan der Waerden ideal#✓fully proved

The van der Waerden ideal \(W\) consists of the sets \(A \subseteq \mathbb{N}\) for which there is an \(n > 0\) such that \(A\) contains no arithmetic progression \(a, a + r, \dots, a + (n - 1) r\) of \(n\) terms with \(a \in \mathbb{N}\) and \(r > 0\).

public def vanDerWaerdenIdeal : Set (Set ℕ) :=
  {A | ∃ n > 0, ∀ a r : ℕ, 0 < r → ∃ j < n, a + r * j ∉ A}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 9.
Used by 2
Used byThe empty set lies in the van der Waerden ideal · A set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal

TheoremThe empty set lies in the van der Waerden ideal#✓fully proved

The empty subset of \(\mathbb{N}\) belongs to the van der Waerden ideal.

public theorem empty_mem_vanDerWaerdenIdeal : (∅ : Set ℕ) ∈ vanDerWaerdenIdeal
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 9.
Uses 1
Statement usesVan der Waerden ideal

DefinitionPositive difference set#✓fully proved

For a set \(Z \subseteq \mathbb{N}\), the positive difference set \(D(Z)\) is the set of all differences \(a - b\) with \(a, b \in Z\) and \(a > b\).

public def positiveDifferences (Z : Set ℕ) : Set ℕ :=
  {d | ∃ a ∈ Z, ∃ b ∈ Z, b < a ∧ d = a - b}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 1 (notation A - B and D(A)).
Used by 2
Used byThe ideal of sets avoiding large difference sets · The empty set lies in the difference-set ideal

DefinitionThe ideal of sets avoiding large difference sets#✓fully proved

For a set \(Z \subseteq \mathbb{N}\), let \(D(Z) = \{a - b : a, b \in Z,\ b < a\}\) be its set of positive differences. The ideal \(D_{\mathrm{fin}}\) consists of the sets \(A \subseteq \mathbb{N}\) for which there is a natural number \(n\) such that \(D(Z) \not\subseteq A\) for every \(n\)-element set \(Z \subseteq \mathbb{N}\).

public def dFinIdeal : Set (Set ℕ) :=
  {A | ∃ n : ℕ, ∀ Z : Finset ℕ, Z.card = n → ¬ positiveDifferences (Z : Set ℕ) ⊆ A}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 3.
Uses 1 · Used by 2
Statement usesPositive difference set
Used byThe empty set lies in the difference-set ideal · A set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal

TheoremThe empty set lies in the difference-set ideal#✓fully proved

The empty set belongs to the ideal \(D_{\mathrm{fin}}\) of sets \(A \subseteq \mathbb{N}\) for which some natural number \(n\) satisfies \(D(Z) \not\subseteq A\) for every \(n\)-element set \(Z \subseteq \mathbb{N}\), where \(D(Z)\) is the set of positive differences \(a - b\) with \(a, b \in Z\) and \(b < a\).

One can take \(n = 2\): every two-element set has a positive difference.

public theorem empty_mem_dFinIdeal : (∅ : Set ℕ) ∈ dFinIdeal
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Definition 3.
Uses 2
Statement usesThe ideal of sets avoiding large difference sets
Proof usesPositive difference set

DefinitionBlock sets#✓fully proved

For natural numbers \(n\), \(C\), \(M\) and \(K\), the block \(\mathrm{Block}(n, C, M, K)\) is the set of natural numbers \(M l + C \cdot 2^k\) with \(0 \le k < n\) and \(1 \le l \le K\).

public def sidonBlock (n C M K : ℕ) : Set ℕ :=
  {x | ∃ k < n, ∃ l, 1 ≤ l ∧ l ≤ K ∧ x = M * l + C * 2 ^ k}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 3 (definition of Block before Lemma 2).
Used by 2
Used byA block not covered by few Sidon sets · One-term blocks

TheoremOne-term blocks#✓fully proved

For all natural numbers \(C\) and \(M\), the block \(\mathrm{Block}(1, C, M, 1) = \{M l + C \cdot 2^k : 0 \le k < 1,\ 1 \le l \le 1\}\) is the singleton \(\{M + C\}\).

public theorem sidonBlock_one_one (C M : ℕ) : sidonBlock 1 C M 1 = {M + C}
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Section 3 (definition of Block before Lemma 2).
Uses 1
Statement usesBlock sets

TheoremWeak Sidon sets split into two Sidon sets#●ready to prove

Every weak Sidon set \(A \subseteq \mathbb{N}\) is the union of two disjoint Sidon sets \(B\) and \(C\).

public theorem_wanted exists_partition_isSidon_of_isWeakSidonSet {A : Set ℕ}
    (hA : IsWeakSidonSet A) :
    ∃ B C : Set ℕ, B ∪ C = A ∧ Disjoint B C ∧ B.IsSidon ∧ C.IsSidon
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 1.
Uses 2
Statement usesWeak Sidon set · Sidon set

TheoremWeak Sidon sets generate the Sidon ideal#●ready to prove

The ideal on \(\mathbb{N}\) generated by the weak Sidon sets equals the Sidon ideal.

public theorem_wanted generatedIdeal_isWeakSidonSet_eq_sidonIdeal :
    generatedIdeal IsWeakSidonSet = sidonIdeal
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Corollary 1.
Uses 3
Statement usesWeak Sidon set · Ideal generated by a property · Sidon ideal

TheoremThe Sidon ideal is \(F_\sigma\)#●ready to prove

Give the Cantor space \(\{0, 1\}^{\mathbb{N}}\) the product topology and identify each set \(A \subseteq \mathbb{N}\) with its indicator function. Then the set of indicator functions of the members of the Sidon ideal is a countable union of closed subsets of \(\{0, 1\}^{\mathbb{N}}\).

public theorem_wanted sidonIdeal_isFSigma :
    ∃ F : ℕ → Set (ℕ → Bool), (∀ k, IsClosed (F k)) ∧
      {f : ℕ → Bool | {n | f n = true} ∈ sidonIdeal} = ⋃ k, F k
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Corollary 2.
Uses 1
Statement usesSidon ideal

TheoremPositive sets whose elements at least double are Sidon#●ready to prove

Let \(A \subseteq \mathbb{N}\) with \(0 \notin A\), and write \(A(n)\) for the \(n\)-th element of \(A\) in increasing order, counting from \(n = 0\), with \(A(n) = 0\) when \(A\) has at most \(n\) elements. If \(2 A(n) \le A(n+1)\) for every \(n \in \mathbb{N}\), then \(A\) is a Sidon set.

The hypotheses force \(A\) to be empty or infinite, so the source's standing assumption that \(A\) is infinite is not needed.

public theorem_wanted isSidon_of_two_mul_nth_le {A : Set ℕ} (h0 : 0 ∉ A)
    (h : ∀ n, 2 * Nat.nth (· ∈ A) n ≤ Nat.nth (· ∈ A) (n + 1)) : A.IsSidon
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Lemma 1.
Uses 1
Statement usesSidon set

TheoremThe Sidon ideal is contained in the lacunary ideal#●ready to prove

Call a set \(A \subseteq \mathbb{N}\) lacunary if it is infinite and the gaps \(A(n + 1) - A(n)\) between consecutive elements tend to infinity, where \(A(n)\) is the \(n\)-th element of \(A\) in increasing order. Every set in the Sidon ideal is contained in a finite union of lacunary sets, that is, it lies in the ideal \(\mathrm{Lac}\) generated by the lacunary sets.

public theorem_wanted sidonIdeal_subset_lacunaryIdeal :
    sidonIdeal ⊆ generatedIdeal IsGapLacunarySet
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 2.
Uses 3
Statement usesGap-lacunary set · Ideal generated by a property · Sidon ideal

TheoremMian–Chowla lower bound for an infinite Sidon set#●ready to prove

There exist a Sidon set \(A \subseteq \mathbb{N}\) and a real constant \(c > 0\) such that \(|A \cap \{1, \dots, n\}| > c\, n^{1/3}\) for every natural number \(n \ge 1\).

public theorem_wanted exists_isSidon_card_gt_cbrt :
    ∃ A : Set ℕ, A.IsSidon ∧ ∃ c : ℝ, 0 < c ∧
      ∀ n : ℕ, 1 ≤ n → c * (n : ℝ) ^ ((1 : ℝ) / 3) < (A ∩ Set.Icc 1 n).ncard
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 3, item 1, quoting A. M. Mian and S. Chowla, On the B₂ sequences of Sidon, Proc. Nat. Acad. Sci. India Sect. A 14 (1944).
Uses 1
Statement usesSidon set

TheoremAjtai–Komlós–Szemerédi lower bound for an infinite Sidon set#●ready to prove

There exist a Sidon set \(A \subseteq \mathbb{N}\) and a real constant \(c > 0\) such that \(|A \cap \{1, \dots, n\}| > c\, (n \log n)^{1/3}\) for every natural number \(n \ge 1\), where \(\log\) is the natural logarithm.

public theorem_wanted exists_isSidon_card_gt_cbrt_mul_log :
    ∃ A : Set ℕ, A.IsSidon ∧ ∃ c : ℝ, 0 < c ∧
      ∀ n : ℕ, 1 ≤ n →
        c * ((n : ℝ) * Real.log n) ^ ((1 : ℝ) / 3) < (A ∩ Set.Icc 1 n).ncard
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 3, item 2, quoting M. Ajtai, J. Komlós and E. Szemerédi, A dense infinite Sidon sequence, European J. Combin. 2 (1981).
Uses 1
Statement usesSidon set

TheoremRuzsa's lower bound for an infinite Sidon set#●ready to prove

There is a Sidon set \(A \subseteq \mathbb{N}\) such that for every real \(\varepsilon > 0\), the inequality \(|A \cap \{1, \dots, n\}| > n^{\sqrt{2} - 1 - \varepsilon}\) holds for all sufficiently large natural numbers \(n\); that is, \(|A \cap \{1, \dots, n\}| > n^{\sqrt{2} - 1 - o(1)}\).

public theorem_wanted exists_isSidon_card_gt_rpow_sqrt_two_sub_one :
    ∃ A : Set ℕ, A.IsSidon ∧ ∀ ε : ℝ, 0 < ε →
      ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ (Real.sqrt 2 - 1 - ε) < (A ∩ Set.Icc 1 n).ncard
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 3, item 3, quoting I. Z. Ruzsa, An infinite Sidon sequence, J. Number Theory 68 (1998).
Uses 1
Statement usesSidon set

TheoremA Sidon set outside the almost thin ideal#●ready to prove

There is a Sidon set \(A \subseteq \mathbb{N}\) that is not contained in any finite union of almost thin sets; that is, \(A\) does not belong to the ideal generated by the almost thin sets.

public theorem_wanted exists_isSidon_not_mem_almostThinIdeal :
    ∃ A : Set ℕ, A.IsSidon ∧ A ∉ generatedIdeal IsAlmostThinSet
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Proposition 1.
Uses 3
Statement usesAlmost thin set · Ideal generated by a property · Sidon set

TheoremThe almost thin ideal is contained in the Sidon ideal#●ready to prove

Every set \(A \subseteq \mathbb{N}\) that is contained in a finite union of almost thin sets is contained in a finite union of Sidon sets; that is, the ideal generated by the almost thin sets is contained in the Sidon ideal.

public theorem_wanted almostThinIdeal_subset_sidonIdeal :
    generatedIdeal IsAlmostThinSet ⊆ sidonIdeal
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 4.
Uses 3
Statement usesAlmost thin set · Ideal generated by a property · Sidon ideal

TheoremA block not covered by few Sidon sets#●ready to prove

Let \(n \ge 1\) and \(C \ge 1\) be natural numbers, and put \(M = C \cdot 2^n + 1\) and \(K = (n - 1)\binom{n}{2} + 1\). Then the block \(\mathrm{Block}(n, C, M, K) = \{M l + C \cdot 2^k : 0 \le k < n,\ 1 \le l \le K\}\) is not contained in the union of any \(n - 1\) Sidon subsets of \(\mathbb{N}\).

public theorem_wanted not_sidonBlock_subset_iUnion_isSidon {n C : ℕ} (hn : 0 < n)
    (hC : 0 < C) :
    ¬ ∃ S : Fin (n - 1) → Set ℕ, (∀ j, (S j).IsSidon) ∧
      sidonBlock n C (C * 2 ^ n + 1) ((n - 1) * n.choose 2 + 1) ⊆ ⋃ j, S j
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Lemma 3.
Uses 2
Statement usesBlock sets · Sidon set

TheoremA set in the van der Waerden, lacunary and difference-set ideals outside the Sidon ideal#●ready to prove

There is a set \(A \subseteq \mathbb{N}\) that belongs to the van der Waerden ideal, is contained in a finite union of gap-lacunary sets (infinite sets whose gaps between consecutive elements tend to infinity), and belongs to the ideal \(D_{\mathrm{fin}}\) of sets avoiding large difference sets, but is not contained in any finite union of Sidon sets.

public theorem_wanted exists_mem_vanDerWaerden_lacunary_dFin_not_mem_sidonIdeal :
    ∃ A : Set ℕ, A ∈ vanDerWaerdenIdeal ∧ A ∈ generatedIdeal IsGapLacunarySet ∧
      A ∈ dFinIdeal ∧ A ∉ sidonIdeal
Sources
  • Andrzej Nowik, On the Sidon Ideal, INTEGERS 25 (2025), Article A91, Theorem 5.
Uses 5
Statement usesGap-lacunary set · The ideal of sets avoiding large difference sets · Ideal generated by a property · Sidon ideal · Van der Waerden ideal
18 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.