Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Filter.atTop.isCountablyGenerated instance

[Preorder α] [Countable α] : (atTop : Filter <| α).IsCountablyGenerated

Full source

instance (priority := 200) atTop.isCountablyGenerated [Preorder α] [Countable α] :
    (atTop : Filter <| α).IsCountablyGenerated :=
  isCountablyGenerated_seq _

Countable Generation of the `atTop` Filter on Countable Preorders

Informal description

For any countable preorder $\alpha$, the filter `atTop` on $\alpha$ is countably generated.

Filter.atBot.isCountablyGenerated instance

[Preorder α] [Countable α] : (atBot : Filter <| α).IsCountablyGenerated

Full source

instance (priority := 200) atBot.isCountablyGenerated [Preorder α] [Countable α] :
    (atBot : Filter <| α).IsCountablyGenerated :=
  isCountablyGenerated_seq _

Countable Generation of the `atBot` Filter on Countable Preorders

Informal description

For any countable preorder $\alpha$, the filter `atBot` on $\alpha$ is countably generated.

Filter.instIsCountablyGeneratedAtTopProd instance

 [Preorder α] [IsCountablyGenerated (atTop : Filter α)] [Preorder β] [IsCountablyGenerated (atTop : Filter β)] :
  IsCountablyGenerated (atTop : Filter (α × β))

Full source

instance instIsCountablyGeneratedAtTopProd [Preorder α] [IsCountablyGenerated (atTop : Filter α)]
    [Preorder β] [IsCountablyGenerated (atTop : Filter β)] :
    IsCountablyGenerated (atTop : Filter (α × β)) := by
  rw [← prod_atTop_atTop_eq]
  infer_instance

Countable Generation of `atTop` Filter on Product Types

Informal description

For any preordered types $\alpha$ and $\beta$ where the `atTop` filters are countably generated, the `atTop` filter on the product type $\alpha \times \beta$ is also countably generated.

Filter.instIsCountablyGeneratedAtBotProd instance

 [Preorder α] [IsCountablyGenerated (atBot : Filter α)] [Preorder β] [IsCountablyGenerated (atBot : Filter β)] :
  IsCountablyGenerated (atBot : Filter (α × β))

Full source

instance instIsCountablyGeneratedAtBotProd [Preorder α] [IsCountablyGenerated (atBot : Filter α)]
    [Preorder β] [IsCountablyGenerated (atBot : Filter β)] :
    IsCountablyGenerated (atBot : Filter (α × β)) := by
  rw [← prod_atBot_atBot_eq]
  infer_instance

Countable Generation of `atBot` Filter on Product Types

Informal description

For any preordered types $\alpha$ and $\beta$ where the `atBot` filters are countably generated, the `atBot` filter on the product type $\alpha \times \beta$ is also countably generated.

OrderDual.instIsCountablyGeneratedAtTop instance

[Preorder α] [IsCountablyGenerated (atBot : Filter α)] : IsCountablyGenerated (atTop : Filter αᵒᵈ)

Full source

instance _root_.OrderDual.instIsCountablyGeneratedAtTop [Preorder α]
    [IsCountablyGenerated (atBot : Filter α)] : IsCountablyGenerated (atTop : Filter αᵒᵈ) := ‹_›

Countable Generation of `atTop` Filter on Order Dual

Informal description

For any preorder $\alpha$, if the filter `atBot` on $\alpha$ is countably generated, then the filter `atTop` on the order dual $\alpha^{\text{op}}$ is also countably generated.

OrderDual.instIsCountablyGeneratedAtBot instance

[Preorder α] [IsCountablyGenerated (atTop : Filter α)] : IsCountablyGenerated (atBot : Filter αᵒᵈ)

Full source

instance _root_.OrderDual.instIsCountablyGeneratedAtBot [Preorder α]
    [IsCountablyGenerated (atTop : Filter α)] : IsCountablyGenerated (atBot : Filter αᵒᵈ) := ‹_›

Countable Generation of `atBot` Filter on Order Dual

Informal description

For any preorder $\alpha$, if the filter `atTop` on $\alpha$ is countably generated, then the filter `atBot` on the order dual $\alpha^{\text{op}}$ is also countably generated.

Filter.atTop_countable_basis theorem

 [Preorder α] [IsDirected α (· ≤ ·)] [Nonempty α] [Countable α] :
  HasCountableBasis (atTop : Filter α) (fun _ => True) Ici

Full source

lemma atTop_countable_basis [Preorder α] [IsDirected α (· ≤ ·)] [Nonempty α] [Countable α] :
    HasCountableBasis (atTop : Filter α) (fun _ => True) Ici :=
  { atTop_basis with countable := to_countable _ }

