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

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

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

Equations

• Ultrafilter.mul = { mul := fun (U V : Ultrafilter M) => (fun (x1 x2 : M) => x1 * x2) <$> U <*> V }

def Ultrafilter.add {M : Type u_1} [Add M] : Add (Ultrafilter M)

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

Equations

• Ultrafilter.add = { add := fun (U V : Ultrafilter M) => (fun (x1 x2 : M) => x1 + x2) <$> U <*> V }

theorem Ultrafilter.eventually_mul {M : Type u_1} [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} [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 (Ultrafilter M)

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

Equations

• Ultrafilter.semigroup = { toMul := Ultrafilter.mul, mul_assoc := ⋯ }

def Ultrafilter.addSemigroup {M : Type u_1} [AddSemigroup M] : AddSemigroup (Ultrafilter M)

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

Equations

• Ultrafilter.addSemigroup = { toAdd := Ultrafilter.add, add_assoc := ⋯ }

theorem Ultrafilter.continuous_mul_left {M : Type u_1} [Mul M] (V : Ultrafilter M) : Continuous fun (x : Ultrafilter M) => x * V

theorem Ultrafilter.continuous_add_left {M : Type u_1} [Add M] (V : Ultrafilter M) : Continuous fun (x : Ultrafilter M) => x + V

inductive Hindman.FS {M : Type u_1} [AddSemigroup M] : Stream' M → Set 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} [AddSemigroup M] (a : Stream' M) : FS a a.head
• tail' {M : Type u_1} [AddSemigroup M] (a : Stream' M) (m : M) (h : FS a.tail m) : FS a m
• cons' {M : Type u_1} [AddSemigroup M] (a : Stream' M) (m : M) (h : FS a.tail m) : FS a (a.head + m)

inductive Hindman.FP {M : Type u_1} [Semigroup M] : Stream' M → Set 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.

• head' {M : Type u_1} [Semigroup M] (a : Stream' M) : FP a a.head
• tail' {M : Type u_1} [Semigroup M] (a : Stream' M) (m : M) (h : FP a.tail m) : FP a m
• cons' {M : Type u_1} [Semigroup M] (a : Stream' M) (m : M) (h : FP a.tail m) : FP a (a.head * m)

Since the constructors for FS and FP cheat using the Set M = M → Prop defeq, we provide match patterns that preserve the defeq correctly in their type.

@[reducible, match_pattern, inline]

abbrev Hindman.FP.head {M : Type u_1} [Semigroup M] (a : Stream' M) : a.head ∈ FP a

Constructor for FP. This is the preferred spelling over FP.head'.

Equations

• ⋯ = ⋯

@[reducible, match_pattern, inline]

abbrev Hindman.FS.head {M : Type u_1} [AddSemigroup M] (a : Stream' M) : a.head ∈ FS a

Constructor for FS. This is the preferred spelling over FS.head'.

Equations

• ⋯ = ⋯

@[reducible, match_pattern, inline]

abbrev Hindman.FP.tail {M : Type u_1} [Semigroup M] (a : Stream' M) (m : M) (h : FP a.tail m) : m ∈ FP a

Constructor for FP. This is the preferred spelling over FP.tail'.

Equations

• ⋯ = ⋯

@[reducible, match_pattern, inline]

abbrev Hindman.FS.tail {M : Type u_1} [AddSemigroup M] (a : Stream' M) (m : M) (h : FS a.tail m) : m ∈ FS a

Constructor for FS. This is the preferred spelling over FS.tail'.

Equations

• ⋯ = ⋯

@[reducible, match_pattern, inline]

abbrev Hindman.FP.cons {M : Type u_1} [Semigroup M] (a : Stream' M) (m : M) (h : FP a.tail m) : a.head * m ∈ FP a

Constructor for FP. This is the preferred spelling over FP.cons'.

Equations

• ⋯ = ⋯

@[reducible, match_pattern, inline]

abbrev Hindman.FS.cons {M : Type u_1} [AddSemigroup M] (a : Stream' M) (m : M) (h : FS a.tail m) : a.head + m ∈ FS a

Constructor for FS. This is the preferred spelling over FS.cons'.

Equations

• ⋯ = ⋯

theorem Hindman.FP.mul {M : Type u_1} [Semigroup M] {a : Stream' M} {m : M} (hm : m ∈ FP a) : ∃ (n : ℕ), ∀ m' ∈ FP (Stream'.drop n a), m * m' ∈ 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.FS.add {M : Type u_1} [AddSemigroup M] {a : Stream' M} {m : M} (hm : m ∈ FS a) : ∃ (n : ℕ), ∀ m' ∈ FS (Stream'.drop n a), m + m' ∈ FS a

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.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 ∈ FP a

theorem Hindman.exists_idempotent_ultrafilter_le_FS {M : Type u_1} [AddSemigroup M] (a : Stream' M) : ∃ (U : Ultrafilter M), U + U = U ∧ ∀ᶠ (m : M) in ↑U, m ∈ 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), FP a ⊆ s₀

theorem Hindman.exists_FS_of_large {M : Type u_1} [AddSemigroup M] (U : Ultrafilter M) (U_idem : U + U = U) (s₀ : Set M) (sU : s₀ ∈ U) : ∃ (a : Stream' M), FS a ⊆ s₀

theorem Hindman.FP_partition_regular {M : Type u_1} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : FP a ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ (b : Stream' M), 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.FS_partition_regular {M : Type u_1} [AddSemigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : FS a ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ (b : Stream' M), FS 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.exists_FP_of_finite_cover {M : Type u_1} [Semigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : ⊤ ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ (a : Stream' M), 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.exists_FS_of_finite_cover {M : Type u_1} [AddSemigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : ⊤ ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ (a : Stream' M), FS 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.

theorem Hindman.FP_drop_subset_FP {M : Type u_1} [Semigroup M] (a : Stream' M) (n : ℕ) : FP (Stream'.drop n a) ⊆ FP a

theorem Hindman.FS_iter_tail_sub_FS {M : Type u_1} [AddSemigroup M] (a : Stream' M) (n : ℕ) : FS (Stream'.drop n a) ⊆ FS a

theorem Hindman.FP.singleton {M : Type u_1} [Semigroup M] (a : Stream' M) (i : ℕ) : a.get i ∈ FP a

theorem Hindman.FS.singleton {M : Type u_1} [AddSemigroup M] (a : Stream' M) (i : ℕ) : a.get i ∈ FS a

theorem Hindman.FP.mul_two {M : Type u_1} [Semigroup M] (a : Stream' M) (i j : ℕ) (ij : i < j) : a.get i * a.get j ∈ FP a

theorem Hindman.FS.add_two {M : Type u_1} [AddSemigroup M] (a : Stream' M) (i j : ℕ) (ij : i < j) : a.get i + a.get j ∈ FS a

theorem Hindman.FP.finset_prod {M : Type u_1} [CommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) : ∏ i ∈ s, a.get i ∈ FP a

theorem Hindman.FS.finset_sum {M : Type u_1} [AddCommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) : ∑ i ∈ s, a.get i ∈ FS a