Infinite Ramsey theory

Stream: mathlib4

[Leo Shine]

I was looking into trying to prove some facts about well quasi ordering (namely that if a relation is Well Quasi Ordered then a set based version of the relation is Well quasi ordered) and I noticed I had to assume that my relation was a preorder even though I believe this is not necessary for the proof.

I wanted to use the fact that every sequence within a WQO (well quasi order) has a monotone subsequence, which I also think does not need a preorder property,

theorem WellQuasiOrdered.exists_monotone_subseq [IsPreorder α r] (h : WellQuasiOrdered r)
    (f : ℕ → α) : ∃ g : ℕ ↪o ℕ, ∀ m n, m ≤ n → r (f (g m)) (f (g n))

if I remove the assumption then theorem ends up breaking because it relies on

/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
Bolzano-Weierstrass for `ℝ`. -/
theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTrans α r] (f : ℕ → α) :
    ∃ g : ℕ ↪o ℕ,
      (∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n)) := by

Which directly uses IsTrans α r in the proof.

This shouldn't be necessary as you should be able to colour the edges between each pair of Numbers based on whether the relation is true for them, and then use the Infinite Ramsey theorem to get an infinite clique of increasing or non-increasing numbers.

Now it looks like someone has used Lean (possibly not lean 4) to prove a version of this here https://github.com/b-mehta/combinatorics/blob/extras/src/inf_ramsey.lean , so I'm wondering if there's a reason this has been left out of MathLib itself?\

Now it looks like there was a discussion of this earlier this year here #new members > Is the infinitary Ramsey theorem in mathlib? but it doesn't look like any of the referenced PRs have been merged

[Ching-Tsun Chou]

For uses in my automata theory project, I proved Ramsey's theorem for infinite graphs in Lean4:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/Mathlib/InfGraphRamsey.lean
which should suffice for your purpose.

[Bhavik Mehta]

I have an updated version of that code for Lean 4, which I can post later in the week, which gives a short proof of the infinite Ramsey theorem for hypergraphs. But I agree that the theorem you quote should be true without transitivity. The linked Lean 3 code wasn't ported or updated because it uses a weird recursion principle which mathlib at the time didn't want, and with the benefit of (several) years of hindsight, is not the right way of proving it.

[Zachary Mullaghy]

Ive been working on incorporating ramsey theory in my own transform theory work - ill keep an eye on this. Thanks for the heads up

[Ching-Tsun Chou]

@Bhavik Mehta Just wondering if your code will be available soon. Thanks in advance!