Countable Basis for `atTop` Filter on Directed Countable Preorders

Informal description

Let $\alpha$ be a nonempty countable preorder where the relation $\leq$ is directed. Then the filter `atTop` on $\alpha$ has a countable basis consisting of all left-closed right-infinite intervals $[a, \infty)$ for $a \in \alpha$. In other words, there exists a countable collection of sets that generates the `atTop` filter.

Filter.atBot_countable_basis theorem

 [Preorder α] [IsDirected α (· ≥ ·)] [Nonempty α] [Countable α] :
  HasCountableBasis (atBot : Filter α) (fun _ => True) Iic

Full source

lemma atBot_countable_basis [Preorder α] [IsDirected α (· ≥ ·)] [Nonempty α] [Countable α] :
    HasCountableBasis (atBot : Filter α) (fun _ => True) Iic :=
  { atBot_basis with countable := to_countable _ }

Countable Basis for `atBot` Filter on Directed Countable Preorders

Informal description

Let $\alpha$ be a nonempty countable preorder where the relation $\geq$ is directed. Then the filter `atBot` on $\alpha$ has a countable basis consisting of all left-infinite right-closed intervals $(-\infty, b]$ for $b \in \alpha$. In other words, there exists a countable collection of sets that generates the `atBot` filter.

Filter.exists_seq_tendsto theorem

(f : Filter α) [IsCountablyGenerated f] [NeBot f] : ∃ x : ℕ → α, Tendsto x atTop f

Full source

/-- If `f` is a nontrivial countably generated filter, then there exists a sequence that converges
to `f`. -/
theorem exists_seq_tendsto (f : Filter α) [IsCountablyGenerated f] [NeBot f] :
    ∃ x : ℕ → α, Tendsto x atTop f := by
  obtain ⟨B, h⟩ := f.exists_antitone_basis
  choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
  exact ⟨x, h.tendsto hx⟩

Existence of a Convergent Sequence for a Countably Generated Filter

Informal description

For any nontrivial countably generated filter $f$ on a type $\alpha$, there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ that converges to $f$ as $n \to \infty$.

Filter.exists_seq_monotone_tendsto_atTop_atTop theorem

 (α : Type*) [Preorder α] [Nonempty α] [IsDirected α (· ≤ ·)] [(atTop : Filter α).IsCountablyGenerated] :
  ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop

Full source

theorem exists_seq_monotone_tendsto_atTop_atTop (α : Type*) [Preorder α] [Nonempty α]
    [IsDirected α (· ≤ ·)] [(atTop : Filter α).IsCountablyGenerated] :
    ∃ xs : ℕ → α, Monotone xs ∧ Tendsto xs atTop atTop := by
  obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
  choose c hleft hright using exists_ge_ge (α := α)
  set xs : ℕ → α := fun n => (List.range n).foldl (fun x n ↦ c x (ys n)) (ys 0)
  have hsucc (n : ℕ) : xs (n + 1) = c (xs n) (ys n) := by simp [xs, List.range_succ]
  refine ⟨xs, ?_, ?_⟩
  · refine monotone_nat_of_le_succ fun n ↦ ?_
    rw [hsucc]
    apply hleft
  · refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h
    rw [hsucc]
    apply hright

Existence of Monotone Sequence Tending to $\mathrm{atTop}$ in Directed Preorders

Informal description

Let $\alpha$ be a nonempty preorder where the relation $\leq$ is directed and the filter $\mathrm{atTop}$ on $\alpha$ is countably generated. Then there exists a monotone sequence $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $x_n \to \mathrm{atTop}$ as $n \to \infty$.

Filter.exists_seq_antitone_tendsto_atTop_atBot theorem

 (α : Type*) [Preorder α] [Nonempty α] [IsDirected α (· ≥ ·)] [(atBot : Filter α).IsCountablyGenerated] :
  ∃ xs : ℕ → α, Antitone xs ∧ Tendsto xs atTop atBot

Full source

theorem exists_seq_antitone_tendsto_atTop_atBot (α : Type*) [Preorder α] [Nonempty α]
    [IsDirected α (· ≥ ·)] [(atBot : Filter α).IsCountablyGenerated] :
    ∃ xs : ℕ → α, Antitone xs ∧ Tendsto xs atTop atBot :=
  exists_seq_monotone_tendsto_atTop_atTop αᵒᵈ

Existence of Antitone Sequence Tending to $\mathrm{atBot}$ in Directed Preorders

Informal description

