Arithmetic progressions in CR-sets

DefinitionThick set in a commutative semigroup#✓fully proved

A subset \(A\) of a commutative semigroup \((S, +)\) is thick when for every finite set \(E \subseteq S\) there is an \(x \in S\) with \(E + x \subseteq A\), that is, \(e + x \in A\) for every \(e \in E\).

def IsAddThick (A : Set S) : Prop :=
  ∀ E : Finset S, ∃ x : S, ∀ e ∈ E, e + x ∈ A

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 1 (definition of thick sets).

Used by 4

Used byPiecewise syndetic set in a commutative semigroup · The whole commutative semigroup is piecewise syndetic · The whole commutative semigroup is thick · The empty set is not thick

DefinitionPiecewise syndetic set in a commutative semigroup#✓fully proved

A subset \(A\) of a commutative semigroup \((S, +)\) is piecewise syndetic when there is a finite set \(F \subseteq S\) such that the union \(\bigcup_{t \in F} (-t + A)\) is thick, where \(-t + A = \{s \in S : t + s \in A\}\).

def IsAddPiecewiseSyndetic (A : Set S) : Prop :=
  ∃ F : Finset S, IsAddThick (⋃ t ∈ F, {s : S | t + s ∈ A})

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 1 (definition of piecewise syndetic sets).

Uses 1 · Used by 2

Statement usesThick set in a commutative semigroup

Used byFurstenberg–Glasner theorem on progressions in piecewise syndetic sets · The whole commutative semigroup is piecewise syndetic

DefinitionJ-sets in commutative semigroups#✓fully proved

Let \(S\) be a commutative semigroup and let \(\mathbb{N} = \{0, 1, 2, \dots\}\). A set \(A \subseteq S\) is a \(J\)-set when for every finite set \(F\) of sequences \(f \colon \mathbb{N} \to S\) there are \(a \in S\) and a nonempty finite set \(H \subseteq \mathbb{N}\) such that \(a + \sum_{n \in H} f(n) \in A\) for every \(f \in F\).

def IsJSet (A : Set S) : Prop :=
  ∀ F : Finset (ℕ → S), ∃ a : S, ∃ H : List ℕ, H.Nodup ∧ H ≠ [] ∧
    ∀ f ∈ F, (H.map f).foldl (· + ·) a ∈ A

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Definition 1.

Used by 2

Used byDebnath–Goswami theorem on progressions in J-sets · The whole semigroup is a J-set

DefinitionCR-set#✓fully proved

A subset \(A\) of a commutative semigroup \((S, +)\) is a CR-set (combinatorially rich) when for every natural number \(n\), including \(n = 0\), there is a natural number \(r\) such that for every \(r \times n\) matrix \((m_{ij})\) with entries in \(S\) there are a nonempty set \(\alpha \subseteq \{1, \ldots, r\}\) and an element \(s \in S\) such that \(s + \sum_{i \in \alpha} m_{ij} \in A\) for every column \(j \in \{1, \ldots, n\}\).

The paper takes \(n \ge 1\). Allowing \(n = 0\) adds the requirement that \(S\) be nonempty, the paper's implicit convention: over an empty \(S\) every case \(n \ge 1\) holds vacuously (take \(r = 1\); there is no matrix), so without it \(\emptyset\) would be a CR-set of the empty semigroup. Over a nonempty \(S\) the two definitions agree.

def IsCRSet (A : Set S) : Prop :=
  ∀ n : ℕ, ∃ r : ℕ, ∀ M : Fin r → Fin n → S, ∃ α : Finset (Fin r), α.Nonempty ∧
    ∃ s : S, ∀ j, (α.toList.map fun i => M i j).foldl (· + ·) s ∈ A

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Definition 2.

Used by 5

Used byArithmetic progressions in CR-sets · The whole commutative semigroup is a CR-set · Essential CR-set · Essential CR-sets via decreasing sequences · The empty set is not a CR-set

DefinitionEssential CR-set#✓fully proved

Let \((S, +)\) be a commutative semigroup, and add ultrafilters on \(S\) by the rule that \(E \in p + q\) if and only if \(\{x \in S : \{y \in S : x + y \in E\} \in q\} \in p\). A subset \(A\) of \(S\) is an essential CR-set when there is an ultrafilter \(p\) on \(S\) with \(p + p = p\), all of whose members are CR-sets, such that \(A \in p\).

