The bounding relation

The relation boundingRelation has f related to g when f n < g n infinitely often. Its norm is the bounding number in the manuscript.

def NonMRR.EventuallyLE (f g : ℕ → ℕ) : Prop

Eventual domination of natural-valued sequences.

Equations

• NonMRR.EventuallyLE f g = ∀ᶠ (n : ℕ) in Filter.atTop, f n ≤ g n

def NonMRR.FrequentlyLT (f g : ℕ → ℕ) : Prop

The strict comparison holding at arbitrarily large coordinates.

Equations

• NonMRR.FrequentlyLT f g = ∃ᶠ (n : ℕ) in Filter.atTop, f n < g n

theorem NonMRR.frequentlyLT_iff_not_eventuallyLE (f g : ℕ → ℕ) : FrequentlyLT f g ↔ ¬EventuallyLE g f

def NonMRR.boundingRelation : Relation

The usual relation whose norm is the bounding number.

Equations

• NonMRR.boundingRelation = { Challenge := ℕ → ℕ, Response := ℕ → ℕ, relates := NonMRR.FrequentlyLT, total := NonMRR.boundingRelation._proof_2 }

noncomputable def NonMRR.boundingNumber : Cardinal.{0}

The least cardinality of an eventually unbounded family.

Equations

• NonMRR.boundingNumber = NonMRR.boundingRelation.norm

theorem NonMRR.dominating_boundingRelation_iff (s : Set (ℕ → ℕ)) : boundingRelation.Dominating s ↔ ¬∃ (f : ℕ → ℕ), ∀ g ∈ s, EventuallyLE g f

theorem NonMRR.exists_eventually_bounds_of_countable {s : Set (ℕ → ℕ)} (hs : s.Countable) : ∃ (f : ℕ → ℕ), ∀ g ∈ s, EventuallyLE g f

Every countable family of functions is eventually bounded.

theorem NonMRR.aleph0_lt_boundingNumber : Cardinal.aleph0 < boundingNumber

The bounding number is uncountable.