From coincidence families to a nonmeagre set

The finite-block description is combined with the explicit pasting of separated blocks. All cardinal estimates use images of actual families.

def NonMRR.StronglyCoincident (F : Set (ℕ → ℕ)) : Prop

A family meeting each prescribed function infinitely often along each infinite set of coordinates.

Equations

• NonMRR.StronglyCoincident F = ∀ (W : Set ℕ), W.Infinite → ∀ (c : ℕ → ℕ), ∃ f ∈ F, ∃ᶠ (n : ℕ) in Filter.atTop, n ∈ W ∧ f n = c n

def NonMRR.GapUnbounded (B : Set (ℕ → ℕ)) : Prop

A family of increasing sequences with gaps escaping each bound.

Equations

• NonMRR.GapUnbounded B = ((∀ t ∈ B, StrictMono t) ∧ ∀ (g : ℕ → ℕ), ∃ t ∈ B, ∃ᶠ (k : ℕ) in Filter.atTop, g (t k) < t (k + 1))

@[reducible, inline]

abbrev NonMRR.FiniteBinaryWord : Type

Finite binary words, including the empty word.

Equations

• NonMRR.FiniteBinaryWord = ((m : ℕ) × (Fin m → Bool))

def NonMRR.wordEnd (n : ℕ) (w : FiniteBinaryWord) : ℕ

The endpoint of a word placed at coordinate n.

Equations

• NonMRR.wordEnd n w = n + w.fst

def NonMRR.wordValue (n : ℕ) (w : FiniteBinaryWord) (i : ℕ) : Bool

Read a word at offset i - n, returning false past its endpoint.

Equations

• NonMRR.wordValue n w i = if hi : i - n < w.fst then w.snd ⟨i - n, hi⟩ else false

def NonMRR.restrictWord (n m : ℕ) (a : ℕ → Bool) : FiniteBinaryWord

Encode a finite restriction of a binary sequence as a word.

Equations

• NonMRR.restrictWord n m a = ⟨m - n, fun (i : Fin (m - n)) => a (n + ↑i)⟩

theorem NonMRR.wordEnd_restrictWord {n m : ℕ} (hnm : n ≤ m) (a : ℕ → Bool) : wordEnd n (restrictWord n m a) = m

theorem NonMRR.wordValue_restrictWord {n m i : ℕ} (hni : n ≤ i) (him : i < m) (a : ℕ → Bool) : wordValue n (restrictWord n m a) i = a i

theorem NonMRR.exists_nonmeagre_of_gap_and_coincidence {B F : Set (ℕ → ℕ)} (hB : GapUnbounded B) (hF : StronglyCoincident F) : ∃ (Y : Set (ℕ → Bool)), ¬IsMeagre Y ∧ Cardinal.mk ↑Y ≤ Cardinal.mk ↑B * Cardinal.mk ↑F

The central category reduction: pasting a gap-unbounded family and a strong coincidence family yields a nonmeagre set of the expected size.

theorem NonMRR.nonMeagreCardinal_le_product_of_gap_and_coincidence {B F : Set (ℕ → ℕ)} (hB : GapUnbounded B) (hF : StronglyCoincident F) : nonMeagreCardinal (ℕ → Bool) ≤ Cardinal.mk ↑B * Cardinal.mk ↑F