Infinite occurrences

def Cslib.ωSequence.infOcc {α : Type u} (xs : ωSequence α) : Set α

The set of elements that appear infinitely often in an ω-sequence.

Equations

• xs.infOcc = {x : α | ∃ᶠ (k : ℕ) in Filter.atTop, xs k = x}

theorem Cslib.ωSequence.frequently_iff_strictMono {p : ℕ → Prop} : (∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (m : ℕ), p (f m)

An alternative characterization of "infinitely often".

theorem Cslib.ωSequence.frequently_in_finite_type {α : Type u} [Finite α] {s : Set α} {xs : ωSequence α} : (∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ s) ↔ ∃ x ∈ s, ∃ᶠ (k : ℕ) in Filter.atTop, xs k = x

In a finite type, the elements of a set occurs infinitely often iff some element in the set occurs infinitely often.

theorem Cslib.ωSequence.frequently_in_strictMono {p : ℕ → Prop} {f : ℕ → ℕ} (hm : StrictMono f) (hf : ∃ᶠ (k : ℕ) in Filter.atTop, p k) : ∃ᶠ (n : ℕ) in Filter.atTop, ∃ k < f (n + 1) - f n, p (f n + k)

If p is true infinitely often, then p is true in infinitely many segments of any strictly monotonic function f.

theorem Cslib.ωSequence.strictMono_of_infinite {ns : Set ℕ} (h : ns.Infinite) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Set.range φ = ns

Every infinite subset of ℕ is the range of a strictly monotonic function from ℕ to ℕ.