Piecewise syndetic sets

DefinitionLattice cube#✓fully proved

For \(t, m \in \mathbb{N}\) and \(a \in \mathbb{N}^t\), the lattice cube with least corner \(a\) and side \(m\) is the set of points \(x \in \mathbb{N}^t\) such that \(a_i \le x_i < a_i + m\) for every coordinate \(i\); it is a subcube of size \(m^t\).

def latticeCube {t : ℕ} (a : Fin t → ℕ) (m : ℕ) : Set (Fin t → ℕ) :=
  Set.univ.pi fun i => Set.Ico (a i) (a i + m)

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1 (subcubes of N^t of size m^t).

Used by 14

Used byGap size · Density bounds the gap size · Finite sets in positive dimension have positive gap size · Gap size of a singleton · A color class is dense in a large subcube (Brown, Lemma 2) · Monochromatic sets that are large relative to their gap size · A color class is dense in a subcube (Brown, Lemma 1) · Density in subcubes · Density one means containment · Piecewise syndetic set · The whole space is piecewise syndetic · Lattice cube of side one · Membership in a lattice cube · The empty set is not piecewise syndetic

TheoremMembership in a lattice cube#✓fully proved

For \(t, m \in \mathbb{N}\) and \(a, x \in \mathbb{N}^t\), the point \(x\) lies in the lattice cube with least corner \(a\) and side \(m\) if and only if \(a_i \le x_i < a_i + m\) for every coordinate \(i\).

theorem mem_latticeCube {t : ℕ} {a x : Fin t → ℕ} {m : ℕ} :
    x ∈ latticeCube a m ↔ ∀ i, a i ≤ x i ∧ x i < a i + m

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1 (subcubes of N^t of size m^t).

Uses 1 · Used by 1

Statement usesLattice cube

Used byLattice cube of side one

TheoremLattice cube of side one#✓fully proved

For \(t \in \mathbb{N}\) and \(a \in \mathbb{N}^t\), the lattice cube with least corner \(a\) and side \(1\) is the singleton \(\{a\}\).

theorem latticeCube_one {t : ℕ} (a : Fin t → ℕ) : latticeCube a 1 = {a}

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1 (subcubes of N^t of size m^t).

Uses 2 · Used by 4

Statement usesLattice cube

Proof usesMembership in a lattice cube

Used byGap size of a singleton · Density one means containment · The whole space is piecewise syndetic · The empty set is not piecewise syndetic

DefinitionDensity in subcubes#✓fully proved

Let \(d \in \mathbb{N}\) and let \(C, M \subseteq \mathbb{N}^t\). The set \(C\) is \(d\)-dense in \(M\) when every subcube of \(\mathbb{N}^t\) of side \(d\) that is contained in \(M\) meets \(C\).