def IsEssentialCRSet (A : Set S) : Prop :=
  ∃ p : Ultrafilter S, p + p = p ∧ (∀ B ∈ p, IsCRSet B) ∧ A ∈ p

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 2 (definition of essential CR-sets before Theorem 7).

Uses 1 · Used by 2

Statement usesCR-set

Used byArithmetic progressions in essential CR-sets of the positive integers · Essential CR-sets via decreasing sequences

TheoremThe whole commutative semigroup is thick#✓fully proved

If \(S\) is a nonempty commutative semigroup, then \(S\) itself is a thick subset of \(S\).

theorem isAddThick_univ [Nonempty S] : IsAddThick (Set.univ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 1 (definition of thick sets).

Uses 1

Statement usesThick set in a commutative semigroup

TheoremThe empty set is not thick#✓fully proved

In a nonempty commutative semigroup, the empty set is not thick.

theorem not_isAddThick_empty [Nonempty S] : ¬ IsAddThick (∅ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 1 (definition of thick sets).

Uses 1

Statement usesThick set in a commutative semigroup

TheoremThe whole commutative semigroup is piecewise syndetic#✓fully proved

If \(S\) is a nonempty commutative semigroup, then \(S\) itself is a piecewise syndetic subset of \(S\).

theorem isAddPiecewiseSyndetic_univ [Nonempty S] :
    IsAddPiecewiseSyndetic (Set.univ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 1 (definition of piecewise syndetic sets).

Uses 2

Statement usesPiecewise syndetic set in a commutative semigroup

Proof usesThick set in a commutative semigroup

TheoremThe whole semigroup is a J-set#✓fully proved

In every nonempty commutative semigroup \(S\), the set \(S\) itself is a \(J\)-set.

theorem isJSet_univ [Nonempty S] : IsJSet (Set.univ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Definition 1.

Uses 1

Statement usesJ-sets in commutative semigroups

TheoremThe whole commutative semigroup is a CR-set#✓fully proved

If \(S\) is a nonempty commutative semigroup, then \(S\) itself is a CR-set in \(S\).

theorem isCRSet_univ [Nonempty S] : IsCRSet (Set.univ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Definition 2.

Uses 1

Statement usesCR-set

TheoremThe empty set is not a CR-set#✓fully proved

In every commutative semigroup, the empty set is not a CR-set.

theorem not_isCRSet_empty : ¬ IsCRSet (∅ : Set S)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Definition 2.

Uses 1

Statement usesCR-set

DefinitionFamilies with the Ramsey property#✓fully proved

Let \(S\) be a set. A collection \(F\) of subsets of \(S\) is a family with the Ramsey property when \(F\) is nonempty, \(\emptyset \notin F\), \(F\) is closed under supersets (if \(A \in F\) and \(A \subseteq B\), then \(B \in F\)), and whenever \(A \cup B \in F\), then \(A \in F\) or \(B \in F\).

def IsRamseyFamily (F : Set (Set S)) : Prop :=
  F.Nonempty ∧ ∅ ∉ F ∧ (∀ A B, A ∈ F → A ⊆ B → B ∈ F) ∧
    ∀ A B, A ∪ B ∈ F → A ∈ F ∨ B ∈ F

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 2 (families and the Ramsey property).

Used by 8

Used byLeft-ideal criterion for β(F) · Subsemigroup criterion for β(F) · Essential F-sets contain shift-closed decreasing sequences (countable case) · β(F) contains an idempotent when it is a subsemigroup · Decreasing shift-closed sequences give essential sets · Ultrafilters inside a Ramsey family form a closed set · Nonempty closed sets of ultrafilters come from Ramsey families · Theorem 3, part 2: a Ramsey family is the union of its ultrafilters

DefinitionThe set β(F) of ultrafilters inside a family#✓fully proved

For a family \(\mathcal F\) of subsets of a set \(S\), \(\beta(\mathcal F)\) is the set of ultrafilters \(p\) on \(S\) all of whose members lie in \(\mathcal F\), that is, \(A \in \mathcal F\) for every \(A \in p\).

def betaFamily (F : Set (Set S)) : Set (Ultrafilter S) :=
  {p | ∀ A ∈ p, A ∈ F}

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 2 (definition of β(F)).

Used by 10

Used byLeft-ideal criterion for β(F) · Subsemigroup criterion for β(F) · β of the nonempty sets is all of βS · Essential F-sets contain shift-closed decreasing sequences (countable case) · β(F) contains an idempotent when it is a subsemigroup · Decreasing shift-closed sequences give essential sets · Ultrafilters inside a Ramsey family form a closed set · Nonempty closed sets of ultrafilters come from Ramsey families · Membership in β(F) · Theorem 3, part 2: a Ramsey family is the union of its ultrafilters

TheoremMembership in β(F)#✓fully proved

Let \(F\) be a collection of subsets of a set \(S\) and let \(p\) be an ultrafilter on \(S\). Then \(p \in \beta(F)\) if and only if every member of \(p\) belongs to \(F\).

theorem mem_betaFamily {F : Set (Set S)} {p : Ultrafilter S} :
    p ∈ betaFamily F ↔ ∀ A ∈ p, A ∈ F

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 2 (definition of β(F)).

Uses 1

Statement usesThe set β(F) of ultrafilters inside a family

Theoremβ of the nonempty sets is all of βS#✓fully proved

For every set \(S\), every ultrafilter on \(S\) lies in \(\beta(\mathcal F)\), where \(\mathcal F\) is the family of all nonempty subsets of \(S\); that is, \(\beta(\mathcal F) = \beta S\), the set of all ultrafilters on \(S\).

theorem betaFamily_nonempty_sets :
    betaFamily {A : Set S | A.Nonempty} = Set.univ

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Section 2 (definition of β(F)).

Uses 1

Statement usesThe set β(F) of ultrafilters inside a family

TheoremUltrafilters inside a Ramsey family form a closed set#●ready to prove

Let \(F\) be a family of subsets of a set \(S\) with the Ramsey property. Then the set \(\beta(F)\) of ultrafilters on \(S\) all of whose members lie in \(F\) is closed in the space \(\beta S\) of all ultrafilters on \(S\).

public theorem_wanted isClosed_betaFamily {F : Set (Set S)} (hF : IsRamseyFamily F) :
    IsClosed (betaFamily F)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 3.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremTheorem 3, part 2: a Ramsey family is the union of its ultrafilters#●ready to prove

Let \(F\) be a family of subsets of a set \(S\) with the Ramsey property, and let \(\beta(F)\) be the set of ultrafilters on \(S\) all of whose members lie in \(F\). Then a set \(A \subseteq S\) lies in \(F\) if and only if \(A \in p\) for some \(p \in \beta(F)\); that is, \(F = \bigcup \beta(F)\).

public theorem_wanted mem_iff_exists_mem_betaFamily {F : Set (Set S)} (hF : IsRamseyFamily F)
    (A : Set S) : A ∈ F ↔ ∃ p ∈ betaFamily F, A ∈ p

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 3.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremNonempty closed sets of ultrafilters come from Ramsey families#●ready to prove

Let \(S\) be a set, let \(\beta S\) be the space of ultrafilters on \(S\), and let \(K\) be a nonempty closed subset of \(\beta S\). Let \(\mathcal F_K\) be the collection of the sets \(E \subseteq S\) with \(E \in p\) for some \(p \in K\). Then \(\mathcal F_K\) is a family with the Ramsey property, and \(\beta(\mathcal F_K) = K\), where \(\beta(\mathcal F_K)\) is the set of ultrafilters on \(S\) all of whose members lie in \(\mathcal F_K\).

The paper omits \(K \ne \emptyset\); for \(K = \emptyset\) the collection \(\mathcal F_K\) is empty, hence not a family.

public theorem_wanted isRamseyFamily_and_betaFamily_eq_of_isClosed {K : Set (Ultrafilter S)}
    (hK : IsClosed K) (hne : K.Nonempty) :
    IsRamseyFamily {E : Set S | ∃ p ∈ K, E ∈ p} ∧ betaFamily {E : Set S | ∃ p ∈ K, E ∈ p} = K

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 3.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

Theoremβ(F) contains an idempotent when it is a subsemigroup#●ready to prove

Let \(S\) be a semigroup and \(\mathcal F\) a family of subsets of \(S\) with the Ramsey property, and multiply ultrafilters on \(S\) by \(E \in pq\) iff \(\{x \in S : \{y \in S : xy \in E\} \in q\} \in p\). If \(pq \in \beta(\mathcal F)\) for all \(p, q \in \beta(\mathcal F)\), then there is \(p \in \beta(\mathcal F)\) with \(pp = p\).

public theorem_wanted exists_idempotent_mem_betaFamily [Semigroup S] {F : Set (Set S)}
    (hF : IsRamseyFamily F) (hsub : ∀ p ∈ betaFamily F, ∀ q ∈ betaFamily F, p * q ∈ betaFamily F) :
    ∃ p ∈ betaFamily F, p * p = p

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 3.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremLeft-ideal criterion for β(F)#●ready to prove

Let \(S\) be a semigroup and \(\mathcal F\) a family of subsets of \(S\) with the Ramsey property. Multiply ultrafilters on \(S\) by \(E \in pq\) iff \(\{x \in S : \{y \in S : xy \in E\} \in q\} \in p\). Then \(pq \in \beta(\mathcal F)\) for every ultrafilter \(p\) on \(S\) and every \(q \in \beta(\mathcal F)\) (that is, \(\beta(\mathcal F)\) is a left ideal of \(\beta S\)) if and only if \(sE = \{se : e \in E\}\) lies in \(\mathcal F\) for every \(s \in S\) and every \(E \in \mathcal F\).

The paper's second sentence (right ideal iff right shift-invariant) is omitted: with this convention it fails. Let \(L\) be a minimal left ideal of \(\beta\mathbb{N}\) and \(\mathcal F_L\) the family of sets belonging to some member of \(L\). By the left half \(\mathcal F_L\) is shift-invariant (\(\mathbb{N}\) is commutative), yet \(L\) is not a right ideal, since a two-sided ideal contains the smallest ideal \(K(\beta\mathbb{N})\), a union of more than one minimal left ideal.

public theorem_wanted betaFamily_isLeftIdeal_iff [Semigroup S] {F : Set (Set S)}
    (hF : IsRamseyFamily F) :
    (∀ p : Ultrafilter S, ∀ q ∈ betaFamily F, p * q ∈ betaFamily F) ↔
      ∀ s : S, ∀ E ∈ F, (fun e => s * e) '' E ∈ F

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 4.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremSubsemigroup criterion for β(F)#●ready to prove

Let \(S\) be a semigroup and \(\mathcal F\) a family of subsets of \(S\) with the Ramsey property. For \(x \in S\) and \(E \subseteq S\) write \(x^{-1}E = \{y \in S : xy \in E\}\), and multiply ultrafilters on \(S\) by \(E \in pq\) iff \(\{x \in S : x^{-1}E \in q\} \in p\). Then \(pq \in \beta(\mathcal F)\) for all \(p, q \in \beta(\mathcal F)\) if and only if every \(E \subseteq S\) has the following property: if there is \(A \in \mathcal F\) such that \(\bigcap_{x \in H} x^{-1}E \in \mathcal F\) for every finite \(H \subseteq A\), then \(E \in \mathcal F\).

The source's intersection \(\bigcap_{q \in H} x^{-1}E\) is read as \(\bigcap_{x \in H} x^{-1}E\).

public theorem_wanted betaFamily_isSubsemigroup_iff [Semigroup S] {F : Set (Set S)}
    (hF : IsRamseyFamily F) :
    (∀ p ∈ betaFamily F, ∀ q ∈ betaFamily F, p * q ∈ betaFamily F) ↔
      ∀ E : Set S, (∃ A ∈ F, ∀ H : Finset S, ↑H ⊆ A →
        (⋂ x ∈ H, {y : S | x * y ∈ E}) ∈ F) → E ∈ F

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 5.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremDecreasing shift-closed sequences give essential sets#●ready to prove

Let \(S\) be a semigroup and let \(F\) be a family of subsets of \(S\) with the Ramsey property, and write \(\beta(F)\) for the set of ultrafilters on \(S\) all of whose members lie in \(F\). For \(x \in S\) and \(E \subseteq S\) write \(x^{-1}E = \{y \in S : xy \in E\}\), and multiply ultrafilters on \(S\) by the rule that \(E \in p \cdot q\) if and only if \(\{x \in S : x^{-1}E \in q\} \in p\). Suppose that \(p \cdot q \in \beta(F)\) whenever \(p, q \in \beta(F)\). Let \(A \subseteq S\), and let \(C_0 \supseteq C_1 \supseteq C_2 \supseteq \cdots\) be members of \(F\) contained in \(A\) such that for every \(n\) and every \(x \in C_n\) there is an \(m\) with \(C_m \subseteq x^{-1}C_n\). Then some \(p \in \beta(F)\) satisfies \(p \cdot p = p\) and \(A \in p\); that is, \(A\) is an essential \(F\)-set.

This is the implication (d) ⇒ (a) of the paper's Theorem 6; statements (b) (trees of functions) and (c) (downward directed families) are omitted. The sequence is indexed from \(0\) rather than \(1\).

public theorem_wanted exists_idempotent_mem_of_decreasing_sequence [Semigroup S]
    {F : Set (Set S)} (hF : IsRamseyFamily F)
    (hsub : ∀ p ∈ betaFamily F, ∀ q ∈ betaFamily F, p * q ∈ betaFamily F) {A : Set S}
    (C : ℕ → Set S) (hanti : Antitone C) (hCA : ∀ n, C n ⊆ A)
    (hshift : ∀ n, ∀ x ∈ C n, ∃ m, C m ⊆ {y : S | x * y ∈ C n}) (hCF : ∀ n, C n ∈ F) :
    ∃ p ∈ betaFamily F, p * p = p ∧ A ∈ p

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 6.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremEssential F-sets contain shift-closed decreasing sequences (countable case)#●ready to prove

Let \(S\) be a countable semigroup and \(\mathcal F\) a family of subsets of \(S\) with the Ramsey property. For \(x \in S\) and \(E \subseteq S\) write \(x^{-1}E = \{y \in S : xy \in E\}\), multiply ultrafilters on \(S\) by \(E \in pq\) iff \(\{x \in S : x^{-1}E \in q\} \in p\), and assume \(pq \in \beta(\mathcal F)\) for all \(p, q \in \beta(\mathcal F)\). If \(A \subseteq S\) belongs to some \(p \in \beta(\mathcal F)\) with \(pp = p\) (an essential \(\mathcal F\)-set), then there are sets \(C_0 \supseteq C_1 \supseteq C_2 \supseteq \cdots\) in \(\mathcal F\), all contained in \(A\), such that for every \(n\) and every \(x \in C_n\) there is \(m\) with \(C_m \subseteq x^{-1}C_n\).

Statements (b) (trees of functions) and (c) (downward directed families) of the paper are omitted. The sequence is indexed from \(0\).

public theorem_wanted exists_decreasing_sequence_of_idempotent_mem [Semigroup S] [Countable S]
    {F : Set (Set S)} (hF : IsRamseyFamily F)
    (hsub : ∀ p ∈ betaFamily F, ∀ q ∈ betaFamily F, p * q ∈ betaFamily F) {A : Set S}
    (hA : ∃ p ∈ betaFamily F, p * p = p ∧ A ∈ p) :
    ∃ C : ℕ → Set S, Antitone C ∧ (∀ n, C n ⊆ A) ∧
      (∀ n, ∀ x ∈ C n, ∃ m, C m ⊆ {y : S | x * y ∈ C n}) ∧ ∀ n, C n ∈ F

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 6.

Uses 2

Statement usesFamilies with the Ramsey property · The set β(F) of ultrafilters inside a family

TheoremFurstenberg–Glasner theorem on progressions in piecewise syndetic sets#●ready to prove

If \(S \subseteq \mathbb{Z}\) is piecewise syndetic, then for every natural number \(k\) the set of pairs \((a, d) \in \mathbb{Z} \times \mathbb{Z}\) such that \(a + i d \in S\) for all \(i = 0, 1, \dots, k\) is piecewise syndetic in \(\mathbb{Z} \times \mathbb{Z}\).

The paper takes \(k \ge 1\); the case \(k = 0\) is included.

public theorem_wanted IsAddPiecewiseSyndetic.arithmeticProgressions_int {S : Set ℤ}
    (hS : IsAddPiecewiseSyndetic S) (k : ℕ) :
    IsAddPiecewiseSyndetic {p : ℤ × ℤ | ∀ i ≤ k, p.1 + i * p.2 ∈ S}

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 1.

Uses 1

Statement usesPiecewise syndetic set in a commutative semigroup

TheoremDebnath–Goswami theorem on progressions in J-sets#●ready to prove

Let \(\mathbb{N}^+\) denote the positive integers under addition. If \(S \subseteq \mathbb{N}^+\) is a \(J\)-set, then for every natural number \(k\) the set of pairs \((a, d) \in \mathbb{N}^+ \times \mathbb{N}^+\) such that \(a + i d \in S\) for all \(i = 0, 1, \dots, k\) is a \(J\)-set in \(\mathbb{N}^+ \times \mathbb{N}^+\).

The paper writes \(\mathbb{N}\) for the positive integers and takes \(k \ge 1\); the case \(k = 0\) is included.

public theorem_wanted IsJSet.arithmeticProgressions_pnat {S : Set ℕ+} (hS : IsJSet S) (k : ℕ) :
    IsJSet {p : ℕ+ × ℕ+ | ∀ i ≤ k, (· + p.2)^[i] p.1 ∈ S}

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 2.

Uses 1

Statement usesJ-sets in commutative semigroups

TheoremEssential CR-sets via decreasing sequences#●ready to prove

Let \(S\) be a countable commutative semigroup and let \(A \subseteq S\). Then \(A\) is an essential CR-set if and only if there is a decreasing sequence \(C_0 \supseteq C_1 \supseteq C_2 \supseteq \cdots\) of CR-sets contained in \(A\) such that for every \(n\) and every \(x \in C_n\) there is an \(m\) with \(C_m \subseteq -x + C_n\), where \(-x + C_n = \{y \in S : x + y \in C_n\}\).

The sequence is indexed from \(0\) rather than \(1\).

public theorem_wanted isEssentialCRSet_iff_exists_decreasing_sequence {S : Type*}
    [AddCommSemigroup S] [Countable S] (A : Set S) :
    IsEssentialCRSet A ↔ ∃ C : ℕ → Set S, Antitone C ∧ (∀ n, C n ⊆ A) ∧
      (∀ n, ∀ x ∈ C n, ∃ m, C m ⊆ {y : S | x + y ∈ C n}) ∧ ∀ n, IsCRSet (C n)

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 7.

Uses 2

Statement usesCR-set · Essential CR-set

TheoremArithmetic progressions in CR-sets#●ready to prove

If \(A\) is a CR-set in a commutative semigroup \((S, +)\) and \(l\) is a natural number, then the set of pairs \((a, b) \in S \times S\) such that \(a, a + b, a + 2b, \dots, a + lb\) all lie in \(A\) is a CR-set in \(S \times S\). Here \(a + ib\) is \(a\) followed by \(i\) additions of \(b\), since \(S\) need not have a zero.

The paper takes \(l \ge 1\); the case \(l = 0\) is included.

public theorem_wanted IsCRSet.arithmeticProgressions {S : Type*} [AddCommSemigroup S]
    {A : Set S} (hA : IsCRSet A) (l : ℕ) :
    IsCRSet {p : S × S | ∀ i ≤ l, (· + p.2)^[i] p.1 ∈ A}

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 8.

Uses 1

Statement usesCR-set

TheoremArithmetic progressions in essential CR-sets of the positive integers#●ready to prove

Let \(\mathbb{N}^+\) denote the positive integers under addition. If \(A \subseteq \mathbb{N}^+\) is an essential CR-set and \(l\) is a natural number, then the set of pairs \((a, b) \in \mathbb{N}^+ \times \mathbb{N}^+\) such that \(a + i b \in A\) for all \(i = 0, 1, \dots, l\) is an essential CR-set in \(\mathbb{N}^+ \times \mathbb{N}^+\).

The paper writes \(\mathbb{N}\) for the positive integers and takes \(l \ge 1\); the case \(l = 0\) is included.

public theorem_wanted IsEssentialCRSet.arithmeticProgressions_pnat {A : Set ℕ+}
    (hA : IsEssentialCRSet A) (l : ℕ) :
    IsEssentialCRSet {p : ℕ+ × ℕ+ | ∀ i ≤ l, (· + p.2)^[i] p.1 ∈ A}

Sources

• De and Debnath, Abundance of Arithmetic Progressions in CR-Sets, INTEGERS 25 (2025), Article A4, Theorem 9.

Uses 1

Statement usesEssential CR-set

15 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.