mathlib documentation

combinatorics.hindman

Hindman's theorem on finite sums #

We prove Hindman's theorem on finite sums, using idempotent ultrafilters.

Given an infinite sequence a₀, a₁, a₂, … of positive integers, the set FS(a₀, …) is the set of positive integers that can be expressed as a finite sum of aᵢ's, without repetition. Hindman's theorem asserts that whenever the positive integers are finitely colored, there exists a sequence a₀, a₁, a₂, … such that FS(a₀, …) is monochromatic. There is also a stronger version, saying that whenever a set of the form FS(a₀, …) is finitely colored, there exists a sequence b₀, b₁, b₂, … such that FS(b₀, …) is monochromatic and contained in FS(a₀, …). We prove both these versions for a general semigroup M instead of ℕ+ since it is no harder, although this special case implies the general case.

The idea of the proof is to extend the addition (+) : M → M → M to addition (+) : βM → βM → βM on the space βM of ultrafilters on M. One can prove that if U is an idempotent ultrafilter, i.e. U + U = U, then any U-large subset of M contains some set FS(a₀, …) (see exists_FS_of_large). And with the help of a general topological argument one can show that any set of the form FS(a₀, …) is U-large according to some idempotent ultrafilter U (see exists_idempotent_ultrafilter_le_FS). This is enough to prove the theorem since in any finite partition of a U-large set, one of the parts is U-large.

Main results #

Tags #

Ramsey theory, ultrafilter

def ultrafilter.has_mul {M : Type u_1} [has_mul M] :

Multiplication of ultrafilters given by ∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m').

Equations
def ultrafilter.has_add {M : Type u_1} [has_add M] :

Addition of ultrafilters given by ∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m').

Equations
theorem ultrafilter.eventually_mul {M : Type u_1} [has_mul M] (U V : ultrafilter M) (p : M → Prop) :
(∀ᶠ (m : M) in (U * V), p m) ∀ᶠ (m : M) in U, ∀ᶠ (m' : M) in V, p (m * m')
theorem ultrafilter.eventually_add {M : Type u_1} [has_add M] (U V : ultrafilter M) (p : M → Prop) :
(∀ᶠ (m : M) in (U + V), p m) ∀ᶠ (m : M) in U, ∀ᶠ (m' : M) in V, p (m + m')
def ultrafilter.semigroup {M : Type u_1} [semigroup M] :

Semigroup structure on ultrafilter M induced by a semigroup structure on M.

Equations

Additive semigroup structure on ultrafilter M induced by an additive semigroup structure on M.

Equations
theorem ultrafilter.continuous_add_left {M : Type u_1} [add_semigroup M] (V : ultrafilter M) :
continuous (λ (_x : ultrafilter M), _x + V)
theorem ultrafilter.continuous_mul_left {M : Type u_1} [semigroup M] (V : ultrafilter M) :
continuous (λ (_x : ultrafilter M), _x * V)
inductive hindman.FS {M : Type u_1} [add_semigroup M] :
stream Mset M

FS a is the set of finite sums in a, i.e. m ∈ FS a if m is the sum of a nonempty subsequence of a. We give a direct inductive definition instead of talking about subsequences.

inductive hindman.FP {M : Type u_1} [semigroup M] :
stream Mset M

FP a is the set of finite products in a, i.e. m ∈ FP a if m is the product of a nonempty subsequence of a. We give a direct inductive definition instead of talking about subsequences.

theorem hindman.FS.add {M : Type u_1} [add_semigroup M] {a : stream M} {m : M} (hm : m hindman.FS a) :
∃ (n : ), ∀ (m' : M), m' hindman.FS (stream.drop n a)m + m' hindman.FS a
theorem hindman.FP.mul {M : Type u_1} [semigroup M] {a : stream M} {m : M} (hm : m hindman.FP a) :
∃ (n : ), ∀ (m' : M), m' hindman.FP (stream.drop n a)m * m' hindman.FP a

If m and m' are finite products in M, then so is m * m', provided that m' is obtained from a subsequence of M starting sufficiently late.

theorem hindman.exists_idempotent_ultrafilter_le_FP {M : Type u_1} [semigroup M] (a : stream M) :
∃ (U : ultrafilter M), U * U = U ∀ᶠ (m : M) in U, m hindman.FP a
theorem hindman.exists_idempotent_ultrafilter_le_FS {M : Type u_1} [add_semigroup M] (a : stream M) :
∃ (U : ultrafilter M), U + U = U ∀ᶠ (m : M) in U, m hindman.FS a
theorem hindman.exists_FP_of_large {M : Type u_1} [semigroup M] (U : ultrafilter M) (U_idem : U * U = U) (s₀ : set M) (sU : s₀ U) :
∃ (a : stream M), hindman.FP a s₀
theorem hindman.exists_FS_of_large {M : Type u_1} [add_semigroup M] (U : ultrafilter M) (U_idem : U + U = U) (s₀ : set M) (sU : s₀ U) :
∃ (a : stream M), hindman.FS a s₀
theorem hindman.FS_partition_regular {M : Type u_1} [add_semigroup M] (a : stream M) (s : set (set M)) (sfin : s.finite) (scov : hindman.FS a ⋃₀ s) :
∃ (c : set M) (H : c s) (b : stream M), hindman.FS b c
theorem hindman.FP_partition_regular {M : Type u_1} [semigroup M] (a : stream M) (s : set (set M)) (sfin : s.finite) (scov : hindman.FP a ⋃₀ s) :
∃ (c : set M) (H : c s) (b : stream M), hindman.FP b c

The strong form of Hindman's theorem: in any finite cover of an FP-set, one the parts contains an FP-set.

theorem hindman.exists_FS_of_finite_cover {M : Type u_1} [add_semigroup M] [nonempty M] (s : set (set M)) (sfin : s.finite) (scov : ⋃₀ s) :
∃ (c : set M) (H : c s) (a : stream M), hindman.FS a c
theorem hindman.exists_FP_of_finite_cover {M : Type u_1} [semigroup M] [nonempty M] (s : set (set M)) (sfin : s.finite) (scov : ⋃₀ s) :
∃ (c : set M) (H : c s) (a : stream M), hindman.FP a c

The weak form of Hindman's theorem: in any finite cover of a nonempty semigroup, one of the parts contains an FP-set.

theorem hindman.FP_drop_subset_FP {M : Type u_1} [semigroup M] (a : stream M) (n : ) :
theorem hindman.FS_iter_tail_sub_FS {M : Type u_1} [add_semigroup M] (a : stream M) (n : ) :
theorem hindman.FS.singleton {M : Type u_1} [add_semigroup M] (a : stream M) (i : ) :
theorem hindman.FP.singleton {M : Type u_1} [semigroup M] (a : stream M) (i : ) :
theorem hindman.FP.mul_two {M : Type u_1} [semigroup M] (a : stream M) (i j : ) (ij : i < j) :
a.nth i * a.nth j hindman.FP a
theorem hindman.FS.add_two {M : Type u_1} [add_semigroup M] (a : stream M) (i j : ) (ij : i < j) :
a.nth i + a.nth j hindman.FS a
theorem hindman.FP.finset_prod {M : Type u_1} [comm_monoid M] (a : stream M) (s : finset ) (hs : s.nonempty) :
s.prod (λ (i : ), a.nth i) hindman.FP a
theorem hindman.FS.finset_sum {M : Type u_1} [add_comm_monoid M] (a : stream M) (s : finset ) (hs : s.nonempty) :
s.sum (λ (i : ), a.nth i) hindman.FS a