A common sparse set ordered eventually by a small family of permutations

An eventually bounded family of permutation controls admits a common increasing sequence whose tail is preserved in order by the inverse of each permutation.

def NonMRR.permutationControl (π : Equiv.Perm ℕ) (n : ℕ) : ℕ

A cutoff after which all inverse images exceed the inverse images of 0, ..., n.

Equations

• NonMRR.permutationControl π n = (Finset.range ((Finset.range (n + 1)).sup ⇑(Equiv.symm π) + 1)).sup ⇑π + 1

theorem NonMRR.permutationControl_separates (π : Equiv.Perm ℕ) {n x y : ℕ} (hx : x ≤ n) (hy : permutationControl π n ≤ y) : (Equiv.symm π) x < (Equiv.symm π) y

def NonMRR.spacedSequence (g : ℕ → ℕ) : ℕ → ℕ

Insert enough space after each point to pass the next cutoff.

Equations

• NonMRR.spacedSequence g 0 = 0
• NonMRR.spacedSequence g n.succ = max (NonMRR.spacedSequence g n + 1) (g (NonMRR.spacedSequence g n))

theorem NonMRR.spacedSequence_strictMono (g : ℕ → ℕ) : StrictMono (spacedSequence g)

theorem NonMRR.id_le_spacedSequence (g : ℕ → ℕ) (n : ℕ) : n ≤ spacedSequence g n

theorem NonMRR.spacedSequence_eventually_ordered (g : ℕ → ℕ) (π : Equiv.Perm ℕ) (hπ : EventuallyLE (permutationControl π) g) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), n < m → (Equiv.symm π) (spacedSequence g n) < (Equiv.symm π) (spacedSequence g m)

theorem NonMRR.exists_bound_permutationControls (P : Set (Equiv.Perm ℕ)) (hP : Cardinal.mk ↑P < boundingNumber) : ∃ (g : ℕ → ℕ), ∀ π ∈ P, EventuallyLE (permutationControl π) g

A family with cardinality below the bounding number has a common eventual bound for all of its permutation controls.

theorem NonMRR.exists_common_eventually_ordered_subsequence (P : Set (Equiv.Perm ℕ)) (hP : Cardinal.mk ↑P < boundingNumber) : ∃ (l : ℕ → ℕ), StrictMono l ∧ ∀ π ∈ P, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), n < m → (Equiv.symm π) (l n) < (Equiv.symm π) (l m)

Every family of fewer than boundingNumber permutations has a common infinite set on which the inverse of each permutation is eventually increasing.