mathlib3 documentation

combinatorics.hales_jewett

The Hales-Jewett theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove the Hales-Jewett theorem and deduce Van der Waerden's theorem as a corollary.

The Hales-Jewett theorem is a result in Ramsey theory dealing with combinatorial lines. Given an 'alphabet' α : Type* and a b : α, an example of a combinatorial line in α^5 is { (a, x, x, b, x) | x : α }. See combinatorics.line for a precise general definition. The Hales-Jewett theorem states that for any fixed finite types α and κ, there exists a (potentially huge) finite type ι such that whenever ι → α is κ-colored (i.e. for any coloring C : (ι → α) → κ), there exists a monochromatic line. We prove the Hales-Jewett theorem using the idea of color focusing and a product argument. See the proof of combinatorics.line.exists_mono_in_high_dimension' for details.

The version of Van der Waerden's theorem in this file states that whenever a commutative monoid M is finitely colored and S is a finite subset, there exists a monochromatic homothetic copy of S. This follows from the Hales-Jewett theorem by considering the map (ι → S) → M sending v to ∑ i : ι, v i, which sends a combinatorial line to a homothetic copy of S.

Main results #

combinatorics.line.exists_mono_in_high_dimension: the Hales-Jewett theorem.
combinatorics.exists_mono_homothetic_copy: a generalization of Van der Waerden's theorem.

Implementation details #

For convenience, we work directly with finite types instead of natural numbers. That is, we write α, ι, κ for (finite) types where one might traditionally use natural numbers n, H, c. This allows us to work directly with α, option α, (ι → α) → κ, and ι ⊕ ι' instead of fin n, fin (n+1), fin (c^(n^H)), and fin (H + H').

Todo #

Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the current proof).
One could reformulate the proof of Hales-Jewett to give explicit upper bounds on the number of coordinates needed.

Tags #

combinatorial line, Ramsey theory, arithmetic progession

References #

https://en.wikipedia.org/wiki/Hales%E2%80%93Jewett_theorem

structure combinatorics.line (α : Type u_1) (ι : Type u_2) :

Type (max u_1 u_2)

idx_fun : ι → option α
proper : ∃ (i : ι), self.idx_fun i = option.none

The type of combinatorial lines. A line l : line α ι in the hypercube ι → α defines a function α → ι → α from α to the hypercube, such that for each coordinate i : ι, the function λ x, l x i is either id or constant. We require lines to be nontrivial in the sense that λ x, l x i is id for at least one i.

Formally, a line is represented by the function l.idx_fun : ι → option α which says whether λ x, l x i is id (corresponding to l.idx_fun i = none) or constantly y (corresponding to l.idx_fun i = some y).

When α has size 1 there can be many elements of line α ι defining the same function.

Instances for combinatorics.line

@[protected, instance]

def combinatorics.line.has_coe_to_fun (α : Type u_1) (ι : Type u_2) :

has_coe_to_fun (combinatorics.line α ι) (λ (_x : combinatorics.line α ι), α → ι → α)

Equations

combinatorics.line.has_coe_to_fun α ι = {coe := λ (l : combinatorics.line α ι) (x : α) (i : ι), (l.idx_fun i).get_or_else x}

def combinatorics.line.is_mono {α : Type u_1} {ι : Type u_2} {κ : Sort u_3} (C : (ι → α) → κ) (l : combinatorics.line α ι) :

Prop

A line is monochromatic if all its points are the same color.

Equations

combinatorics.line.is_mono C l = ∃ (c : κ), ∀ (x : α), C (⇑l x) = c

def combinatorics.line.diagonal (α : Type u_1) (ι : Type u_2) [nonempty ι] :

combinatorics.line α ι

The diagonal line. It is the identity at every coordinate.

Equations

combinatorics.line.diagonal α ι = {idx_fun := λ (_x : ι), option.none, proper := _}

@[protected, instance]

def combinatorics.line.inhabited (α : Type u_1) (ι : Type u_2) [nonempty ι] :

inhabited (combinatorics.line α ι)

Equations

combinatorics.line.inhabited α ι = {default := combinatorics.line.diagonal α ι _inst_1}

