Hindman's theorem on finite sums #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 theoremexists_FS_of_finite_cover: the weak form of Hindman's theorem
Tags #
Ramsey theory, ultrafilter
Multiplication of ultrafilters given by ∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m').
Equations
- ultrafilter.has_mul = {mul := λ (U V : ultrafilter M), has_mul.mul <$> U <*> V}
Addition of ultrafilters given by
∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m').
Equations
- ultrafilter.has_add = {add := λ (U V : ultrafilter M), has_add.add <$> U <*> V}
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
- head : ∀ {M : Type u_1} [_inst_1 : add_semigroup M] (a : stream M), hindman.FS a a.head
- tail : ∀ {M : Type u_1} [_inst_1 : add_semigroup M] (a : stream M) (m : M), hindman.FS a.tail m → hindman.FS a m
- cons : ∀ {M : Type u_1} [_inst_1 : add_semigroup M] (a : stream M) (m : M), hindman.FS a.tail m → hindman.FS a (a.head + 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.
- head : ∀ {M : Type u_1} [_inst_1 : semigroup M] (a : stream M), hindman.FP a a.head
- tail : ∀ {M : Type u_1} [_inst_1 : semigroup M] (a : stream M) (m : M), hindman.FP a.tail m → hindman.FP a m
- cons : ∀ {M : Type u_1} [_inst_1 : semigroup M] (a : stream M) (m : M), hindman.FP a.tail m → hindman.FP a (a.head * 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.
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.
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.
The strong form of Hindman's theorem: in any finite cover of an FS-set, one the parts contains an FS-set.
The strong form of Hindman's theorem: in any finite cover of an FP-set, one the parts contains an FP-set.
The weak form of Hindman's theorem: in any finite cover of a nonempty additive semigroup, one of the parts contains an FS-set.