Unbounded families of interval gaps

An eventually unbounded family gives, without increasing its cardinality, a family of increasing sequences whose successive gaps escape any prescribed function. This is the bounding-number ingredient in the category reduction.

def NonMRR.monotoneMajorant (f : ℕ → ℕ) (n : ℕ) : ℕ

A monotone pointwise majorant of an arbitrary function.

Equations

• NonMRR.monotoneMajorant f n = max (n + 1) ((Finset.range (n + 1)).sup f)

theorem NonMRR.le_monotoneMajorant (f : ℕ → ℕ) (n : ℕ) : f n ≤ monotoneMajorant f n

theorem NonMRR.monotone_monotoneMajorant (f : ℕ → ℕ) : Monotone (monotoneMajorant f)

theorem NonMRR.exists_between_consecutive {t : ℕ → ℕ} (ht : StrictMono t) (hzero : t 0 = 0) (n : ℕ) : ∃ (k : ℕ), t k ≤ n ∧ n < t (k + 1)

Locate an integer between consecutive terms of an increasing sequence starting at zero.

theorem NonMRR.eventuallyLE_of_tame_gaps (f h : ℕ → ℕ) (htame : ∀ᶠ (k : ℕ) in Filter.atTop, spacedSequence (monotoneMajorant f) (k + 1) ≤ h (spacedSequence (monotoneMajorant f) k)) : EventuallyLE f (monotoneMajorant h ∘ monotoneMajorant h)

Tame successive gaps force eventual domination of the original function.

theorem NonMRR.exists_gap_unbounded_family : ∃ (B : Set (ℕ → ℕ)), Cardinal.mk ↑B ≤ boundingNumber ∧ (∀ t ∈ B, StrictMono t) ∧ ∀ (h : ℕ → ℕ), ∃ t ∈ B, ∃ᶠ (k : ℕ) in Filter.atTop, h (t k) < t (k + 1)

There is a family of increasing sequences of size at most b whose gaps escape every natural-valued function infinitely often.