structure combinatorics.line.almost_mono {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :

Type (max u_1 u_2 u_3)

line : combinatorics.line (option α) ι
color : κ
has_color : ∀ (x : α), C (⇑(self.line) (option.some x)) = self.color

The type of lines that are only one color except possibly at their endpoints.

Instances for combinatorics.line.almost_mono

combinatorics.line.almost_mono.has_sizeof_inst
combinatorics.line.almost_mono.inhabited

@[protected, instance]

def combinatorics.line.almost_mono.inhabited {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [nonempty ι] [inhabited κ] :

inhabited (combinatorics.line.almost_mono (λ (v : ι → option α), inhabited.default))

Equations

combinatorics.line.almost_mono.inhabited = {default := {line := inhabited.default (combinatorics.line.inhabited (option α) ι), color := inhabited.default _inst_2, has_color := _}}

structure combinatorics.line.color_focused {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :

Type (max u_1 u_2 u_3)

lines : multiset (combinatorics.line.almost_mono C)
focus : ι → option α
is_focused : ∀ (p : combinatorics.line.almost_mono C), p ∈ self.lines → ⇑(p.line) option.none = self.focus
distinct_colors : (multiset.map combinatorics.line.almost_mono.color self.lines).nodup

The type of collections of lines such that

each line is only one color except possibly at its endpoint
the lines all have the same endpoint
the colors of the lines are distinct. Used in the proof exists_mono_in_high_dimension.

Instances for combinatorics.line.color_focused

combinatorics.line.color_focused.has_sizeof_inst
combinatorics.line.color_focused.inhabited

@[protected, instance]

def combinatorics.line.color_focused.inhabited {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (C : (ι → option α) → κ) :

inhabited (combinatorics.line.color_focused C)

Equations

combinatorics.line.color_focused.inhabited C = {default := {lines := 0, focus := λ (_x : ι), option.none, is_focused := _, distinct_colors := _}}

def combinatorics.line.map {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : combinatorics.line α ι) :

combinatorics.line α' ι

A function f : α → α' determines a function line α ι → line α' ι. For a coordinate i, l.map f is the identity at i if l is, and constantly f y if l is constantly y at i.

Equations

combinatorics.line.map f l = {idx_fun := λ (i : ι), option.map f (l.idx_fun i), proper := _}

def combinatorics.line.vertical {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ι → α) (l : combinatorics.line α ι') :

combinatorics.line α (ι ⊕ ι')

A point in ι → α and a line in ι' → α determine a line in ι ⊕ ι' → α.

Equations

combinatorics.line.vertical v l = {idx_fun := sum.elim (option.some ∘ v) l.idx_fun, proper := _}

def combinatorics.line.horizontal {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (v : ι' → α) :

combinatorics.line α (ι ⊕ ι')

A line in ι → α and a point in ι' → α determine a line in ι ⊕ ι' → α.

Equations

l.horizontal v = {idx_fun := sum.elim l.idx_fun (option.some ∘ v), proper := _}

def combinatorics.line.prod {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (l' : combinatorics.line α ι') :

combinatorics.line α (ι ⊕ ι')

One line in ι → α and one in ι' → α together determine a line in ι ⊕ ι' → α.

Equations

l.prod l' = {idx_fun := sum.elim l.idx_fun l'.idx_fun, proper := _}

theorem combinatorics.line.apply {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) :

⇑l x = λ (i : ι), (l.idx_fun i).get_or_else x

theorem combinatorics.line.apply_none {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) (i : ι) (h : l.idx_fun i = option.none) :

⇑l x i = x

theorem combinatorics.line.apply_of_ne_none {α : Type u_1} {ι : Type u_2} (l : combinatorics.line α ι) (x : α) (i : ι) (h : l.idx_fun i ≠ option.none) :

option.some (⇑l x i) = l.idx_fun i

@[simp]

theorem combinatorics.line.map_apply {α : Type u_1} {α' : Type u_2} {ι : Type u_3} (f : α → α') (l : combinatorics.line α ι) (x : α) :

⇑(combinatorics.line.map f l) (f x) = f ∘ ⇑l x

@[simp]

theorem combinatorics.line.vertical_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (v : ι → α) (l : combinatorics.line α ι') (x : α) :

⇑(combinatorics.line.vertical v l) x = sum.elim v (⇑l x)

@[simp]

theorem combinatorics.line.horizontal_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (v : ι' → α) (x : α) :

⇑(l.horizontal v) x = sum.elim (⇑l x) v

@[simp]

theorem combinatorics.line.prod_apply {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (l : combinatorics.line α ι) (l' : combinatorics.line α ι') (x : α) :

⇑(l.prod l') x = sum.elim (⇑l x) (⇑l' x)

@[simp]

theorem combinatorics.line.diagonal_apply {α : Type u_1} {ι : Type u_2} [nonempty ι] (x : α) :

⇑(combinatorics.line.diagonal α ι) x = λ (i : ι), x

theorem combinatorics.line.exists_mono_in_high_dimension (α : Type u) [finite α] (κ : Type v) [finite κ] :

∃ (ι : Type) [_inst_3 : fintype ι], ∀ (C : (ι → α) → κ), ∃ (l : combinatorics.line α ι), combinatorics.line.is_mono C l

The Hales-Jewett theorem: for any finite types α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial line.

theorem combinatorics.exists_mono_homothetic_copy {M : Type u_1} {κ : Type u_2} [add_comm_monoid M] (S : finset M) [finite κ] (C : M → κ) :

∃ (a : ℕ) (H : a > 0) (b : M) (c : κ), ∀ (s : M), s ∈ S → C (a • s + b) = c

A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.