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 #

Tags #

Ramsey theory, ultrafilter

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

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

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

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

    Equations
    Instances For
      theorem Ultrafilter.eventually_add {M : Type u_1} [Add M] (U : Ultrafilter M) (V : Ultrafilter M) (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 : Ultrafilter M) (V : Ultrafilter M) (p : MProp) :
      (∀ᶠ (m : M) in (U * V), p m) ∀ᶠ (m : M) in U, ∀ᶠ (m' : M) in V, p (m * m')

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

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

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

        Equations
        • Ultrafilter.semigroup = let __src := Ultrafilter.mul; Semigroup.mk
        Instances For
          theorem Ultrafilter.continuous_mul_left {M : Type u_1} [Semigroup M] (V : Ultrafilter M) :
          Continuous fun (x : Ultrafilter M) => x * V
          inductive Hindman.FS {M : Type u_1} [AddSemigroup 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.

          Instances For
            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.

            Instances For
              theorem Hindman.FS.add {M : Type u_1} [AddSemigroup M] {a : Stream' M} {m : M} (hm : m Hindman.FS a) :
              ∃ (n : ), m'Hindman.FS (Stream'.drop n a), m + m' Hindman.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.FP.mul {M : Type u_1} [Semigroup M] {a : Stream' M} {m : M} (hm : m Hindman.FP a) :
              ∃ (n : ), 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_FS {M : Type u_1} [AddSemigroup M] (a : Stream' M) :
              ∃ (U : Ultrafilter M), U + U = U ∀ᶠ (m : M) in U, m Hindman.FS a
              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_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), Hindman.FS a s₀
              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₀
              abbrev Hindman.FS_partition_regular.match_1 {M : Type u_1} (s : Set (Set M)) (U : Ultrafilter M) (motive : (ts, t U)Prop) :
              ∀ (x : ts, t U), (∀ (c : Set M) (cs : c s) (hc : c U), motive )motive x
              Equations
              • =
              Instances For
                abbrev Hindman.FS_partition_regular.match_2 {M : Type u_1} [AddSemigroup M] (a : Stream' M) (motive : (∃ (U : Ultrafilter M), U + U = U ∀ᶠ (m : M) in U, m Hindman.FS a)Prop) :
                ∀ (x : ∃ (U : Ultrafilter M), U + U = U ∀ᶠ (m : M) in U, m Hindman.FS a), (∀ (U : Ultrafilter M) (idem : U + U = U) (aU : ∀ᶠ (m : M) in U, m Hindman.FS a), motive )motive x
                Equations
                • =
                Instances For
                  theorem Hindman.FS_partition_regular {M : Type u_1} [AddSemigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : Hindman.FS a ⋃₀ s) :
                  cs, ∃ (b : Stream' M), Hindman.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.FP_partition_regular {M : Type u_1} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) (scov : Hindman.FP a ⋃₀ s) :
                  cs, ∃ (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} [AddSemigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : ⋃₀ s) :
                  cs, ∃ (a : Stream' M), Hindman.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.

                  abbrev Hindman.exists_FS_of_finite_cover.match_1 {M : Type u_1} [AddSemigroup M] (motive : (∃ (m : Ultrafilter M), m + m = m)Prop) :
                  ∀ (x : ∃ (m : Ultrafilter M), m + m = m), (∀ (U : Ultrafilter M) (hU : U + U = U), motive )motive x
                  Equations
                  • =
                  Instances For
                    theorem Hindman.exists_FP_of_finite_cover {M : Type u_1} [Semigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) (scov : ⋃₀ s) :
                    cs, ∃ (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.FS.singleton {M : Type u_1} [AddSemigroup M] (a : Stream' M) (i : ) :
                    a.get i Hindman.FS a
                    theorem Hindman.FP.singleton {M : Type u_1} [Semigroup M] (a : Stream' M) (i : ) :
                    a.get i Hindman.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 Hindman.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 Hindman.FP a
                    theorem Hindman.FS.finset_sum {M : Type u_1} [AddCommMonoid M] (a : Stream' M) (s : Finset ) (hs : s.Nonempty) :
                    (s.sum fun (i : ) => a.get i) Hindman.FS a
                    theorem Hindman.FP.finset_prod {M : Type u_1} [CommMonoid M] (a : Stream' M) (s : Finset ) (hs : s.Nonempty) :
                    (s.prod fun (i : ) => a.get i) Hindman.FP a