Let $\alpha$ be a nonempty preorder where the relation $\geq$ is directed (i.e., any two elements have a common lower bound) and the filter $\mathrm{atBot}$ on $\alpha$ is countably generated. Then there exists an antitone sequence $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $x_n \to \mathrm{atBot}$ as $n \to \infty$.

Filter.tendsto_iff_seq_tendsto theorem

 {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
  Tendsto f k l ↔ ∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Full source

/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
if a filter `k` is countably generated then `Tendsto f k l` iff for every sequence `u`
converging to `k`, `f ∘ u` tends to `l`. -/
theorem tendsto_iff_seq_tendsto {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
    TendstoTendsto f k l ↔ ∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l := by
  refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
  contrapose! H
  have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
  rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
  rw [tendsto_inf, tendsto_principal] at hx
  refine ⟨x, hx.1, fun h => ?_⟩
  rcases (hx.2.and (h hs)).exists with ⟨N, hnmem, hmem⟩
  exact hnmem hmem

Sequential Characterization of Filter Convergence: $f \to l$ along $k$ iff all sequences converging to $k$ compose to sequences converging to $l$

Informal description

For a function $f \colon \alpha \to \beta$ and filters $k$ on $\alpha$ and $l$ on $\beta$, where $k$ is countably generated, the following are equivalent: 1. $f$ tends to $l$ along $k$; 2. For every sequence $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ that tends to $k$, the composition $(f(x_n))_{n \in \mathbb{N}}$ tends to $l$.

Filter.tendsto_of_seq_tendsto theorem

 {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
  (∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l) → Tendsto f k l

Full source

theorem tendsto_of_seq_tendsto {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated] :
    (∀ x : ℕ → α, Tendsto x atTop k → Tendsto (f ∘ x) atTop l) → Tendsto f k l :=
  tendsto_iff_seq_tendsto.2

Convergence via Sequences Implies Filter Convergence

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $k$ be a countably generated filter on $\alpha$ and $l$ a filter on $\beta$. If for every sequence $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ that tends to $k$, the sequence $(f(x_n))_{n \in \mathbb{N}}$ tends to $l$, then $f$ tends to $l$ along $k$.

Filter.eventually_iff_seq_eventually theorem

 {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
  (∀ᶠ n in l, p n) ↔ ∀ x : ℕ → ι, Tendsto x atTop l → ∀ᶠ n : ℕ in atTop, p (x n)

Full source

theorem eventually_iff_seq_eventually {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] :
    (∀ᶠ n in l, p n) ↔ ∀ x : ℕ → ι, Tendsto x atTop l → ∀ᶠ n : ℕ in atTop, p (x n) := by
  simpa using tendsto_iff_seq_tendsto (f := id) (l := 𝓟 {x | p x})

Eventual Property via Sequences: $p$ holds eventually for $l$ iff all sequences converging to $l$ satisfy $p$ eventually

Informal description

For a countably generated filter $l$ on a type $\iota$ and a predicate $p : \iota \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $p$ holds eventually for $l$; 2. For every sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ that tends to $l$, the predicate $p(x_n)$ holds eventually as $n \to \infty$.

Filter.frequently_iff_seq_frequently theorem

 {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
  (∃ᶠ n in l, p n) ↔ ∃ x : ℕ → ι, Tendsto x atTop l ∧ ∃ᶠ n : ℕ in atTop, p (x n)

Full source

theorem frequently_iff_seq_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] :
    (∃ᶠ n in l, p n) ↔ ∃ x : ℕ → ι, Tendsto x atTop l ∧ ∃ᶠ n : ℕ in atTop, p (x n) := by
  simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]
  push_neg; rfl

Frequent Property via Sequences: $p$ holds frequently for $l$ iff there exists a sequence converging to $l$ where $p$ holds frequently.

Informal description

For a countably generated filter $l$ on a type $\iota$ and a predicate $p : \iota \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $p$ holds frequently for $l$ (i.e., $p$ does not eventually hold for $\neg p$); 2. There exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ that tends to $l$ such that $p(x_n)$ holds frequently as $n \to \infty$.

Filter.exists_seq_forall_of_frequently theorem

 {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] (h : ∃ᶠ n in l, p n) :
  ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n)

Full source

theorem exists_seq_forall_of_frequently {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] (h : ∃ᶠ n in l, p n) :
    ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n) := by
  rw [frequently_iff_seq_frequently] at h
  obtain ⟨x, hx_tendsto, hx_freq⟩ := h
  obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq
  exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩

Existence of Sequence Satisfying Predicate Along a Countably Generated Filter

Informal description

For a countably generated filter $l$ on a type $\iota$ and a predicate $p : \iota \to \mathrm{Prop}$, if $p$ holds frequently for $l$ (i.e., $\existsᶠ n \text{ in } l, p(n)$), then there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ such that: 1. The sequence $x_n$ tends to $l$ as $n \to \infty$, and 2. $p(x_n)$ holds for all $n \in \mathbb{N}$.

Filter.frequently_iff_seq_forall theorem

 {ι : Type*} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] :
  (∃ᶠ n in l, p n) ↔ ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n)

