Perfect/bad dichotomy and monotone subsequences in a well-quasi-order

The infinite Ramsey theorem for pairs gives a clean "perfect or bad" dichotomy for sequences in any relation, from which the monotone subsequence property of a well-quasi-order follows without any transitivity assumption.

Main results

• Sequences.perfect_or_bad: every sequence has a subsequence that is either perfect (all earlier terms r-below all later ones) or bad (no earlier term r-below a later one). Pure consequence of infinite_ramsey_pairs; needs no order axioms.
• WellQuasiOrdered.exists_monotone_subseq_lt: in a WQO, every sequence has a strictly increasing reindexing along which r holds for all pairs m < n. No typeclass assumptions.

The second result answers a question of Leo Shine on the Mathlib Zulip: the monotone-subsequence property of a WQO does not need the preorder (in particular transitivity) hypothesis carried by the current Mathlib WellQuasiOrdered.exists_monotone_subseq.

def Sequences.IsBad {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) : Prop

A sequence is bad for r if no earlier term is r-below a later one.

Equations

• Sequences.IsBad r f = ∀ (m n : ℕ), m < n → ¬r (f m) (f n)

def Sequences.IsPerfect {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) : Prop

A sequence is perfect for r if every earlier term is r-below every later one.

Equations

• Sequences.IsPerfect r f = ∀ (m n : ℕ), m < n → r (f m) (f n)

theorem Sequences.perfect_or_bad {α : Type u_1} (r : α → α → Prop) (f : ℕ → α) : ∃ (e : ℕ → ℕ), StrictMono e ∧ (IsPerfect r (f ∘ e) ∨ IsBad r (f ∘ e))

Perfect/bad dichotomy. Every sequence f : ℕ → α has a strictly increasing reindexing f ∘ e that is either perfect or bad for r. Immediate from the infinite Ramsey theorem for pairs applied to the 2-colouring (m, n) ↦ ¬ r (f m) (f n); no order axioms are used.

theorem WellQuasiOrdered.exists_monotone_subseq_lt {α : Type u_1} {r : α → α → Prop} (h : WellQuasiOrdered r) (f : ℕ → α) : ∃ (e : ℕ → ℕ), StrictMono e ∧ ∀ (m n : ℕ), m < n → r (f (e m)) (f (e n))

Monotone subsequences from a WQO, without transitivity. In a well-quasi-order, every sequence has a strictly increasing reindexing e along which r (f (e m)) (f (e n)) holds for all m < n. Follows directly from the perfect/bad dichotomy: a bad subsequence would contradict the WQO. No typeclass assumptions on r.