Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Port/Combinatorics.Hindman (#2280)
port of combinatorics.hindman Co-authored-by: Johan Commelin <johan@commelin.net>
- Loading branch information
1 parent
f249e00
commit 17e458e
Showing
2 changed files
with
311 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,310 @@ | ||
/- | ||
Copyright (c) 2021 David Wärn. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: David Wärn | ||
! This file was ported from Lean 3 source module combinatorics.hindman | ||
! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Topology.StoneCech | ||
import Mathlib.Topology.Algebra.Semigroup | ||
import Mathlib.Data.Stream.Init | ||
|
||
/-! | ||
# 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 | ||
-/ | ||
|
||
|
||
open Filter | ||
|
||
/-- Multiplication of ultrafilters given by `∀ᶠ m in U*V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m*m')`. -/ | ||
@[to_additive | ||
"Addition of ultrafilters given by\n`∀ᶠ m in U+V, p m ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m+m')`."] | ||
def Ultrafilter.hasMul {M} [Mul M] : Mul (Ultrafilter M) where mul U V := (· * ·) <$> U <*> V | ||
#align ultrafilter.has_mul Ultrafilter.hasMul | ||
#align ultrafilter.has_add Ultrafilter.hasAdd | ||
|
||
attribute [local instance] Ultrafilter.hasMul Ultrafilter.hasAdd | ||
|
||
/- We could have taken this as the definition of `U * V`, but then we would have to prove that it | ||
defines an ultrafilter. -/ | ||
@[to_additive] | ||
theorem Ultrafilter.eventually_mul {M} [Mul M] (U V : Ultrafilter M) (p : M → Prop) : | ||
(∀ᶠ m in ↑(U * V), p m) ↔ ∀ᶠ m in U, ∀ᶠ m' in V, p (m * m') := | ||
Iff.rfl | ||
#align ultrafilter.eventually_mul Ultrafilter.eventually_mul | ||
#align ultrafilter.eventually_add Ultrafilter.eventually_add | ||
|
||
-- porting note: slow to typecheck | ||
/-- Semigroup structure on `Ultrafilter M` induced by a semigroup structure on `M`. -/ | ||
@[to_additive | ||
"Additive semigroup structure on `Ultrafilter M` induced by an additive semigroup | ||
structure on `M`."] | ||
def Ultrafilter.semigroup {M} [Semigroup M] : Semigroup (Ultrafilter M) := | ||
{ Ultrafilter.hasMul with | ||
mul_assoc := fun U V W => | ||
Ultrafilter.coe_inj.mp <| | ||
Filter.ext' fun p => by simp only [Ultrafilter.eventually_mul, mul_assoc] } | ||
#align ultrafilter.semigroup Ultrafilter.semigroup | ||
#align ultrafilter.add_semigroup Ultrafilter.addSemigroup | ||
|
||
attribute [local instance] Ultrafilter.semigroup Ultrafilter.addSemigroup | ||
|
||
-- We don't prove `continuous_mul_right`, because in general it is false! | ||
@[to_additive] | ||
theorem Ultrafilter.continuous_mul_left {M} [Semigroup M] (V : Ultrafilter M) : | ||
Continuous (· * V) := | ||
TopologicalSpace.IsTopologicalBasis.continuous ultrafilterBasis_is_basis _ <| | ||
Set.forall_range_iff.mpr fun s => ultrafilter_isOpen_basic { m : M | ∀ᶠ m' in V, m * m' ∈ s } | ||
#align ultrafilter.continuous_mul_left Ultrafilter.continuous_mul_left | ||
#align ultrafilter.continuous_add_left Ultrafilter.continuous_add_left | ||
|
||
namespace Hindman | ||
|
||
-- porting note: mathport wants these names to be `fS`, `fP`, etc, but this does violence to | ||
-- mathematical naming conventions, as does `fs`, `fp`, so we just followed `mathlib` 3 here | ||
|
||
/-- `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 FS {M} [AddSemigroup M] : Stream' M → Set M | ||
| head (a : Stream' M) : FS a a.head | ||
| tail (a : Stream' M) (m : M) (h : FS a.tail m) : FS a m | ||
| cons (a : Stream' M) (m : M) (h : FS a.tail m) : FS a (a.head + m) | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS Hindman.FS | ||
|
||
/-- `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. -/ | ||
@[to_additive FS] | ||
inductive FP {M} [Semigroup M] : Stream' M → Set M | ||
| head (a : Stream' M) : FP a a.head | ||
| tail (a : Stream' M) (m : M) (h : FP a.tail m) : FP a m | ||
| cons (a : Stream' M) (m : M) (h : FP a.tail m) : FP a (a.head * m) | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP Hindman.FP | ||
|
||
/-- 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. -/ | ||
@[to_additive | ||
"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 FP.mul {M} [Semigroup M] {a : Stream' M} {m : M} (hm : m ∈ FP a) : | ||
∃ n, ∀ m' ∈ FP (a.drop n), m * m' ∈ FP a := by | ||
induction' hm with a a m hm ih a m hm ih | ||
· exact ⟨1, fun m hm => FP.cons a m hm⟩ | ||
· cases' ih with n hn | ||
use n + 1 | ||
intro m' hm' | ||
exact FP.tail _ _ (hn _ hm') | ||
· cases' ih with n hn | ||
use n + 1 | ||
intro m' hm' | ||
rw [mul_assoc] | ||
exact FP.cons _ _ (hn _ hm') | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP.mul Hindman.FP.mul | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS.add Hindman.FS.add | ||
|
||
@[to_additive exists_idempotent_ultrafilter_le_FS] | ||
theorem exists_idempotent_ultrafilter_le_FP {M} [Semigroup M] (a : Stream' M) : | ||
∃ U : Ultrafilter M, U * U = U ∧ ∀ᶠ m in U, m ∈ FP a := by | ||
let S : Set (Ultrafilter M) := ⋂ n, { U | ∀ᶠ m in U, m ∈ FP (a.drop n) } | ||
have h := exists_idempotent_in_compact_subsemigroup ?_ S ?_ ?_ ?_ | ||
rcases h with ⟨U, hU, U_idem⟩ | ||
· refine' ⟨U, U_idem, _⟩ | ||
convert Set.mem_interᵢ.mp hU 0 | ||
· exact Ultrafilter.continuous_mul_left | ||
· apply IsCompact.nonempty_interᵢ_of_sequence_nonempty_compact_closed | ||
· intro n U hU | ||
apply Eventually.mono hU | ||
rw [add_comm, ← Stream'.drop_drop, ← Stream'.tail_eq_drop] | ||
exact FP.tail _ | ||
· intro n | ||
exact ⟨pure _, mem_pure.mpr <| FP.head _⟩ | ||
· exact (ultrafilter_isClosed_basic _).isCompact | ||
· intro n | ||
apply ultrafilter_isClosed_basic | ||
· exact IsClosed.isCompact (isClosed_interᵢ fun i => ultrafilter_isClosed_basic _) | ||
· intro U hU V hV | ||
rw [Set.mem_interᵢ] at * | ||
intro n | ||
rw [Set.mem_setOf_eq, Ultrafilter.eventually_mul] | ||
apply Eventually.mono (hU n) | ||
intro m hm | ||
obtain ⟨n', hn⟩ := FP.mul hm | ||
apply Eventually.mono (hV (n' + n)) | ||
intro m' hm' | ||
apply hn | ||
simpa only [Stream'.drop_drop] using hm' | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_idempotent_ultrafilter_le_FP Hindman.exists_idempotent_ultrafilter_le_FP | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_idempotent_ultrafilter_le_FS Hindman.exists_idempotent_ultrafilter_le_FS | ||
|
||
@[to_additive exists_FS_of_large] | ||
theorem exists_FP_of_large {M} [Semigroup M] (U : Ultrafilter M) (U_idem : U * U = U) (s₀ : Set M) | ||
(sU : s₀ ∈ U) : ∃ a, FP a ⊆ s₀ := by | ||
/- Informally: given a `U`-large set `s₀`, the set `s₀ ∩ { m | ∀ᶠ m' in U, m * m' ∈ s₀ }` is also | ||
`U`-large (since `U` is idempotent). Thus in particular there is an `a₀` in this intersection. Now | ||
let `s₁` be the intersection `s₀ ∩ { m | a₀ * m ∈ s₀ }`. By choice of `a₀`, this is again | ||
`U`-large, so we can repeat the argument starting from `s₁`, obtaining `a₁`, `s₂`, etc. | ||
This gives the desired infinite sequence. -/ | ||
have exists_elem : ∀ {s : Set M} (_hs : s ∈ U), (s ∩ { m | ∀ᶠ m' in U, m * m' ∈ s }).Nonempty := | ||
fun {s} hs => | ||
Ultrafilter.nonempty_of_mem | ||
(inter_mem hs <| by | ||
rw [← U_idem] at hs | ||
exact hs) | ||
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some | ||
let succ : {s // s ∈ U} → {s // s ∈ U} := fun (p : {s // s ∈ U}) => | ||
⟨p.val ∩ {m : M | elem p * m ∈ p.val}, | ||
inter_mem p.property | ||
(show (exists_elem p.property).some ∈ {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} from | ||
p.val.inter_subset_right {m : M | ∀ᶠ (m' : M) in ↑U, m * m' ∈ p.val} | ||
(exists_elem p.property).some_mem)⟩ | ||
use Stream'.corec elem succ (Subtype.mk s₀ sU) | ||
suffices ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ p, a = Stream'.corec elem succ p → m ∈ p.val | ||
by | ||
intro m hm | ||
exact this _ m hm ⟨s₀, sU⟩ rfl | ||
clear sU s₀ | ||
intro a m h | ||
induction' h with b b n h ih b n h ih | ||
· rintro p rfl | ||
rw [Stream'.corec_eq, Stream'.head_cons] | ||
exact Set.inter_subset_left _ _ (Set.Nonempty.some_mem _) | ||
· rintro p rfl | ||
refine' Set.inter_subset_left _ _ (ih (succ p) _) | ||
rw [Stream'.corec_eq, Stream'.tail_cons] | ||
· rintro p rfl | ||
have := Set.inter_subset_right _ _ (ih (succ p) ?_) | ||
· simpa only using this | ||
rw [Stream'.corec_eq, Stream'.tail_cons] | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_FP_of_large Hindman.exists_FP_of_large | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_FS_of_large Hindman.exists_FS_of_large | ||
|
||
/-- The strong form of **Hindman's theorem**: in any finite cover of an FP-set, one the parts | ||
contains an FP-set. -/ | ||
@[to_additive FS_partition_regular | ||
"The strong form of **Hindman's theorem**: in any finite cover of | ||
an FS-set, one the parts contains an FS-set."] | ||
theorem FP_partition_regular {M} [Semigroup M] (a : Stream' M) (s : Set (Set M)) (sfin : s.Finite) | ||
(scov : FP a ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ b : Stream' M, FP b ⊆ c := | ||
let ⟨U, idem, aU⟩ := exists_idempotent_ultrafilter_le_FP a | ||
let ⟨c, cs, hc⟩ := (Ultrafilter.finite_unionₛ_mem_iff sfin).mp (mem_of_superset aU scov) | ||
⟨c, cs, exists_FP_of_large U idem c hc⟩ | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP_partition_regular Hindman.FP_partition_regular | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS_partition_regular Hindman.FS_partition_regular | ||
|
||
/-- The weak form of **Hindman's theorem**: in any finite cover of a nonempty semigroup, one of the | ||
parts contains an FP-set. -/ | ||
@[to_additive exists_FS_of_finite_cover | ||
"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 exists_FP_of_finite_cover {M} [Semigroup M] [Nonempty M] (s : Set (Set M)) (sfin : s.Finite) | ||
(scov : ⊤ ⊆ ⋃₀ s) : ∃ c ∈ s, ∃ a : Stream' M, FP a ⊆ c := | ||
let ⟨U, hU⟩ := | ||
exists_idempotent_of_compact_t2_of_continuous_mul_left (@Ultrafilter.continuous_mul_left M _) | ||
let ⟨c, c_s, hc⟩ := (Ultrafilter.finite_unionₛ_mem_iff sfin).mp (mem_of_superset univ_mem scov) | ||
⟨c, c_s, exists_FP_of_large U hU c hc⟩ | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_FP_of_finite_cover Hindman.exists_FP_of_finite_cover | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.exists_FS_of_finite_cover Hindman.exists_FS_of_finite_cover | ||
|
||
@[to_additive FS_iter_tail_sub_FS] | ||
theorem FP_drop_subset_FP {M} [Semigroup M] (a : Stream' M) (n : ℕ) : FP (a.drop n) ⊆ FP a := by | ||
induction' n with n ih; · rfl | ||
rw [Nat.succ_eq_one_add, ← Stream'.drop_drop] | ||
exact _root_.trans (FP.tail _) ih | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP_drop_subset_FP Hindman.FP_drop_subset_FP | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS_iter_tail_sub_FS Hindman.FS_iter_tail_sub_FS | ||
|
||
@[to_additive] | ||
theorem FP.singleton {M} [Semigroup M] (a : Stream' M) (i : ℕ) : a.nth i ∈ FP a := by | ||
induction' i with i ih generalizing a | ||
· apply FP.head | ||
· apply FP.tail | ||
apply ih | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP.singleton Hindman.FP.singleton | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS.singleton Hindman.FS.singleton | ||
|
||
@[to_additive] | ||
theorem FP.mul_two {M} [Semigroup M] (a : Stream' M) (i j : ℕ) (ij : i < j) : | ||
a.nth i * a.nth j ∈ FP a := by | ||
refine' FP_drop_subset_FP _ i _ | ||
rw [← Stream'.head_drop] | ||
apply FP.cons | ||
rcases le_iff_exists_add.mp (Nat.succ_le_of_lt ij) with ⟨d, hd⟩ | ||
have := FP.singleton (a.drop i).tail d | ||
rw [Stream'.tail_eq_drop, Stream'.nth_drop, Stream'.nth_drop] at this | ||
convert this | ||
rw [hd, add_comm, Nat.succ_add, Nat.add_succ] | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP.mul_two Hindman.FP.mul_two | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS.add_two Hindman.FS.add_two | ||
|
||
@[to_additive] | ||
theorem FP.finset_prod {M} [CommMonoid M] (a : Stream' M) (s : Finset ℕ) (hs : s.Nonempty) : | ||
(s.prod fun i => a.nth i) ∈ FP a := by | ||
refine' FP_drop_subset_FP _ (s.min' hs) _ | ||
induction' s using Finset.strongInduction with s ih | ||
rw [← Finset.mul_prod_erase _ _ (s.min'_mem hs), ← Stream'.head_drop] | ||
cases' (s.erase (s.min' hs)).eq_empty_or_nonempty with h h | ||
· rw [h, Finset.prod_empty, mul_one] | ||
exact FP.head _ | ||
· apply FP.cons | ||
rw [Stream'.tail_eq_drop, Stream'.drop_drop, add_comm] | ||
refine' Set.mem_of_subset_of_mem _ (ih _ (Finset.erase_ssubset <| s.min'_mem hs) h) | ||
have : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h := | ||
Nat.succ_le_of_lt (Finset.min'_lt_of_mem_erase_min' _ _ <| Finset.min'_mem _ _) | ||
cases' le_iff_exists_add.mp this with d hd | ||
rw [hd, add_comm, ← Stream'.drop_drop] | ||
apply FP_drop_subset_FP | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FP.finset_prod Hindman.FP.finset_prod | ||
set_option linter.uppercaseLean3 false in | ||
#align hindman.FS.finset_sum Hindman.FS.finset_sum | ||
|
||
end Hindman |