Full source

lemma frequently_iff_seq_forall {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] :
    (∃ᶠ n in l, p n) ↔ ∃ ns : ℕ → ι, Tendsto ns atTop l ∧ ∀ n, p (ns n) :=
  ⟨exists_seq_forall_of_frequently, fun ⟨_ns, hnsl, hpns⟩ ↦
    hnsl.frequently <| Frequently.of_forall hpns⟩

Frequent Property via Sequences: $p$ holds frequently for $l$ iff there exists a sequence converging to $l$ where $p$ always holds

Informal description

For a countably generated filter $l$ on a type $\iota$ and a predicate $p : \iota \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $p$ holds frequently for $l$ (i.e., $p$ does not eventually hold for $\neg p$); 2. There exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ that tends to $l$ such that $p(x_n)$ holds for all $n \in \mathbb{N}$.

Filter.tendsto_of_subseq_tendsto theorem

 {ι : Type*} {x : ι → α} {f : Filter α} {l : Filter ι} [l.IsCountablyGenerated]
  (hxy : ∀ ns : ℕ → ι, Tendsto ns atTop l → ∃ ms : ℕ → ℕ, Tendsto (fun n => x (ns <| ms n)) atTop f) : Tendsto x l f

Full source

/-- A sequence converges if every subsequence has a convergent subsequence. -/
theorem tendsto_of_subseq_tendsto {ι : Type*} {x : ι → α} {f : Filter α} {l : Filter ι}
    [l.IsCountablyGenerated]
    (hxy : ∀ ns : ℕ → ι, Tendsto ns atTop l →
      ∃ ms : ℕ → ℕ, Tendsto (fun n => x (ns <| ms n)) atTop f) :
    Tendsto x l f := by
  contrapose! hxy
  obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by
    rwa [not_tendsto_iff_exists_frequently_nmem] at hxy
  obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
  refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩
  rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩
  exact absurd hn <| hy_freq _

Convergence via Subsequence Convergence for Countably Generated Filters

Informal description

Let $\iota$ and $\alpha$ be types, $x : \iota \to \alpha$ a function, $f$ a filter on $\alpha$, and $l$ a countably generated filter on $\iota$. If for every sequence $(n_k)_{k \in \mathbb{N}}$ in $\iota$ that tends to $l$, there exists a subsequence $(n_{k_m})_{m \in \mathbb{N}}$ such that $(x(n_{k_m}))_{m \in \mathbb{N}}$ tends to $f$, then $x$ tends to $f$ along $l$.

Filter.subseq_tendsto_of_neBot theorem

 {f : Filter α} [IsCountablyGenerated f] {u : ℕ → α} (hx : NeBot (f ⊓ map u atTop)) :
  ∃ θ : ℕ → ℕ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Full source

theorem subseq_tendsto_of_neBot {f : Filter α} [IsCountablyGenerated f] {u : ℕ → α}
    (hx : NeBot (f ⊓ map u atTop)) : ∃ θ : ℕ → ℕ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f := by
  rw [← Filter.push_pull', map_neBot_iff] at hx
  rcases exists_seq_tendsto (comapcomap u f ⊓ atTop) with ⟨φ, hφ⟩
  rw [tendsto_inf, tendsto_comap_iff] at hφ
  obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ) :=
    strictMono_subseq_of_tendsto_atTop hφ.2
  exact ⟨φ ∘ ψ, hψφ, hφ.1.comp hψ.tendsto_atTop⟩

Existence of a Convergent Subsequence for a Nontrivial Countably Generated Filter

Informal description

Let $f$ be a countably generated filter on a type $\alpha$, and let $u : \mathbb{N} \to \alpha$ be a sequence such that the filter $f \sqcap \mathrm{map}\, u\, \mathrm{atTop}$ is nontrivial (i.e., not the bottom filter). Then there exists a strictly increasing function $\theta : \mathbb{N} \to \mathbb{N}$ such that the subsequence $u \circ \theta$ tends to $f$ as $n \to \infty$.