Regular sequences in a well quasi-order

A sequence f : ℕ → Q in a quasi-order (Q, r) is regular if every term dominates infinitely many later terms. This file shows that in a WQO every sequence has a regular tail (WellQuasiOrdered.eventuallyRegular), and draws two consequences that are the backbone of the 2-BQO closure theorems in TwoBQO.lean:

• an antitone sequence in a WQO eventually stabilizes (WellQuasiOrdered.exists_forall_le_of_antitone);
• List.SublistForall₂ r (Higman's order) is a WQO on all of List Q, not just on a PartiallyWellOrderedOn subset (WellQuasiOrdered.sublistForall₂), a direct corollary of Higman's lemma already in Mathlib (Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂).

Main definitions

• Preorder.IsRegularSeq r f: every term of f dominates infinitely many later terms.

Main results

• WellQuasiOrdered.eventuallyRegular: every sequence in a WQO has a regular tail.
• WellQuasiOrdered.exists_forall_le_of_antitone: an antitone sequence in a WQO stabilizes.
• WellQuasiOrdered.sublistForall₂: Higman's order is a WQO on List Q when r is a WQO on Q.

Regular sequences

A sequence (f i)_{i ∈ ℕ} in a quasi-order (Q, ≤) is regular if for every i : ℕ, the set {j : ℕ | f i ≤ f j} is infinite.

def Preorder.IsRegularSeq {Q : Type u_1} (r : Q → Q → Prop) (f : ℕ → Q) : Prop

A sequence is regular if every term dominates infinitely many later terms.

Equations

• Preorder.IsRegularSeq r f = ∀ (i : ℕ), {j : ℕ | r (f i) (f j)}.Infinite

theorem Preorder.IsRegularSeq.exists_ge {Q : Type u_1} {r : Q → Q → Prop} {f : ℕ → Q} (hf : IsRegularSeq r f) (i N : ℕ) : ∃ (j : ℕ), N ≤ j ∧ r (f i) (f j)

A regular sequence has arbitrarily large indices dominating any given index: for every i and threshold N there is j ≥ N with f i ≤ f j.

theorem Preorder.IsRegularSeq.tail {Q : Type u_1} {r : Q → Q → Prop} {f : ℕ → Q} (hf : IsRegularSeq r f) (k : ℕ) : IsRegularSeq r fun (i : ℕ) => f (i + k)

A tail of a regular sequence is regular.

theorem WellQuasiOrdered.eventuallyRegular {Q : Type u_1} (r : Q → Q → Prop) (hwqo : WellQuasiOrdered r) (f : ℕ → Q) : ∃ (n : ℕ), Preorder.IsRegularSeq r fun (i : ℕ) => f (i + n)

In a WQO every sequence is eventually regular. In fact this is an equivalent characterization of WQO, since any bad sequence admits no regular tail.

theorem WellQuasiOrdered.exists_forall_le_of_antitone {β : Type u_1} {r : β → β → Prop} [IsPreorder β r] (hwqo : WellQuasiOrdered r) (a : ℕ → β) (hanti : ∀ (m n : ℕ), m ≤ n → r (a n) (a m)) : ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → r (a m) (a n)

In a WQO, an antitone sequence stabilizes from above: there is an index m from which the sequence becomes r-dominated by a m (so, together with antitonicity, a m is r-equivalent to every later term).

instance List.SublistForall₂.instIsPreorder {Q : Type u_1} (r : Q → Q → Prop) [IsPreorder Q r] : IsPreorder (List Q) (SublistForall₂ r)

List.SublistForall₂ r is a preorder on List Q whenever r is a preorder on Q.

theorem WellQuasiOrdered.sublistForall₂ {Q : Type u_1} {r : Q → Q → Prop} [IsPreorder Q r] (h : WellQuasiOrdered r) : WellQuasiOrdered (List.SublistForall₂ r)

Higman's Lemma, unrestricted. If r is a WQO on Q, then List.SublistForall₂ r is a WQO on all of List Q (not just on a PartiallyWellOrderedOn subset). A direct restatement of Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ via partiallyWellOrderedOn_univ_iff.