Skip to content

Density Hales–Jewett theorem

10 fully proved

Line

DefinitionReindexing a combinatorial line#✓fully proved

A combinatorial line \(l\) in \(\alpha^\iota\) assigns to each coordinate \(i \in \iota\) either a fixed value in \(\alpha\) or the free variable, with at least one free coordinate. Given a bijection \(e : \iota \to \iota'\), the reindexing of \(l\) along \(e\) is the combinatorial line in \(\alpha^{\iota'}\) that assigns to each coordinate \(j \in \iota'\) what \(l\) assigns to the coordinate \(e^{-1}(j)\).

public def reindex (l : Line α ι) (e : ι ≃ ι') : Line α ι' where
  idxFun i := l.idxFun (e.symm i)
  proper := by
    obtain ⟨i, hi⟩ := l.proper
    exact ⟨e i, by simpa⟩
Used by 4
Used byDensity Hales–Jewett theorem · Graham–Rothschild theorem for combinatorial lines · Points of a reindexed line · Reindexing commutes with images of lines

TheoremPoints of a reindexed line#✓fully proved

Let \(l\) be a combinatorial line in \(\alpha^\iota\), let \(e : \iota \to \iota'\) be a bijection, and for \(a \in \alpha\) write \(l(a) \in \alpha^\iota\) for the point of \(l\) whose free coordinates equal \(a\). Then for every \(a \in \alpha\) and every \(j \in \iota'\), the \(j\)-th coordinate of the point at \(a\) of the reindexing of \(l\) along \(e\) equals the \(e^{-1}(j)\)-th coordinate of \(l(a)\).

@[simp]
public theorem reindex_apply (l : Line α ι) (e : ι ≃ ι') (a : α) (i : ι') :
    l.reindex e a i = l a (e.symm i)
Uses 1 · Used by 1
Statement usesReindexing a combinatorial line
Used byDensity Hales–Jewett theorem

Subspace

DefinitionComposition of combinatorial subspaces#✓fully proved

A combinatorial subspace \(V\) of \(\alpha^\iota\) with parameter set \(\eta\) assigns to each coordinate \(i \in \iota\) either a fixed value in \(\alpha\) or a parameter in \(\eta\), with every parameter assigned to some coordinate. Let \(V\) be such a subspace and let \(W\) be a combinatorial subspace of \(\alpha^\eta\) with parameter set \(\eta'\). The composite \(V \circ W\) is the combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta'\) that assigns to a coordinate \(i\) the fixed value \(a\) if \(V\) assigns \(a\) to \(i\), and assigns to \(i\) what \(W\) assigns to the coordinate \(e \in \eta\) if \(V\) assigns the parameter \(e\) to \(i\).

public def comp (V : Subspace η α ι) (W : Subspace η' α η) : Subspace η' α ι where
  idxFun i := (V.idxFun i).elim Sum.inl W.idxFun
  proper e := by
    obtain ⟨j, hj⟩ := W.proper e
    obtain ⟨i, hi⟩ := V.proper j
    exact ⟨i, by simp [hi, hj]⟩
Used by 4
Used byEvaluating a composite subspace · Images of lines under composite subspaces · Density Hales–Jewett theorem · Graham–Rothschild theorem for combinatorial lines

TheoremEvaluating a composite subspace#✓fully proved

Let \(V\) be a combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta\) and let \(W\) be a combinatorial subspace of \(\alpha^\eta\) with parameter set \(\eta'\); view each subspace as its map from parameter values to points. Then for every \(x \in \alpha^{\eta'}\), the composite \(V \circ W\) sends \(x\) to \(V(W(x))\).

@[simp]
public theorem comp_apply (V : Subspace η α ι) (W : Subspace η' α η) (x : η' → α) :
    V.comp W x = V (W x)
Uses 1 · Used by 1
Statement usesComposition of combinatorial subspaces
Used byDensity Hales–Jewett theorem

DefinitionImage of a combinatorial line in a combinatorial subspace#✓fully proved

Let \(V\) be a combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta\) and let \(l\) be a combinatorial line in \(\alpha^\eta\). The image \(V_* l\) is the combinatorial line in \(\alpha^\iota\) that has the fixed value \(a\) at each coordinate \(i\) to which \(V\) assigns the fixed value \(a\), and has at each coordinate \(i\) to which \(V\) assigns a parameter \(e \in \eta\) what \(l\) has at the coordinate \(e\) (the free variable or a fixed value).

public def compLine (V : Subspace η α ι) (l : Combinatorics.Line α η) :
    Combinatorics.Line α ι where
  idxFun i := (V.idxFun i).elim some l.idxFun
  proper := by
    obtain ⟨e, he⟩ := l.proper
    obtain ⟨i, hi⟩ := V.proper e
    exact ⟨i, by simp [hi, he]⟩
Used by 5
Used byImages of lines under composite subspaces · Points of the image of a line · Density Hales–Jewett theorem · Graham–Rothschild theorem for combinatorial lines · Reindexing commutes with images of lines

TheoremPoints of the image of a line#✓fully proved

Let \(V\) be a combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta\), viewed as its map \(x \mapsto V(x)\) from parameter values to points, and let \(l\) be a combinatorial line in \(\alpha^\eta\), with \(l(a)\) the point of \(l\) whose free coordinates equal \(a\). Then for every \(a \in \alpha\), the point at \(a\) of the image line \(V_* l\) is \(V(l(a))\).

@[simp]
public theorem compLine_apply (V : Subspace η α ι) (l : Combinatorics.Line α η) (a : α) :
    V.compLine l a = V (l a)
