Finiteness and Filter.atTop and Filter.atBot filters

This file contains results on Filter.atTop and Filter.atBot that depend on the finiteness theory developed in Mathlib.

theorem Filter.eventually_forall_ge_atTop {α : Type u_3} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

theorem Filter.eventually_forall_le_atBot {α : Type u_3} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in atBot, p x

theorem Filter.Tendsto.eventually_forall_ge_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Tendsto f l atTop) (h_evtl : ∀ᶠ (x : β) in atTop, p x) : ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

theorem Filter.Tendsto.eventually_forall_le_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Tendsto f l atBot) (h_evtl : ∀ᶠ (x : β) in atBot, p x) : ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Sequences

theorem Filter.high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) (N : ℕ) : ∃ n ≥ N, ∀ k < n, u k < u n

If u is a sequence which is unbounded above, then after any point, it reaches a value strictly greater than all previous values.

theorem Filter.low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Tendsto u atTop atBot) (N : ℕ) : ∃ n ≥ N, ∀ k < n, u n < u k

If u is a sequence which is unbounded below, then after any point, it reaches a value strictly smaller than all previous values.

theorem Filter.frequently_high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) : ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

If u is a sequence which is unbounded above, then it Frequently reaches a value strictly greater than all previous values.

theorem Filter.frequently_low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Tendsto u atTop atBot) : ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u n < u k

If u is a sequence which is unbounded below, then it Frequently reaches a value strictly smaller than all previous values.

theorem Filter.strictMono_subseq_of_tendsto_atTop {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

theorem Filter.strictMono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ (n : ℕ), n ≤ u n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

theorem Filter.Eventually.atTop_of_arithmetic {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)) : ∀ᶠ (a : ℕ) in atTop, p a

theorem Filter.HasAntitoneBasis.subbasis_with_rel {α : Type u_3} {f : Filter α} {s : ℕ → Set α} (hs : f.HasAntitoneBasis s) {r : ℕ → ℕ → Prop} (hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Given an antitone basis s : ℕ → Set α of a filter, extract an antitone subbasis s ∘ φ, φ : ℕ → ℕ, such that m < n implies r (φ m) (φ n). This lemma can be used to extract an antitone basis with basis sets decreasing "sufficiently fast".

theorem Nat.eventually_pow_lt_factorial_sub (c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c ^ n < (n - d).factorial

theorem Nat.eventually_mul_pow_lt_factorial_sub (a c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < (n - d).factorial