Bounded slaloms as a relation

This defines the actual finite-set-valued slaloms of the manuscript. Their relation norm is not identified with nonM by definition.

def NonMRR.Slalom (r : ℕ → ℕ) : Type

A slalom with the pointwise width bound r.

Equations

• NonMRR.Slalom r = { φ : ℕ → Finset ℕ // ∀ (n : ℕ), (φ n).card ≤ r n }

def NonMRR.slalomRelation (r : ℕ → ℕ) (hr : ∀ (n : ℕ), 0 < r n) : Relation

The slalom relation: the response catches the challenge infinitely often.

Equations

• NonMRR.slalomRelation r hr = { Challenge := ℕ → ℕ, Response := NonMRR.Slalom r, relates := fun (e : ℕ → ℕ) (φ : NonMRR.Slalom r) => ∃ᶠ (n : ℕ) in Filter.atTop, e n ∈ ↑φ n, total := ⋯ }

theorem NonMRR.dominating_slalomRelation_iff (r : ℕ → ℕ) (hr : ∀ (n : ℕ), 0 < r n) (s : Set (Slalom r)) : (slalomRelation r hr).Dominating s ↔ ¬∃ (e : ℕ → ℕ), ∀ φ ∈ s, ∀ᶠ (n : ℕ) in Filter.atTop, e n ∉ ↑φ n

A slalom family is dominating exactly when it has no common eventual avoider.