def IsDenseInCubes {t : ℕ} (d : ℕ) (C M : Set (Fin t → ℕ)) : Prop :=
  ∀ b : Fin t → ℕ, latticeCube b d ⊆ M → (latticeCube b d ∩ C).Nonempty

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1 (definition of m_{i-1}-dense in M').

Uses 1 · Used by 7

Statement usesLattice cube

Used byGap size · Density bounds the gap size · Finite sets in positive dimension have positive gap size · Gap size of a singleton · A color class is dense in a large subcube (Brown, Lemma 2) · A color class is dense in a subcube (Brown, Lemma 1) · Density one means containment

TheoremDensity one means containment#✓fully proved

For sets \(C, M \subseteq \mathbb{N}^t\), the set \(C\) is \(1\)-dense in \(M\) if and only if \(M \subseteq C\).

theorem isDenseInCubes_one_iff {t : ℕ} {C M : Set (Fin t → ℕ)} :
    IsDenseInCubes 1 C M ↔ M ⊆ C

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1 (definition of m_{i-1}-dense in M', with m_0 = 1).

Uses 3 · Used by 1

Statement usesDensity in subcubes

Proof usesLattice cube · Lattice cube of side one

Used byGap size of a singleton

DefinitionPiecewise syndetic set#✓fully proved

Let \(t \in \mathbb{N}\). A set \(A \subseteq \mathbb{N}^t\) is piecewise syndetic if there is \(d \in \mathbb{N}\) such that, writing \([0, d] = \{0, 1, \dots, d\}\), for every \(m \in \mathbb{N}\) the set \(A + [0, d]^t = \{y + z : y \in A,\ z \in [0, d]^t\}\) contains a lattice cube of side \(m\).

def IsPiecewiseSyndetic {t : ℕ} (A : Set (Fin t → ℕ)) : Prop :=
  ∃ d : ℕ, ∀ m : ℕ, ∃ a : Fin t → ℕ,
    latticeCube a m ⊆ {x | ∃ y ∈ A, ∃ z ∈ latticeCube 0 (d + 1), x = y + z}

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Proof 1 of Theorem 2 (meaning of piecewise syndetic).

Uses 1 · Used by 3

Statement usesLattice cube

Used byPiecewise syndeticity is partition regular · The whole space is piecewise syndetic · The empty set is not piecewise syndetic

TheoremThe whole space is piecewise syndetic#✓fully proved

For every \(t \in \mathbb{N}\), the whole space \(\mathbb{N}^t\) is piecewise syndetic.

theorem isPiecewiseSyndetic_univ {t : ℕ} : IsPiecewiseSyndetic (Set.univ : Set (Fin t → ℕ))

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Proof 1 of Theorem 2 (meaning of piecewise syndetic).

Uses 3

Statement usesPiecewise syndetic set

Proof usesLattice cube · Lattice cube of side one

TheoremThe empty set is not piecewise syndetic#✓fully proved

For every \(t \in \mathbb{N}\), the empty subset of \(\mathbb{N}^t\) is not piecewise syndetic.

theorem not_isPiecewiseSyndetic_empty {t : ℕ} :
    ¬ IsPiecewiseSyndetic (∅ : Set (Fin t → ℕ))

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Proof 1 of Theorem 2 (meaning of piecewise syndetic).

Uses 3

Statement usesPiecewise syndetic set

Proof usesLattice cube · Lattice cube of side one

TheoremA color class is dense in a subcube (Brown, Lemma 1)#●ready to prove

Let \(t, r \in \mathbb{N}\) and let \(1 = m_0 < m_1 < m_2 < \cdots\) be a strictly increasing sequence of natural numbers. Let \(M\) be a subcube of \(\mathbb{N}^t\) of side \(m_r\), and let \(c\) be a coloring of \(\mathbb{N}^t\) by natural numbers with \(1 \le c(x) \le r\) for every \(x \in M\). Then for some color \(i\) with \(1 \le i \le r\) there is a subcube \(M' \subseteq M\) of side \(m_i\) in which the class of color \(i\) is \(m_{i-1}\)-dense.

The paper fixes \(t \ge 1\) and \(r \ge 1\); both are dropped, since \(t = 0\) holds trivially and \(r = 0\) admits no coloring of the nonempty cube \(M\).

public theorem_wanted exists_subcube_isDenseInCubes_colorClass (t : ℕ) (m : ℕ → ℕ)
    (hm0 : m 0 = 1) (hm : StrictMono m) (r : ℕ) (a : Fin t → ℕ) (c : (Fin t → ℕ) → ℕ)
    (hc : ∀ x ∈ latticeCube a (m r), c x ∈ Set.Icc 1 r) :
    ∃ i ∈ Set.Icc 1 r, ∃ a' : Fin t → ℕ, latticeCube a' (m i) ⊆ latticeCube a (m r) ∧
      IsDenseInCubes (m (i - 1)) {x | c x = i} (latticeCube a' (m i))

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 1.

Uses 2

Statement usesDensity in subcubes · Lattice cube

TheoremA color class is dense in a large subcube (Brown, Lemma 2)#●ready to prove

Let \(r, t \in \mathbb{N}\) and let \(f : \mathbb{N} \to \mathbb{N}\). There is \(A \in \mathbb{N}\) such that for every coloring of \(\mathbb{N}^t\) with \(r\) colors there are natural numbers \(d \ge 1\) and \(m > f(d)\), a color \(j\), and a subcube \(M\) of side \(m\) with \(M \subseteq [1, A]^t\) in which the class of color \(j\) is \(d\)-dense. Here \([1, A]^t\) is the set of points \(x\) with \(1 \le x_i \le A\) for every coordinate \(i\).

The paper's "(a smallest)" is omitted: it follows from existence. Only the restriction of the coloring to \([1, A]^t\) matters.

public theorem_wanted exists_cube_bound_isDenseInCubes (r t : ℕ) (f : ℕ → ℕ) :
    ∃ A : ℕ, ∀ c : (Fin t → ℕ) → Fin r, ∃ d m : ℕ, 1 ≤ d ∧ f d < m ∧ ∃ j : Fin r,
      ∃ a : Fin t → ℕ, latticeCube a m ⊆ latticeCube (fun _ => 1) A ∧
        IsDenseInCubes d {x | c x = j} (latticeCube a m)

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Lemma 2.

Uses 2

Statement usesDensity in subcubes · Lattice cube

TheoremPiecewise syndeticity is partition regular#●ready to prove

Let \(A \subseteq \mathbb{N}^t\) be piecewise syndetic and let \(A_1, \dots, A_r \subseteq \mathbb{N}^t\) with \(A = A_1 \cup \dots \cup A_r\). Then some \(A_i\) is piecewise syndetic.

public theorem_wanted IsPiecewiseSyndetic.exists_of_eq_iUnion {t r : ℕ}
    {A : Set (Fin t → ℕ)} (hA : IsPiecewiseSyndetic A) (B : Fin r → Set (Fin t → ℕ))
    (hAB : A = ⋃ i, B i) : ∃ i, IsPiecewiseSyndetic (B i)

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Theorem 1.

Uses 1

Statement usesPiecewise syndetic set

DefinitionGap size#✓fully proved

For a set \(S \subseteq \mathbb{N}^t\), the gap size \(\operatorname{gs}(S)\) is the least \(d \ge 1\) such that \(S\) is \(d\)-dense in some subcube of \(\mathbb{N}^t\) that contains \(S\). If no such \(d\) exists (for instance when \(S\) is unbounded, so that no subcube contains it), the value is \(0\).

For \(t = 1\), the gap size of a finite set with at least two points is the largest difference between consecutive elements, and a one-point set has gap size \(1\) (Definition 1). The paper defines \(\operatorname{gs}\) only for finite sets; when \(t \ge 1\), every finite set has positive gap size.

public noncomputable def cubeGapSize {t : ℕ} (S : Set (Fin t → ℕ)) : ℕ :=
  sInf {d : ℕ | 0 < d ∧ ∃ (a : Fin t → ℕ) (m : ℕ), S ⊆ latticeCube a m ∧
    IsDenseInCubes d S (latticeCube a m)}

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Definition 5.

Uses 2 · Used by 4

Statement usesDensity in subcubes · Lattice cube

Used byDensity bounds the gap size · Finite sets in positive dimension have positive gap size · Gap size of a singleton · Monochromatic sets that are large relative to their gap size

TheoremDensity bounds the gap size#✓fully proved

Let \(S \subseteq \mathbb{N}^t\), let \(d \ge 1\), and let \(M\) be a subcube of \(\mathbb{N}^t\) with \(S \subseteq M\). If \(S\) is \(d\)-dense in \(M\), then the gap size of \(S\) satisfies \(\operatorname{gs}(S) \le d\).

public theorem cubeGapSize_le_of_isDenseInCubes {t d m : ℕ} {S : Set (Fin t → ℕ)}
    {a : Fin t → ℕ} (hd : 0 < d) (hS : S ⊆ latticeCube a m)
    (hdense : IsDenseInCubes d S (latticeCube a m)) : cubeGapSize S ≤ d

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Definition 5 (and Proof 1 of Theorem 2, "hence gs(S) ≤ d").

Uses 3

Statement usesDensity in subcubes · Gap size · Lattice cube

TheoremFinite sets in positive dimension have positive gap size#✓fully proved

Let \(t \ge 1\). Every finite set \(S \subseteq \mathbb{N}^t\) has gap size \(\operatorname{gs}(S) > 0\).

Indeed, \(S\) lies in some subcube \([0, m)^t\), and it is vacuously \((m + 1)\)-dense there, since no subcube of side \(m + 1\) fits inside.

public theorem cubeGapSize_pos {t : ℕ} (ht : 1 ≤ t) (S : Finset (Fin t → ℕ)) :
    0 < cubeGapSize (S : Set (Fin t → ℕ))

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Definition 5.

Uses 3

Statement usesGap size

Proof usesDensity in subcubes · Lattice cube

TheoremGap size of a singleton#✓fully proved

For every point \(x \in \mathbb{N}^t\), the one-point set \(\lbrace x \rbrace\) has gap size \(\operatorname{gs}(\lbrace x \rbrace) = 1\).

public theorem cubeGapSize_singleton {t : ℕ} (x : Fin t → ℕ) : cubeGapSize {x} = 1

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Definitions 1 and 5 ("If |S| = 1, we set gs(S) = 1").

Uses 5

Statement usesGap size

Proof usesDensity in subcubes · Density one means containment · Lattice cube · Lattice cube of side one

TheoremMonochromatic sets that are large relative to their gap size#●ready to prove

Let \(r, t \in \mathbb{N}\) with \(t \ge 1\), and let \(f : \mathbb{N} \to \mathbb{N}\) be nondecreasing. There is \(B \in \mathbb{N}\) such that for every coloring of \(\mathbb{N}^t\) with \(r\) colors there is a finite monochromatic set \(S \subseteq [1, B]^t\) with \(|S| > f(\operatorname{gs}(S))\), where \(\operatorname{gs}(S)\) is the gap size of \(S\) and \([1, B]^t\) is the set of points \(x\) with \(1 \le x_i \le B\) for every coordinate \(i\).

The paper's "(a smallest)" is omitted: it follows from existence. Only the restriction of the coloring to \([1, B]^t\) matters. The hypothesis \(t \ge 1\) is the paper's; for \(t = 0\) and \(r \ge 1\) the statement fails when \(f(1) \ge 1\), since the only point gives \(|S| = 1 = \operatorname{gs}(S)\). The paper's hypothesis \(r \ge 1\) is dropped: for \(r = 0\) there is no coloring and the statement holds vacuously.

public theorem_wanted exists_cube_bound_monochromatic_card_gt_gapSize (r t : ℕ) (ht : 1 ≤ t)
    (f : ℕ → ℕ) (hf : Monotone f) :
    ∃ B : ℕ, ∀ c : (Fin t → ℕ) → Fin r, ∃ j : Fin r, ∃ S : Finset (Fin t → ℕ),
      (S : Set (Fin t → ℕ)) ⊆ latticeCube (fun _ => 1) B ∧ (∀ x ∈ S, c x = j) ∧
        f (cubeGapSize (S : Set (Fin t → ℕ))) < S.card

Sources

• Tom C. Brown, Piecewise Syndetic Sets in N^t and N^X, INTEGERS 24 (2024), Article A2, Theorem 2.

Uses 2

Statement usesGap size · Lattice cube

12 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.