Uses 1 · Used by 1
Statement usesImage of a combinatorial line in a combinatorial subspace
Used byDensity Hales–Jewett theorem

TheoremReindexing commutes with images of lines#✓fully proved

Let \(V\) be a combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta\), let \(e : \iota \to \iota'\) be a bijection, and let \(l\) be a combinatorial line in \(\alpha^\eta\). Let \(V^e\) be the combinatorial subspace of \(\alpha^{\iota'}\) with parameter set \(\eta\) that assigns to each coordinate \(j \in \iota'\) what \(V\) assigns to the coordinate \(e^{-1}(j)\). Then the image of \(l\) under \(V^e\) is the reindexing along \(e\) of the image of \(l\) under \(V\).

@[simp]
public theorem reindex_compLine (V : Subspace η α ι) (e : ι ≃ ι')
    (l : Combinatorics.Line α η) :
    (V.reindex (Equiv.refl η) (Equiv.refl α) e).compLine l = (V.compLine l).reindex e
Uses 2 · Used by 1
Statement usesReindexing a combinatorial line · Image of a combinatorial line in a combinatorial subspace
Used byGraham–Rothschild theorem for combinatorial lines

TheoremImages of lines under composite subspaces#✓fully proved

Let \(V\) be a combinatorial subspace of \(\alpha^\iota\) with parameter set \(\eta\), let \(W\) be a combinatorial subspace of \(\alpha^\eta\) with parameter set \(\eta'\), and let \(l\) be a combinatorial line in \(\alpha^{\eta'}\). Then the image of \(l\) under the composite \(V \circ W\) equals the image under \(V\) of the image of \(l\) under \(W\), that is, \((V \circ W)_* l = V_*(W_* l)\).

@[simp]
public theorem comp_compLine (V : Subspace η α ι) (W : Subspace η' α η)
    (l : Combinatorics.Line α η') :
    (V.comp W).compLine l = V.compLine (W.compLine l)
Uses 2 · Used by 2
Statement usesComposition of combinatorial subspaces · Image of a combinatorial line in a combinatorial subspace
Used byDensity Hales–Jewett theorem · Graham–Rothschild theorem for combinatorial lines

Density Hales–Jewett theorem

TheoremGraham–Rothschild theorem for combinatorial lines#✓fully proved

Let \(\alpha\) be a finite nonempty alphabet, let \(\kappa\) be a finite nonempty set of colors and let \(m\) be a natural number. Then there is a natural number \(N\) such that for every coloring \(C\) of the combinatorial lines in \(\alpha^N\) with colors in \(\kappa\) there are a combinatorial subspace \(V\) of \(\alpha^N\) with parameter set \(\{0, \dots, m - 1\}\) and a color \(z \in \kappa\) such that for every combinatorial line \(l\) in \(\alpha^m\), the image \(V_* l\) of \(l\) in \(V\) satisfies \(C(V_* l) = z\).

public theorem _root_.Combinatorics.Subspace.exists_lines_mono_in_high_dimension_fin
    (α : Type u) (κ : Type v) [Finite α] [Nonempty α] [Finite κ] [Nonempty κ] (m : ℕ) :
    ∃ N : ℕ, ∀ C : Combinatorics.Line α (Fin N) → κ,
      ∃ V : Combinatorics.Subspace (Fin m) α (Fin N), ∃ z : κ,
        ∀ l : Combinatorics.Line α (Fin m), C (V.compLine l) = z
Uses 5 · Used by 1
Statement usesImage of a combinatorial line in a combinatorial subspace
Proof usesReindexing a combinatorial line · Composition of combinatorial subspaces · Images of lines under composite subspaces · Reindexing commutes with images of lines
Used byDensity Hales–Jewett theorem

TheoremDensity Hales–Jewett theorem#✓fully proved

Write \([k] = \{0, 1, \dots, k - 1\}\). A combinatorial line in \([k]^N\) is given by a nonempty set of free coordinates and a fixed value in \([k]\) at every other coordinate; its \(k\) points are obtained by giving all free coordinates a common value \(a \in [k]\). For every natural number \(k \ge 2\) and every real \(\delta > 0\) there is a natural number \(N\) such that every set \(A \subseteq [k]^N\) with \(\delta k^N \le |A|\) contains all \(k\) points of some combinatorial line in \([k]^N\).

Proof: We follow the density-increment route of Dodos–Kanellopoulos–Tyros, with the binary case supplied by Sperner's theorem and the Graham–Rothschild theorem for lines.

public theorem density_hales_jewett :
    ∀ k : ℕ, 2 ≤ k → ∀ δ : ℝ, 0 < δ → ∃ N : ℕ,
      ∀ A : Finset (Fin N → Fin k),
        δ * ((k : ℝ) ^ N) ≤ (A.card : ℝ) →
          ∃ l : Combinatorics.Line (Fin k) (Fin N), ∀ a : Fin k, l a ∈ A
Sources
  • H. Furstenberg and Y. Katznelson, J. Anal. Math. 57 (1991) and Hales-Jewett, Trans. AMS 106 (1963); Lean states finitary density form over Fin N → Fin k with coloring version as corollary.
Uses 8 · Used by 1
Proof usesReindexing a combinatorial line · Points of a reindexed line · Composition of combinatorial subspaces · Image of a combinatorial line in a combinatorial subspace · Points of the image of a line · Evaluating a composite subspace · Images of lines under composite subspaces · Graham–Rothschild theorem for combinatorial lines
Used bySzemerédi's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.