# Documentation

Mathlib.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 #

• FS_partition_regular: the strong form of Hindman's theorem
• exists_FS_of_finite_cover: the weak form of Hindman's theorem

## Tags #

Ramsey theory, ultrafilter

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

Instances For
def Ultrafilter.mul {M : Type u_1} [Mul M] :
Mul ()

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

Instances For
theorem Ultrafilter.eventually_add {M : Type u_1} [Add M] (U : ) (V : ) (p : MProp) :
(∀ᶠ (m : M) in ↑(U + V), p m) ∀ᶠ (m : M) in U, ∀ᶠ (m' : M) in V, p (m + m')
theorem Ultrafilter.eventually_mul {M : Type u_1} [Mul M] (U : ) (V : ) (p : MProp) :
(∀ᶠ (m : M) in ↑(U * V), p m) ∀ᶠ (m : M) in U, ∀ᶠ (m' : M) in V, p (m * m')
def Ultrafilter.addSemigroup {M : Type u_1} [] :

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

Instances For
theorem Ultrafilter.addSemigroup.proof_1 {M : Type u_1} [] (U : ) (V : ) (W : ) :
U + V + W = U + (V + W)
def Ultrafilter.semigroup {M : Type u_1} [] :

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

Instances For
theorem Ultrafilter.continuous_add_left {M : Type u_1} [] (V : ) :
Continuous fun x => x + V
theorem Ultrafilter.continuous_mul_left {M : Type u_1} [] (V : ) :
Continuous fun x => x * V
inductive Hindman.FS {M : Type u_1} [] :
Set M
• head: ∀ {M : Type u_1} [inst : ] (a : ),
• tail: ∀ {M : Type u_1} [inst : ] (a : ) (m : M),
• cons: ∀ {M : Type u_1} [inst : ] (a : ) (m : M), Hindman.FS a ()

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.

Instances For
inductive Hindman.FP {M : Type u_1} [] :
Set M
• head: ∀ {M : Type u_1} [inst : ] (a : ),
• tail: ∀ {M : Type u_1} [inst : ] (a : ) (m : M),
• cons: ∀ {M : Type u_1} [inst : ] (a : ) (m : M), Hindman.FP a ()

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.

Instances For
theorem Hindman.FS.add {M : Type u_1} [] {a : } {m : M} (hm : m ) :
n, ∀ (m' : M), m' Hindman.FS ()m + m'

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

theorem Hindman.FP.mul {M : Type u_1} [] {a : } {m : M} (hm : m ) :
n, ∀ (m' : M), m' Hindman.FP ()m * m'

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_FS {M : Type u_1} [] (a : ) :
U, U + U = U ∀ᶠ (m : M) in U, m
theorem Hindman.exists_idempotent_ultrafilter_le_FP {M : Type u_1} [] (a : ) :
U, U * U = U ∀ᶠ (m : M) in U, m
theorem Hindman.exists_FS_of_large {M : Type u_1} [] (U : ) (U_idem : U + U = U) (s₀ : Set M) (sU : s₀ U) :
a, s₀
theorem Hindman.exists_FP_of_large {M : Type u_1} [] (U : ) (U_idem : U * U = U) (s₀ : Set M) (sU : s₀ U) :
a, s₀
abbrev Hindman.FS_partition_regular.match_1 {M : Type u_1} (s : Set (Set M)) (U : ) (motive : (t, t s t U) → Prop) :
(x : t, t s t U) → ((c : Set M) → (cs : c s) → (hc : c U) → motive (_ : t, t s t U)) → motive x
Instances For
abbrev Hindman.FS_partition_regular.match_2 {M : Type u_1} [] (a : ) (motive : (U, U + U = U ∀ᶠ (m : M) in U, m ) → Prop) :
(x : U, U + U = U ∀ᶠ (m : M) in U, m ) → ((U : ) → (idem : U + U = U) → (aU : ∀ᶠ (m : M) in U, m ) → motive (_ : U, U + U = U ∀ᶠ (m : M) in U, m )) → motive x
Instances For
theorem Hindman.FS_partition_regular {M : Type u_1} [] (a : ) (s : Set (Set M)) (sfin : ) (scov : ⋃₀ s) :
c, c s b, c

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

theorem Hindman.FP_partition_regular {M : Type u_1} [] (a : ) (s : Set (Set M)) (sfin : ) (scov : ⋃₀ s) :
c, c s 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} [] [] (s : Set (Set M)) (sfin : ) (scov : ⋃₀ s) :
c, c s a, c

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

abbrev Hindman.exists_FS_of_finite_cover.match_1 {M : Type u_1} [] (motive : (m, m + m = m) → Prop) :
(x : m, m + m = m) → ((U : ) → (hU : U + U = U) → motive (_ : m, m + m = m)) → motive x
Instances For
theorem Hindman.exists_FP_of_finite_cover {M : Type u_1} [] [] (s : Set (Set M)) (sfin : ) (scov : ⋃₀ s) :
c, c s 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.FS_iter_tail_sub_FS {M : Type u_1} [] (a : ) (n : ) :
theorem Hindman.FP_drop_subset_FP {M : Type u_1} [] (a : ) (n : ) :
theorem Hindman.FS.singleton {M : Type u_1} [] (a : ) (i : ) :
theorem Hindman.FP.singleton {M : Type u_1} [] (a : ) (i : ) :
theorem Hindman.FS.add_two {M : Type u_1} [] (a : ) (i : ) (j : ) (ij : i < j) :
+
theorem Hindman.FP.mul_two {M : Type u_1} [] (a : ) (i : ) (j : ) (ij : i < j) :
*
theorem Hindman.FS.finset_sum {M : Type u_1} [] (a : ) (s : ) (hs : ) :
(Finset.sum s fun i => )
theorem Hindman.FP.finset_prod {M : Type u_1} [] (a : ) (s : ) (hs : ) :
(Finset.prod s fun i => )