The infinite Ramsey theorem

This file proves the infinite Ramsey theorem for finite colourings of the r-element subsets of ℕ, for arbitrary arity r, and derives the classical pairs (RT²) and triples (RT³) cases in their relational form.

Main results

• infinite_ramsey: for every finite colouring c : Finset ℕ → κ of the r-subsets and every infinite M ⊆ ℕ, there is an infinite N ⊆ M all of whose r-subsets get one colour. Proved by induction on r (the "fan" argument).
• infinite_ramsey_seq: the enumeration form — the monochromatic set is the range of a strictly monotone e : ℕ → ℕ.
• infinite_ramsey_pairs, infinite_ramsey_triples: the classical RT²/RT³ statements for colourings of ordered pairs m < n and triples m < n < l, obtained from infinite_ramsey_seq at arity 2 and 3 by colouring a finite set through its least/greatest (and, for triples, middle) element.

The Finset ℕ colouring interface follows B. Mehta's Lean 3 inf_ramsey.lean. See also the standalone project https://github.com/yannpequignot/lean-infinite-ramsey.

Two proofs of infinite Ramsey

The proof here is direct and self-contained. Front.ramsey_seq_of_nashWilliams, in NashWilliams.Combinatorics.Front.NashWilliams, proves the same statement a second way, by instantiating the Nash-Williams theorem at the uniform front [M]^k. Both are kept, and neither file imports the other: they share only the generic helpers in NashWilliams.Data.

theorem infinite_ramsey {κ : Type u_1} [Finite κ] (r : ℕ) (c : Finset ℕ → κ) {M : Set ℕ} (hM : M.Infinite) : ∃ N ⊆ M, N.Infinite ∧ ∃ (col : κ), ∀ (t : Finset ℕ), ↑t ⊆ N → t.card = r → c t = col

theorem infinite_ramsey_seq {κ : Type u_1} [Finite κ] (r : ℕ) (c : Finset ℕ → κ) : ∃ (e : ℕ → ℕ), StrictMono e ∧ ∃ (col : κ), ∀ (t : Finset ℕ), ↑t ⊆ Set.range e → t.card = r → c t = col

theorem infinite_ramsey_pairs {κ : Type u_2} [Finite κ] (c : (m n : ℕ) → m < n → κ) : ∃ (e : ℕ → ℕ) (he : StrictMono e) (k : κ), ∀ (i j : ℕ) (h : i < j), c (e i) (e j) ⋯ = k

The infinite Ramsey theorem for pairs (RT²), in relational form: for a finite colouring c of the ordered pairs m < n, there is a strictly monotone e and a colour k with c (e i) (e j) = k for all i < j. Derived from infinite_ramsey_seq at arity 2.

theorem infinite_ramsey_triples {κ : Type u_2} [Finite κ] (c : (m n l : ℕ) → m < n ∧ n < l → κ) : ∃ (e : ℕ → ℕ) (he : StrictMono e) (k : κ), ∀ (h i j : ℕ) (hs : h < i ∧ i < j), c (e h) (e i) (e j) ⋯ = k

The infinite Ramsey theorem for triples (RT³), in relational form, derived from infinite_ramsey_seq at arity 3 (colour a 3-subset by c of its least, middle and greatest element).