Mathlib.Order.LiminfLimsup

Filter.limsSup definition

(f : Filter α) : α

Full source

/-- The `limsSup` of a filter `f` is the infimum of the `a` such that, eventually for `f`,
holds `x ≤ a`. -/
def limsSup (f : Filter α) : α :=
  sInf { a | ∀ᶠ n in f, n ≤ a }

Limit superior of a filter

Informal description

The limit superior of a filter $ f $ on a conditionally complete lattice $ \alpha $ is the infimum of the set of all elements $ a \in \alpha $ such that $ n \leq a $ holds eventually for $ n $ in $ f $. In other words, it is the smallest element $ a $ for which the set $\{ n \mid n \leq a \}$ is in the filter $ f $.

Filter.limsInf definition

(f : Filter α) : α

Full source

/-- The `limsInf` of a filter `f` is the supremum of the `a` such that, eventually for `f`,
holds `x ≥ a`. -/
def limsInf (f : Filter α) : α :=
  sSup { a | ∀ᶠ n in f, a ≤ n }

Limit inferior of a filter

Informal description

The limit inferior of a filter $ f $ on a conditionally complete lattice $ \alpha $ is the supremum of all elements $ a \in \alpha $ such that $ a \leq n $ holds eventually for $ n $ in $ f $. In other words, it is the largest element $ a $ for which the set $\{ n \mid a \leq n \}$ is in the filter $ f $.

Filter.limsup definition

(u : β → α) (f : Filter β) : α

Full source

/-- The `limsup` of a function `u` along a filter `f` is the infimum of the `a` such that,
eventually for `f`, holds `u x ≤ a`. -/
def limsup (u : β → α) (f : Filter β) : α :=
  limsSup (map u f)

Limit superior of a function along a filter

Informal description

The limit superior of a function $ u : \beta \to \alpha $ along a filter $ f $ on $ \beta $ is the infimum of all elements $ a $ in the conditionally complete lattice $ \alpha $ such that $ u(x) \leq a $ holds for $ f $-almost all $ x $. In other words, it is the smallest element $ a $ for which the set $\{ x \mid u(x) \leq a \}$ belongs to the filter $ f $.

Filter.liminf definition

(u : β → α) (f : Filter β) : α

Full source

/-- The `liminf` of a function `u` along a filter `f` is the supremum of the `a` such that,
eventually for `f`, holds `u x ≥ a`. -/
def liminf (u : β → α) (f : Filter β) : α :=
  limsInf (map u f)

Limit inferior of a function along a filter

Informal description

The limit inferior of a function $ u : \beta \to \alpha $ along a filter $ f $ on $ \beta $ is the supremum of all elements $ a \in \alpha $ such that $ u(x) \geq a $ holds eventually for $ x $ in $ f $. Here, $ \alpha $ is a conditionally complete lattice. In other words, it is the largest element $ a $ for which the set $\{ x \mid u(x) \geq a \}$ belongs to the filter $ f $.

Filter.blimsup definition

(u : β → α) (f : Filter β) (p : β → Prop)

Full source

/-- The `blimsup` of a function `u` along a filter `f`, bounded by a predicate `p`, is the infimum
of the `a` such that, eventually for `f`, `u x ≤ a` whenever `p x` holds. -/
def blimsup (u : β → α) (f : Filter β) (p : β → Prop) :=
  sInf { a | ∀ᶠ x in f, p x → u x ≤ a }

Bounded limit superior of a function along a filter

Informal description

The bounded limit superior (blimsup) of a function $ u : \beta \to \alpha $ along a filter $ f $ on $ \beta $, with respect to a predicate $ p : \beta \to \text{Prop} $, is the infimum of all $ a \in \alpha $ such that, for $ f $-almost all $ x $, whenever $ p x $ holds, $ u x \leq a $. In other words, it is the smallest element $ a $ of the conditionally complete lattice $ \alpha $ for which the inequality $ u x \leq a $ holds whenever $ p x $ is true, for all $ x $ in a set that is eventually in the filter $ f $.

Filter.bliminf definition

(u : β → α) (f : Filter β) (p : β → Prop)

Full source

/-- The `bliminf` of a function `u` along a filter `f`, bounded by a predicate `p`, is the supremum
of the `a` such that, eventually for `f`, `a ≤ u x` whenever `p x` holds. -/
def bliminf (u : β → α) (f : Filter β) (p : β → Prop) :=
  sSup { a | ∀ᶠ x in f, p x → a ≤ u x }

Bounded limit inferior of a function along a filter

Informal description

The bounded limit inferior (bliminf) of a function $ u : \beta \to \alpha $ along a filter $ f $ on $ \beta $, with respect to a predicate $ p : \beta \to \text{Prop} $, is the supremum of all $ a \in \alpha $ such that, for $ f $-almost all $ x $, whenever $ p x $ holds, $ a \leq u x $. In other words, it is the largest element $ a $ of the conditionally complete lattice $ \alpha $ for which the inequality $ a \leq u x $ holds whenever $ p x $ is true, for all $ x $ in a set that is eventually in the filter $ f $.

Filter.limsup_eq theorem

: limsup u f = sInf {a | ∀ᶠ n in f, u n ≤ a}

Full source

theorem limsup_eq : limsup u f = sInf { a | ∀ᶠ n in f, u n ≤ a } :=
  rfl

Characterization of Limit Superior as Infimum of Upper Bounds

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $u : \beta \to \alpha$ a function, and $f$ a filter on $\beta$. The limit superior of $u$ along $f$ is equal to the infimum of all elements $a \in \alpha$ such that $u(n) \leq a$ holds for $f$-almost all $n$. In symbols: \[ \limsup_{n \to f} u(n) = \inf \{a \in \alpha \mid \forall^f n, u(n) \leq a\}. \]

Filter.liminf_eq theorem

: liminf u f = sSup {a | ∀ᶠ n in f, a ≤ u n}

Full source

theorem liminf_eq : liminf u f = sSup { a | ∀ᶠ n in f, a ≤ u n } :=
  rfl

Characterization of Limit Inferior as Supremum of Lower Bounds

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. The limit inferior of $u$ along $f$ is equal to the supremum of all elements $a \in \alpha$ such that $a \leq u(n)$ holds for $f$-almost all $n \in \beta$. In symbols: \[ \liminf_{f} u = \sup \{a \in \alpha \mid \forall^f n, a \leq u(n)\} \]

Filter.blimsup_eq theorem

: blimsup u f p = sInf {a | ∀ᶠ x in f, p x → u x ≤ a}

Full source

theorem blimsup_eq : blimsup u f p = sInf { a | ∀ᶠ x in f, p x → u x ≤ a } :=
  rfl

Characterization of Bounded Limit Superior as Infimum of Upper Bounds

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $u : \beta \to \alpha$ a function, $f$ a filter on $\beta$, and $p : \beta \to \text{Prop}$ a predicate. The bounded limit superior of $u$ along $f$ with respect to $p$ is equal to the infimum of all elements $a \in \alpha$ such that for $f$-almost all $x$, if $p(x)$ holds then $u(x) \leq a$. In symbols: \[ \text{blimsup}_{x \to f} u(x) \mid p(x) = \inf \{a \in \alpha \mid \forall^f x, p(x) \implies u(x) \leq a\}. \]

Filter.bliminf_eq theorem

: bliminf u f p = sSup {a | ∀ᶠ x in f, p x → a ≤ u x}

Full source

theorem bliminf_eq : bliminf u f p = sSup { a | ∀ᶠ x in f, p x → a ≤ u x } :=
  rfl

Characterization of Bounded Limit Inferior via Supremum of Lower Bounds

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $f$ a filter on $\beta$, $p : \beta \to \text{Prop}$ a predicate, and $u : \beta \to \alpha$ a function. The bounded limit inferior of $u$ along $f$ with respect to $p$ is equal to the supremum of all elements $a \in \alpha$ such that for $f$-almost all $x$, whenever $p(x)$ holds, we have $a \leq u(x)$. In symbols: \[ \text{bliminf}_{f,p} u = \sup \{a \in \alpha \mid \forall^f x, p(x) \to a \leq u(x)\} \]

Filter.liminf_comp theorem

(u : β → α) (v : γ → β) (f : Filter γ) : liminf (u ∘ v) f = liminf u (map v f)

Full source

lemma liminf_comp (u : β → α) (v : γ → β) (f : Filter γ) :
    liminf (u ∘ v) f = liminf u (map v f) := rfl

Limit Inferior of Composition Equals Limit Inferior under Pushforward Filter

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ and $\gamma$ types, $u : \beta \to \alpha$ a function, $v : \gamma \to \beta$ a function, and $f$ a filter on $\gamma$. The limit inferior of the composition $u \circ v$ along $f$ is equal to the limit inferior of $u$ along the image filter of $v$ under $f$. In symbols: \[ \liminf_{x \to f} (u \circ v)(x) = \liminf_{y \to v_*f} u(y) \] where $v_*f$ denotes the pushforward of the filter $f$ under $v$.

Filter.limsup_comp theorem

(u : β → α) (v : γ → β) (f : Filter γ) : limsup (u ∘ v) f = limsup u (map v f)

Full source

lemma limsup_comp (u : β → α) (v : γ → β) (f : Filter γ) :
    limsup (u ∘ v) f = limsup u (map v f) := rfl

Limit Superior of Composition Equals Limit Superior under Pushforward Filter

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ and $\gamma$ types, $u : \beta \to \alpha$ a function, $v : \gamma \to \beta$ a function, and $f$ a filter on $\gamma$. The limit superior of the composition $u \circ v$ along $f$ is equal to the limit superior of $u$ along the pushforward filter of $f$ under $v$. In symbols: \[ \limsup_{x \to f} (u \circ v)(x) = \limsup_{y \to v_*f} u(y) \] where $v_*f$ denotes the image filter of $f$ under $v$.

Filter.blimsup_true theorem

(f : Filter β) (u : β → α) : (blimsup u f fun _ => True) = limsup u f

Full source

@[simp]
theorem blimsup_true (f : Filter β) (u : β → α) : (blimsup u f fun _ => True) = limsup u f := by
  simp [blimsup_eq, limsup_eq]

Bounded Limit Superior with True Predicate Equals Limit Superior

Informal description

For any filter $f$ on a type $\beta$ and any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, the bounded limit superior of $u$ along $f$ with respect to the always-true predicate is equal to the limit superior of $u$ along $f$. In symbols: \[ \text{blimsup}_{x \to f} \, u(x) \, (\text{fun } \_ \Rightarrow \text{True}) = \text{limsup}_{x \to f} \, u(x) \]

Filter.bliminf_true theorem

(f : Filter β) (u : β → α) : (bliminf u f fun _ => True) = liminf u f

Full source

@[simp]
theorem bliminf_true (f : Filter β) (u : β → α) : (bliminf u f fun _ => True) = liminf u f := by
  simp [bliminf_eq, liminf_eq]

Bounded Limit Inferior with True Predicate Equals Limit Inferior

Informal description

For any filter $f$ on a type $\beta$ and any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, the bounded limit inferior of $u$ with respect to $f$ and the always-true predicate equals the limit inferior of $u$ with respect to $f$. That is, \[ \text{bliminf}_{x \in f} \, u(x) \, (\text{True}) = \text{liminf}_{x \in f} \, u(x). \]

Filter.blimsup_eq_limsup theorem

{f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x})

Full source

lemma blimsup_eq_limsup {f : Filter β} {u : β → α} {p : β → Prop} :
    blimsup u f p = limsup u (f ⊓ 𝓟 {x | p x}) := by
  simp only [blimsup_eq, limsup_eq, eventually_inf_principal, mem_setOf_eq]

Bounded Limit Superior Equals Limit Superior on Restricted Filter

Informal description

Let $f$ be a filter on a type $\beta$, $u : \beta \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $p : \beta \to \text{Prop}$ a predicate. Then the bounded limit superior of $u$ with respect to $p$ along $f$ is equal to the limit superior of $u$ along the filter $f$ restricted to the set $\{x \mid p x\}$. In other words, we have: \[ \text{blimsup}_{f} u p = \text{limsup}_{f \sqcap \mathcal{P}\{x \mid p x\}} u \] where $\mathcal{P}\{x \mid p x\}$ denotes the principal filter generated by the set $\{x \mid p x\}$.

Filter.bliminf_eq_liminf theorem

{f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = liminf u (f ⊓ 𝓟 {x | p x})

Full source

lemma bliminf_eq_liminf {f : Filter β} {u : β → α} {p : β → Prop} :
    bliminf u f p = liminf u (f ⊓ 𝓟 {x | p x}) :=
  blimsup_eq_limsup (α := αᵒᵈ)

Bounded Limit Inferior Equals Limit Inferior on Restricted Filter

Informal description

Let $f$ be a filter on a type $\beta$, $u : \beta \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $p : \beta \to \text{Prop}$ a predicate. Then the bounded limit inferior of $u$ with respect to $p$ along $f$ is equal to the limit inferior of $u$ along the filter $f$ restricted to the set $\{x \mid p x\}$. In other words, we have: \[ \text{bliminf}_{f} u p = \text{liminf}_{f \sqcap \mathcal{P}\{x \mid p x\}} u \] where $\mathcal{P}\{x \mid p x\}$ denotes the principal filter generated by the set $\{x \mid p x\}$.

Filter.blimsup_eq_limsup_subtype theorem

 {f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = limsup (u ∘ ((↑) : {x | p x} → β)) (comap (↑) f)

Full source

theorem blimsup_eq_limsup_subtype {f : Filter β} {u : β → α} {p : β → Prop} :
    blimsup u f p = limsup (u ∘ ((↑) : { x | p x } → β)) (comap (↑) f) := by
  rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]

Bounded Limit Superior Equals Limit Superior via Subtype Restriction

Informal description

Let $f$ be a filter on a type $\beta$, $u : \beta \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $p : \beta \to \text{Prop}$ a predicate. Then the bounded limit superior of $u$ with respect to $p$ along $f$ is equal to the limit superior of the composition $u \circ \iota$, where $\iota : \{x \mid p x\} \to \beta$ is the inclusion map, along the filter obtained by pulling back $f$ via $\iota$. In other words, we have: \[ \text{blimsup}_f u p = \text{limsup}_{f \circ \iota} (u \circ \iota) \] where $\iota$ is the inclusion of the subtype $\{x \mid p x\}$ into $\beta$.

Filter.bliminf_eq_liminf_subtype theorem

 {f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = liminf (u ∘ ((↑) : {x | p x} → β)) (comap (↑) f)

Full source

theorem bliminf_eq_liminf_subtype {f : Filter β} {u : β → α} {p : β → Prop} :
    bliminf u f p = liminf (u ∘ ((↑) : { x | p x } → β)) (comap (↑) f) :=
  blimsup_eq_limsup_subtype (α := αᵒᵈ)

Bounded Limit Inferior Equals Limit Inferior via Subtype Restriction

Informal description

Let $f$ be a filter on a type $\beta$, $u : \beta \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $p : \beta \to \text{Prop}$ a predicate. Then the bounded limit inferior of $u$ with respect to $p$ along $f$ is equal to the limit inferior of the composition $u \circ \iota$, where $\iota : \{x \mid p x\} \to \beta$ is the inclusion map, along the filter obtained by pulling back $f$ via $\iota$. In other words, we have: \[ \text{bliminf}_f u p = \text{liminf}_{f \circ \iota} (u \circ \iota) \] where $\iota$ is the inclusion of the subtype $\{x \mid p x\}$ into $\beta$.

Filter.limsSup_principal_eq_csSup theorem

(h : BddAbove s) (hs : s.Nonempty) : limsSup (𝓟 s) = sSup s

Full source

lemma limsSup_principal_eq_csSup (h : BddAbove s) (hs : s.Nonempty) : limsSup (𝓟 s) = sSup s := by
  simp only [limsSup, eventually_principal]; exact csInf_upperBounds_eq_csSup h hs

Limit Superior of Principal Filter Equals Supremum for Bounded Above Sets

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded above. Then the limit superior of the principal filter generated by $s$ equals the supremum of $s$, i.e., \[ \limsup (\mathcal{P}(s)) = \sup s. \]

Filter.limsInf_principal_eq_csSup theorem

(h : BddBelow s) (hs : s.Nonempty) : limsInf (𝓟 s) = sInf s

Full source

lemma limsInf_principal_eq_csSup (h : BddBelow s) (hs : s.Nonempty) : limsInf (𝓟 s) = sInf s :=
  limsSup_principal_eq_csSup (α := αᵒᵈ) h hs

Limit Inferior of Principal Filter Equals Infimum for Bounded Below Sets

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. Then the limit inferior of the principal filter generated by $s$ equals the infimum of $s$, i.e., \[ \liminf (\mathcal{P}(s)) = \inf s. \]

Filter.limsup_top_eq_ciSup theorem

[Nonempty β] (hu : BddAbove (range u)) : limsup u ⊤ = ⨆ i, u i

Full source

lemma limsup_top_eq_ciSup [Nonempty β] (hu : BddAbove (range u)) : limsup u ⊤ = ⨆ i, u i := by
  rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]

Limit Superior of Function Along Top Filter Equals Indexed Supremum for Bounded Above Range

Informal description

Let $\beta$ be a nonempty type and $u : \beta \to \alpha$ a function with bounded above range in a conditionally complete lattice $\alpha$. Then the limit superior of $u$ along the top filter equals the supremum of $u$ over $\beta$, i.e., \[ \limsup u \top = \bigsqcup_{i \in \beta} u_i. \]

Filter.liminf_top_eq_ciInf theorem

[Nonempty β] (hu : BddBelow (range u)) : liminf u ⊤ = ⨅ i, u i

Full source

lemma liminf_top_eq_ciInf [Nonempty β] (hu : BddBelow (range u)) : liminf u ⊤ = ⨅ i, u i := by
  rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]

Limit Inferior of Function Along Top Filter Equals Indexed Infimum for Bounded Below Range

Informal description

Let $\beta$ be a nonempty type and $u : \beta \to \alpha$ a function with bounded below range in a conditionally complete lattice $\alpha$. Then the limit inferior of $u$ along the top filter equals the infimum of $u$ over $\beta$, i.e., \[ \liminf u \top = \bigsqcap_{i \in \beta} u_i. \]

Filter.limsup_congr theorem

 {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ a in f, u a = v a) :
  limsup u f = limsup v f

Full source

theorem limsup_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β}
    (h : ∀ᶠ a in f, u a = v a) : limsup u f = limsup v f := by
  rw [limsup_eq]
  congr with b
  exact eventually_congr (h.mono fun x hx => by simp [hx])

Limit Superior is Invariant under Almost Everywhere Equality

Informal description

Let $\alpha$ be a type and $\beta$ a conditionally complete lattice. Given a filter $f$ on $\alpha$ and two functions $u, v \colon \alpha \to \beta$ such that $u(a) = v(a)$ holds for $f$-almost all $a \in \alpha$, the limit superiors of $u$ and $v$ along $f$ are equal, i.e., \[ \limsup_{a \to f} u(a) = \limsup_{a \to f} v(a). \]

Filter.blimsup_congr theorem

 {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) : blimsup u f p = blimsup v f p

Full source

theorem blimsup_congr {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) :
    blimsup u f p = blimsup v f p := by
  simpa only [blimsup_eq_limsup] using limsup_congr <| eventually_inf_principal.2 h

Bounded Limit Superior is Invariant under Almost Everywhere Equality on Predicate

Informal description

Let $f$ be a filter on a type $\beta$, $u, v \colon \beta \to \alpha$ functions into a conditionally complete lattice $\alpha$, and $p \colon \beta \to \text{Prop}$ a predicate. If for $f$-almost all $a \in \beta$, $p(a)$ implies $u(a) = v(a)$, then the bounded limit superiors of $u$ and $v$ with respect to $p$ along $f$ are equal, i.e., \[ \text{blimsup}_f u p = \text{blimsup}_f v p. \]

Filter.bliminf_congr theorem

 {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) : bliminf u f p = bliminf v f p

Full source

theorem bliminf_congr {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) :
    bliminf u f p = bliminf v f p :=
  blimsup_congr (α := αᵒᵈ) h

Bounded Limit Inferior is Invariant under Almost Everywhere Equality on Predicate

Informal description

Let $f$ be a filter on a type $\beta$, $u, v \colon \beta \to \alpha$ functions into a conditionally complete lattice $\alpha$, and $p \colon \beta \to \text{Prop}$ a predicate. If for $f$-almost all $a \in \beta$, $p(a)$ implies $u(a) = v(a)$, then the bounded limit inferiors of $u$ and $v$ with respect to $p$ along $f$ are equal, i.e., \[ \text{bliminf}_f u p = \text{bliminf}_f v p. \]

Filter.liminf_congr theorem

 {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ a in f, u a = v a) :
  liminf u f = liminf v f

Full source

theorem liminf_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β}
    (h : ∀ᶠ a in f, u a = v a) : liminf u f = liminf v f :=
  limsup_congr (β := βᵒᵈ) h

Limit Inferior is Invariant under Almost Everywhere Equality

Informal description

Let $\alpha$ be a type and $\beta$ a conditionally complete lattice. Given a filter $f$ on $\alpha$ and two functions $u, v \colon \alpha \to \beta$ such that $u(a) = v(a)$ holds for $f$-almost all $a \in \alpha$, the limit inferiors of $u$ and $v$ along $f$ are equal, i.e., \[ \liminf_{a \to f} u(a) = \liminf_{a \to f} v(a). \]

Filter.limsup_const theorem

{α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) : limsup (fun _ => b) f = b

Full source

@[simp]
theorem limsup_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f]
    (b : β) : limsup (fun _ => b) f = b := by
  simpa only [limsup_eq, eventually_const] using csInf_Ici

Limit Superior of a Constant Function Equals the Constant

Informal description

Let $\beta$ be a conditionally complete lattice, $\alpha$ a type, and $f$ a nontrivial filter on $\alpha$. For any constant function $u(x) = b$ where $b \in \beta$, the limit superior of $u$ along $f$ is equal to $b$, i.e., \[ \limsup_{f} u = b. \]

Filter.liminf_const theorem

{α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) : liminf (fun _ => b) f = b

Full source

@[simp]
theorem liminf_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f]
    (b : β) : liminf (fun _ => b) f = b :=
  limsup_const (β := βᵒᵈ) b

Limit Inferior of a Constant Function Equals the Constant

Informal description

Let $\beta$ be a conditionally complete lattice, $\alpha$ a type, and $f$ a nontrivial filter on $\alpha$. For any constant function $u(x) = b$ where $b \in \beta$, the limit inferior of $u$ along $f$ is equal to $b$, i.e., \[ \liminf_{f} u = b. \]

Filter.HasBasis.liminf_eq_sSup_iUnion_iInter theorem

 {ι ι' : Type*} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :
  liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i))

Full source

theorem HasBasis.liminf_eq_sSup_iUnion_iInter {ι ι' : Type*} {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :
    liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i)) := by
  simp_rw [liminf_eq, hv.eventually_iff]
  congr
  ext x
  simp only [mem_setOf_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists,
    exists_prop]

Limit Inferior as Supremum of Union of Intersections of Lower Sets

Informal description

Let $\alpha$ be a conditionally complete lattice, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a basis consisting of sets $s(j)$ indexed by $j \in \iota'$ satisfying a predicate $p$. Then the limit inferior of $f$ along $v$ is equal to the supremum of the union over all $j$ (with $p(j)$) of the intersections over $i \in s(j)$ of the lower sets $Iic(f(i))$. In symbols: \[ \liminf_{v} f = \sup \left( \bigcup_{j : p(j)} \bigcap_{i \in s(j)} (-\infty, f(i)] \right). \]

Filter.HasBasis.liminf_eq_sSup_univ_of_empty theorem

 {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :
  liminf f v = sSup univ

Full source

theorem HasBasis.liminf_eq_sSup_univ_of_empty {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :
    liminf f v = sSup univ := by
  simp [hv.eq_bot_iff.2 ⟨i, hi, h'i⟩, liminf_eq]

Limit Inferior Equals Supremum of Universal Set When Filter Basis Contains Empty Set

Informal description

Let $f : \iota \to \alpha$ be a function, $v$ a filter on $\iota$, and suppose $v$ has a basis consisting of sets $s(i')$ indexed by predicates $p(i')$ (i.e., $v$ is generated by $\{s(i') \mid p(i') \text{ holds}\}$). If there exists an index $i$ such that $p(i)$ holds and $s(i) = \emptyset$, then the limit inferior of $f$ along $v$ equals the supremum of the universal set in $\alpha$, i.e., \[ \liminf_{v} f = \sup \text{univ}. \]

Filter.HasBasis.limsup_eq_sInf_iUnion_iInter theorem

 {ι ι' : Type*} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :
  limsup f v = sInf (⋃ (j : Subtype p), ⋂ (i : s j), Ici (f i))

Full source

theorem HasBasis.limsup_eq_sInf_iUnion_iInter {ι ι' : Type*} {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :
    limsup f v = sInf (⋃ (j : Subtype p), ⋂ (i : s j), Ici (f i)) :=
  HasBasis.liminf_eq_sSup_iUnion_iInter (α := αᵒᵈ) hv

Limit Superior as Infimum of Union of Intersections of Upper Sets

Informal description

Let $\alpha$ be a conditionally complete lattice, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a basis consisting of sets $s(j)$ indexed by $j \in \iota'$ satisfying a predicate $p$. Then the limit superior of $f$ along $v$ is equal to the infimum of the union over all $j$ (with $p(j)$) of the intersections over $i \in s(j)$ of the upper sets $Ici(f(i))$. In symbols: \[ \limsup_{v} f = \inf \left( \bigcup_{j : p(j)} \bigcap_{i \in s(j)} [f(i), \infty) \right). \]

Filter.HasBasis.limsup_eq_sInf_univ_of_empty theorem

 {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :
  limsup f v = sInf univ

Full source

theorem HasBasis.limsup_eq_sInf_univ_of_empty {f : ι → α} {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :
    limsup f v = sInf univ :=
  HasBasis.liminf_eq_sSup_univ_of_empty (α := αᵒᵈ) hv i hi h'i

Limit Superior Equals Infimum of Universal Set When Filter Basis Contains Empty Set

Informal description

Let $f : \iota \to \alpha$ be a function, $v$ a filter on $\iota$, and suppose $v$ has a basis consisting of sets $s(i')$ indexed by predicates $p(i')$ (i.e., $v$ is generated by $\{s(i') \mid p(i') \text{ holds}\}$). If there exists an index $i$ such that $p(i)$ holds and $s(i) = \emptyset$, then the limit superior of $f$ along $v$ equals the infimum of the universal set in $\alpha$, i.e., \[ \limsup_{v} f = \inf \text{univ}. \]

Filter.liminf_nat_add theorem

(f : ℕ → α) (k : ℕ) : liminf (fun i => f (i + k)) atTop = liminf f atTop

Full source

@[simp]
theorem liminf_nat_add (f : ℕ → α) (k : ℕ) :
    liminf (fun i => f (i + k)) atTop = liminf f atTop := by
  rw [← Function.comp_def, liminf, liminf, ← map_map, map_add_atTop_eq_nat]

Limit Inferior Invariance under Index Shift in $\mathbb{N}$

Informal description

For any function $f \colon \mathbb{N} \to \alpha$ and any natural number $k$, the limit inferior of the sequence $(f(i + k))_{i \in \mathbb{N}}$ as $i \to \infty$ is equal to the limit inferior of the original sequence $(f(i))_{i \in \mathbb{N}}$. In other words, shifting the index of the sequence by $k$ does not change its limit inferior.

Filter.limsup_nat_add theorem

(f : ℕ → α) (k : ℕ) : limsup (fun i => f (i + k)) atTop = limsup f atTop

Full source

@[simp]
theorem limsup_nat_add (f : ℕ → α) (k : ℕ) : limsup (fun i => f (i + k)) atTop = limsup f atTop :=
  @liminf_nat_add αᵒᵈ _ f k

Limit Superior Invariance under Index Shift in $\mathbb{N}$

Informal description

For any function $f \colon \mathbb{N} \to \alpha$ mapping to a conditionally complete lattice $\alpha$ and any natural number $k$, the limit superior of the shifted sequence $(f(i + k))_{i \in \mathbb{N}}$ as $i \to \infty$ is equal to the limit superior of the original sequence $(f(i))_{i \in \mathbb{N}}$.

Filter.limsSup_bot theorem

: limsSup (⊥ : Filter α) = ⊥

Full source

@[simp]
theorem limsSup_bot : limsSup (⊥ : Filter α) = ⊥ :=
  bot_unique <| sInf_le <| by simp

Limit Superior of Bottom Filter is Bottom Element

Informal description

The limit superior of the bottom filter $\bot$ in a conditionally complete lattice $\alpha$ is equal to the bottom element $\bot$ of $\alpha$.

Filter.limsup_bot theorem

(f : β → α) : limsup f ⊥ = ⊥

Full source

@[simp] theorem limsup_bot (f : β → α) : limsup f ⊥ = ⊥ := by simp [limsup]

Limit Superior of Function with Bottom Filter is Bottom Element

Informal description

For any function $f : \beta \to \alpha$ mapping to a conditionally complete lattice $\alpha$, the limit superior of $f$ with respect to the bottom filter $\bot$ on $\beta$ is equal to the bottom element $\bot$ of $\alpha$.

Filter.limsInf_bot theorem

: limsInf (⊥ : Filter α) = ⊤

Full source

@[simp]
theorem limsInf_bot : limsInf (⊥ : Filter α) = ⊤ :=
  top_unique <| le_sSup <| by simp

Limit Inferior of Bottom Filter Equals Top Element

Informal description

The limit inferior of the bottom filter $\bot$ on a conditionally complete lattice $\alpha$ is equal to the top element $\top$ of $\alpha$.

Filter.liminf_bot theorem

(f : β → α) : liminf f ⊥ = ⊤

Full source

@[simp] theorem liminf_bot (f : β → α) : liminf f ⊥ = ⊤ := by simp [liminf]

Limit Inferior of Function under Bottom Filter Equals Top Element

Informal description

For any function $f : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, the limit inferior of $f$ with respect to the bottom filter $\bot$ is equal to the top element $\top$ of $\alpha$, i.e., $\liminf_{x \to \bot} f(x) = \top$.

Filter.limsSup_top theorem

: limsSup (⊤ : Filter α) = ⊤

Full source

@[simp]
theorem limsSup_top : limsSup (⊤ : Filter α) = ⊤ :=
  top_unique <| le_sInf <| by simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

Limit Superior of Top Filter Equals Top Element

Informal description

For any conditionally complete lattice $\alpha$, the limit superior of the top filter $\top$ on $\alpha$ is equal to the top element $\top$ of $\alpha$.

Filter.limsInf_top theorem

: limsInf (⊤ : Filter α) = ⊥

Full source

@[simp]
theorem limsInf_top : limsInf (⊤ : Filter α) = ⊥ :=
  bot_unique <| sSup_le <| by simpa [eq_univ_iff_forall] using fun b hb => bot_unique <| hb _

Limit Inferior of Top Filter is Bottom Element ($\liminf \top = \bot$)

Informal description

The limit inferior of the top filter $\top$ on a conditionally complete lattice $\alpha$ is equal to the bottom element $\bot$.

Filter.blimsup_false theorem

{f : Filter β} {u : β → α} : (blimsup u f fun _ => False) = ⊥

Full source

@[simp]
theorem blimsup_false {f : Filter β} {u : β → α} : (blimsup u f fun _ => False) = ⊥ := by
  simp [blimsup_eq]

Bounded Limit Superior with False Predicate is Bottom

Informal description

For any filter $f$ on a type $\beta$ and any function $u : \beta \to \alpha$ taking values in a conditionally complete lattice $\alpha$, the bounded limit superior of $u$ with respect to the constantly false predicate is equal to the bottom element $\bot$ of $\alpha$. In other words, \[ \text{blimsup}_f u (\lambda \_. \text{False}) = \bot. \]

Filter.bliminf_false theorem

{f : Filter β} {u : β → α} : (bliminf u f fun _ => False) = ⊤

Full source

@[simp]
theorem bliminf_false {f : Filter β} {u : β → α} : (bliminf u f fun _ => False) = ⊤ := by
  simp [bliminf_eq]

Bounded Limit Inferior with False Predicate is Top

Informal description

For any filter $f$ on a type $\beta$ and any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, the bounded limit inferior of $u$ with respect to the always-false predicate is equal to the top element of $\alpha$, i.e., \[ \text{bliminf}_f u (\lambda \_. \text{False}) = \top. \]

Filter.limsup_const_bot theorem

{f : Filter β} : limsup (fun _ : β => (⊥ : α)) f = (⊥ : α)

Full source

/-- Same as limsup_const applied to `⊥` but without the `NeBot f` assumption -/
@[simp]
theorem limsup_const_bot {f : Filter β} : limsup (fun _ : β => (⊥ : α)) f = (⊥ : α) := by
  rw [limsup_eq, eq_bot_iff]
  exact sInf_le (Eventually.of_forall fun _ => le_rfl)

Limit Superior of Constant Bottom Function is Bottom

Informal description

For any filter $f$ on a type $\beta$ and any conditionally complete lattice $\alpha$, the limit superior of the constant function $\lambda \_, \bot$ along $f$ is equal to $\bot$. In other words, \[ \limsup_{x \to f} \bot = \bot. \]

Filter.liminf_const_top theorem

{f : Filter β} : liminf (fun _ : β => (⊤ : α)) f = (⊤ : α)

Full source

/-- Same as limsup_const applied to `⊤` but without the `NeBot f` assumption -/
@[simp]
theorem liminf_const_top {f : Filter β} : liminf (fun _ : β => (⊤ : α)) f = (⊤ : α) :=
  limsup_const_bot (α := αᵒᵈ)

Limit Inferior of Constant Top Function is Top

Informal description

For any filter $f$ on a type $\beta$ and any conditionally complete lattice $\alpha$, the limit inferior of the constant function $\lambda \_, \top$ along $f$ is equal to $\top$. In other words, \[ \liminf_{x \to f} \top = \top. \]

Filter.HasBasis.limsSup_eq_iInf_sSup theorem

{ι} {p : ι → Prop} {s} {f : Filter α} (h : f.HasBasis p s) : limsSup f = ⨅ (i) (_ : p i), sSup (s i)

Full source

theorem HasBasis.limsSup_eq_iInf_sSup {ι} {p : ι → Prop} {s} {f : Filter α} (h : f.HasBasis p s) :
    limsSup f = ⨅ (i) (_ : p i), sSup (s i) :=
  le_antisymm (le_iInf₂ fun i hi => sInf_le <| h.eventually_iff.2 ⟨i, hi, fun _ => le_sSup⟩)
    (le_sInf fun _ ha =>
      let ⟨_, hi, ha⟩ := h.eventually_iff.1 ha
      iInf₂_le_of_le _ hi <| sSup_le ha)

Limit Superior as Infimum of Suprema over Filter Basis

Informal description

Let $f$ be a filter on a conditionally complete lattice $\alpha$, and suppose $f$ has a basis consisting of sets $s_i$ indexed by $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the limit superior of $f$ is equal to the infimum over all indices $i$ satisfying $p_i$ of the supremum of $s_i$, i.e., \[ \text{limsSup}\, f = \bigsqcap_{i, p_i} \sup s_i. \]

Filter.HasBasis.limsInf_eq_iSup_sInf theorem

{p : ι → Prop} {s : ι → Set α} {f : Filter α} (h : f.HasBasis p s) : limsInf f = ⨆ (i) (_ : p i), sInf (s i)

Full source

theorem HasBasis.limsInf_eq_iSup_sInf {p : ι → Prop} {s : ι → Set α} {f : Filter α}
    (h : f.HasBasis p s) : limsInf f = ⨆ (i) (_ : p i), sInf (s i) :=
  HasBasis.limsSup_eq_iInf_sSup (α := αᵒᵈ) h

Limit Inferior as Supremum of Infima over Filter Basis

Informal description

Let $f$ be a filter on a conditionally complete lattice $\alpha$, and suppose $f$ has a basis consisting of sets $s_i$ indexed by $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the limit inferior of $f$ is equal to the supremum over all indices $i$ satisfying $p_i$ of the infimum of $s_i$, i.e., \[ \text{limsInf}\, f = \bigsqcup_{i, p_i} \inf s_i. \]

Filter.limsSup_eq_iInf_sSup theorem

{f : Filter α} : limsSup f = ⨅ s ∈ f, sSup s

Full source

theorem limsSup_eq_iInf_sSup {f : Filter α} : limsSup f = ⨅ s ∈ f, sSup s :=
  f.basis_sets.limsSup_eq_iInf_sSup

Limit Superior as Infimum of Suprema over Filter Sets

Informal description

For any filter $f$ on a conditionally complete lattice $\alpha$, the limit superior of $f$ is equal to the infimum of the suprema of all sets in $f$, i.e., \[ \text{limsSup}\, f = \bigsqcap_{s \in f} \sup s. \]

Filter.limsInf_eq_iSup_sInf theorem

{f : Filter α} : limsInf f = ⨆ s ∈ f, sInf s

Full source

theorem limsInf_eq_iSup_sInf {f : Filter α} : limsInf f = ⨆ s ∈ f, sInf s :=
  limsSup_eq_iInf_sSup (α := αᵒᵈ)

Limit Inferior as Supremum of Infima over Filter Sets

Informal description

For any filter $f$ on a conditionally complete lattice $\alpha$, the limit inferior of $f$ is equal to the supremum of the infima of all sets in $f$, i.e., \[ \text{limsInf}\, f = \bigsqcup_{s \in f} \inf s. \]

Filter.limsup_le_iSup theorem

{f : Filter β} {u : β → α} : limsup u f ≤ ⨆ n, u n

Full source

theorem limsup_le_iSup {f : Filter β} {u : β → α} : limsup u f ≤ ⨆ n, u n :=
  limsup_le_of_le (by isBoundedDefault) (Eventually.of_forall (le_iSup u))

Limit Superior Bounded by Supremum: $\limsup_{f} u \leq \sup_n u(n)$

Informal description

For any function $u : \beta \to \alpha$ and any filter $f$ on $\beta$, the limit superior of $u$ along $f$ is bounded above by the supremum of $u$ over all inputs, i.e., \[ \limsup_{f} u \leq \sup_{n} u(n). \]

Filter.iInf_le_liminf theorem

{f : Filter β} {u : β → α} : ⨅ n, u n ≤ liminf u f

Full source

theorem iInf_le_liminf {f : Filter β} {u : β → α} : ⨅ n, u n ≤ liminf u f :=
  le_liminf_of_le (by isBoundedDefault) (Eventually.of_forall (iInf_le u))

Infimum Bounded by Limit Inferior: $\bigsqcap_n u(n) \leq \liminf_f u$

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any filter $f$ on $\beta$, the infimum of $u$ over all inputs is less than or equal to the limit inferior of $u$ along $f$. In other words, \[ \bigsqcap_{n} u(n) \leq \liminf_{f} u. \]

Filter.limsup_eq_iInf_iSup theorem

{f : Filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a

Full source

/-- In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s` -/
theorem limsup_eq_iInf_iSup {f : Filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
  (f.basis_sets.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, id]

Limit Superior as Infimum of Suprema over Filter Sets: $\limsup_{f} u = \inf_{s \in f} \sup_{a \in s} u(a)$

Informal description

Let $\alpha$ be a complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. The limit superior of $u$ along $f$ is equal to the infimum over all sets $s$ in $f$ of the supremum of $u$ over $s$, i.e., \[ \limsup_{f} u = \bigsqcap_{s \in f} \bigsqcup_{a \in s} u(a). \]

Filter.limsup_eq_iInf_iSup_of_nat theorem

{u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i ≥ n, u i

Full source

theorem limsup_eq_iInf_iSup_of_nat {u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i ≥ n, u i :=
  (atTop_basis.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, iInf_const]; rfl

Limit Superior of a Sequence as Infimum of Tail Suprema

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a conditionally complete lattice $\alpha$, the limit superior of $u$ along the cofinite filter `atTop` is equal to the infimum over all $n \in \mathbb{N}$ of the supremum of $u(i)$ for $i \geq n$. In other words, \[ \limsup_{n \to \infty} u(n) = \inf_{n \in \mathbb{N}} \sup_{i \geq n} u(i). \]

Filter.limsup_eq_iInf_iSup_of_nat' theorem

{u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n)

Full source

theorem limsup_eq_iInf_iSup_of_nat' {u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n) := by
  simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]

Limit Superior of a Sequence as Infimum of Shifted Suprema

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a conditionally complete lattice $\alpha$, the limit superior of $u$ along the cofinite filter `atTop` is equal to the infimum over all $n \in \mathbb{N}$ of the supremum of $u(i + n)$ for $i \in \mathbb{N}$. In other words, \[ \limsup_{n \to \infty} u(n) = \inf_{n \in \mathbb{N}} \sup_{i \in \mathbb{N}} u(i + n). \]

Filter.HasBasis.limsup_eq_iInf_iSup theorem

 {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) :
  limsup u f = ⨅ (i) (_ : p i), ⨆ a ∈ s i, u a

Full source

theorem HasBasis.limsup_eq_iInf_iSup {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α}
    (h : f.HasBasis p s) : limsup u f = ⨅ (i) (_ : p i), ⨆ a ∈ s i, u a :=
  (h.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, id]

Limit Superior as Infimum of Suprema over Filter Basis

Informal description

Let $f$ be a filter on $\beta$ with a basis consisting of sets $s_i$ indexed by $\iota$ with a predicate $p : \iota \to \text{Prop}$, and let $u : \beta \to \alpha$ be a function into a conditionally complete lattice $\alpha$. Then the limit superior of $u$ along $f$ is equal to the infimum over all indices $i$ satisfying $p_i$ of the supremum of $u$ over $s_i$, i.e., \[ \limsup_{f} u = \bigsqcap_{i, p_i} \bigsqcup_{a \in s_i} u(a). \]

Filter.limsSup_principal_eq_sSup theorem

(s : Set α) : limsSup (𝓟 s) = sSup s

Full source

lemma limsSup_principal_eq_sSup (s : Set α) : limsSup (𝓟 s) = sSup s := by
  simpa only [limsSup, eventually_principal] using sInf_upperBounds_eq_csSup s

Limit Superior of Principal Filter Equals Supremum

Informal description

For any subset $s$ of a conditionally complete lattice $\alpha$, the limit superior of the principal filter generated by $s$ is equal to the supremum of $s$, i.e., $\limsup (\mathcal{P} s) = \sup s$.

Filter.limsInf_principal_eq_sInf theorem

(s : Set α) : limsInf (𝓟 s) = sInf s

Full source

lemma limsInf_principal_eq_sInf (s : Set α) : limsInf (𝓟 s) = sInf s := by
  simpa only [limsInf, eventually_principal] using sSup_lowerBounds_eq_sInf s

Limit Inferior of Principal Filter Equals Infimum

Informal description

For any subset $s$ of a conditionally complete lattice $\alpha$, the limit inferior of the principal filter generated by $s$ is equal to the infimum of $s$, i.e., $\liminf (\mathcal{P} s) = \inf s$.

Filter.limsup_top_eq_iSup theorem

(u : β → α) : limsup u ⊤ = ⨆ i, u i

Full source

@[simp] lemma limsup_top_eq_iSup (u : β → α) : limsup u ⊤ = ⨆ i, u i := by
  rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]

Limit Superior with Trivial Filter Equals Supremum of Range

Informal description

For any function $u \colon \beta \to \alpha$ mapping to a conditionally complete lattice $\alpha$, the limit superior of $u$ with respect to the trivial filter $\top$ on $\beta$ equals the supremum of the range of $u$, i.e., \[ \limsup_{\top} u = \bigsqcup_{i \in \beta} u(i). \]

Filter.liminf_top_eq_iInf theorem

(u : β → α) : liminf u ⊤ = ⨅ i, u i

Full source

@[simp] lemma liminf_top_eq_iInf (u : β → α) : liminf u ⊤ = ⨅ i, u i := by
  rw [liminf, map_top, limsInf_principal_eq_sInf, sInf_range]

Limit Inferior with Trivial Filter Equals Infimum of Range: $\liminf u \top = \bigsqcap_i u(i)$

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, the limit inferior of $u$ with respect to the trivial filter $\top$ on $\beta$ equals the infimum of the range of $u$, i.e., \[ \liminf u \top = \bigsqcap_{i} u(i). \]

Filter.blimsup_congr' theorem

 {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ x in f, u x ≠ ⊥ → (p x ↔ q x)) : blimsup u f p = blimsup u f q

Full source

theorem blimsup_congr' {f : Filter β} {p q : β → Prop} {u : β → α}
    (h : ∀ᶠ x in f, u x ≠ ⊥ → (p x ↔ q x)) : blimsup u f p = blimsup u f q := by
  simp only [blimsup_eq]
  congr with a
  refine eventually_congr (h.mono fun b hb => ?_)
  rcases eq_or_ne (u b) ⊥ with hu | hu; · simp [hu]
  rw [hb hu]

Bounded Limit Superior is Invariant under Predicate Equivalence Almost Everywhere

Informal description

Let $f$ be a filter on $\beta$, $p, q : \beta \to \text{Prop}$ be predicates, and $u : \beta \to \alpha$ be a function. If for almost all $x$ in $f$ (i.e., for $x$ in some set in $f$), whenever $u x \neq \bot$ we have $p x \leftrightarrow q x$, then the bounded limit superior of $u$ with respect to $p$ equals the bounded limit superior of $u$ with respect to $q$, i.e., \[ \text{blimsup}_f(u, p) = \text{blimsup}_f(u, q). \]

Filter.bliminf_congr' theorem

 {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ x in f, u x ≠ ⊤ → (p x ↔ q x)) : bliminf u f p = bliminf u f q

Full source

theorem bliminf_congr' {f : Filter β} {p q : β → Prop} {u : β → α}
    (h : ∀ᶠ x in f, u x ≠ ⊤ → (p x ↔ q x)) : bliminf u f p = bliminf u f q :=
  blimsup_congr' (α := αᵒᵈ) h

Bounded Limit Inferior is Invariant under Predicate Equivalence Almost Everywhere

Informal description

Let $f$ be a filter on $\beta$, $p, q : \beta \to \text{Prop}$ be predicates, and $u : \beta \to \alpha$ be a function. If for almost all $x$ in $f$ (i.e., for $x$ in some set in $f$), whenever $u x \neq \top$ we have $p x \leftrightarrow q x$, then the bounded limit inferior of $u$ with respect to $p$ equals the bounded limit inferior of $u$ with respect to $q$, i.e., \[ \text{bliminf}_f(u, p) = \text{bliminf}_f(u, q). \]

Filter.HasBasis.blimsup_eq_iInf_iSup theorem

 {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (hf : f.HasBasis p s) {q : β → Prop} :
  blimsup u f q = ⨅ (i) (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Full source

lemma HasBasis.blimsup_eq_iInf_iSup {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α}
    (hf : f.HasBasis p s) {q : β → Prop} :
    blimsup u f q = ⨅ (i) (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a := by
  simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and,
    mem_setOf_eq]

Bounded Limit Superior as Infimum of Suprema over Filter Basis with Predicate

Informal description

Let $f$ be a filter on $\beta$ with a basis consisting of sets $s_i$ indexed by $\iota$ with a predicate $p : \iota \to \text{Prop}$, and let $u : \beta \to \alpha$ be a function into a conditionally complete lattice $\alpha$. For any predicate $q : \beta \to \text{Prop}$, the bounded limit superior of $u$ with respect to $q$ along $f$ is equal to the infimum over all indices $i$ satisfying $p_i$ of the supremum of $u(a)$ over all $a \in s_i$ that satisfy $q(a)$. In other words, we have: \[ \text{blimsup}_f(u, q) = \bigsqcap_{i, p_i} \bigsqcup_{\substack{a \in s_i \\ q(a)}} u(a). \]

Filter.blimsup_eq_iInf_biSup theorem

{f : Filter β} {p : β → Prop} {u : β → α} : blimsup u f p = ⨅ s ∈ f, ⨆ (b) (_ : p b ∧ b ∈ s), u b

Full source

theorem blimsup_eq_iInf_biSup {f : Filter β} {p : β → Prop} {u : β → α} :
    blimsup u f p = ⨅ s ∈ f, ⨆ (b) (_ : p b ∧ b ∈ s), u b := by
  simp only [f.basis_sets.blimsup_eq_iInf_iSup, iSup_and', id, and_comm]

Bounded Limit Superior as Infimum of Suprema over Filter Sets: $\text{blimsup}_f(u,p) = \inf_{s \in f} \sup_{\substack{b \in s \\ p(b)}} u(b)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, $p : \beta \to \text{Prop}$ a predicate, and $u : \beta \to \alpha$ a function. The bounded limit superior of $u$ with respect to $p$ along $f$ is equal to the infimum over all sets $s$ in $f$ of the supremum of $u(b)$ over all $b \in s$ that satisfy $p(b)$. In other words: \[ \text{blimsup}_f(u, p) = \bigsqcap_{s \in f} \bigsqcup_{\substack{b \in s \\ p(b)}} u(b). \]

Filter.blimsup_eq_iInf_biSup_of_nat theorem

{p : ℕ → Prop} {u : ℕ → α} : blimsup u atTop p = ⨅ i, ⨆ (j) (_ : p j ∧ i ≤ j), u j

Full source

theorem blimsup_eq_iInf_biSup_of_nat {p : ℕ → Prop} {u : ℕ → α} :
    blimsup u atTop p = ⨅ i, ⨆ (j) (_ : p j ∧ i ≤ j), u j := by
  simp only [atTop_basis.blimsup_eq_iInf_iSup, @and_comm (p _), iSup_and, mem_Ici, iInf_true]

Bounded Limit Superior of a Sequence as Infimum of Tail Suprema with Predicate: $\text{blimsup}_{\text{atTop}}(u, p) = \inf_{i} \sup_{\substack{j \geq i \\ p(j)}} u(j)$

Informal description

For a sequence $ u : \mathbb{N} \to \alpha $ in a conditionally complete lattice $ \alpha $ and a predicate $ p : \mathbb{N} \to \text{Prop} $, the bounded limit superior of $ u $ with respect to $ p $ along the cofinite filter `atTop` is equal to the infimum over all $ i \in \mathbb{N} $ of the supremum of $ u(j) $ over all $ j \geq i $ satisfying $ p(j) $. In other words: \[ \text{blimsup}_{\text{atTop}}(u, p) = \inf_{i \in \mathbb{N}} \sup_{\substack{j \geq i \\ p(j)}} u(j). \]

Filter.liminf_eq_iSup_iInf theorem

{f : Filter β} {u : β → α} : liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a

Full source

/-- In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s` -/
theorem liminf_eq_iSup_iInf {f : Filter β} {u : β → α} : liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a :=
  limsup_eq_iInf_iSup (α := αᵒᵈ)

Limit Inferior as Supremum of Infima over Filter Sets: $\liminf_{f} u = \sup_{s \in f} \inf_{a \in s} u(a)$

Informal description

Let $\alpha$ be a complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. The limit inferior of $u$ along $f$ is equal to the supremum over all sets $s$ in $f$ of the infimum of $u$ over $s$, i.e., \[ \liminf_{f} u = \bigsqcup_{s \in f} \bigsqcap_{a \in s} u(a). \]

Filter.liminf_eq_iSup_iInf_of_nat theorem

{u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i ≥ n, u i

Full source

theorem liminf_eq_iSup_iInf_of_nat {u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i ≥ n, u i :=
  @limsup_eq_iInf_iSup_of_nat αᵒᵈ _ u

Limit Inferior of a Sequence as Supremum of Tail Infima

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a conditionally complete lattice $\alpha$, the limit inferior of $u$ along the cofinite filter `atTop` is equal to the supremum over all $n \in \mathbb{N}$ of the infimum of $u(i)$ for $i \geq n$. In other words, \[ \liminf_{n \to \infty} u(n) = \sup_{n \in \mathbb{N}} \inf_{i \geq n} u(i). \]

Filter.liminf_eq_iSup_iInf_of_nat' theorem

{u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n)

Full source

theorem liminf_eq_iSup_iInf_of_nat' {u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n) :=
  @limsup_eq_iInf_iSup_of_nat' αᵒᵈ _ _

Limit Inferior of Shifted Sequence as Supremum of Infima

Informal description

For any sequence $u : \mathbb{N} \to \alpha$ in a conditionally complete lattice $\alpha$, the limit inferior of $u$ along the cofinite filter `atTop` is equal to the supremum over all $n \in \mathbb{N}$ of the infimum of $u(i + n)$ for $i \in \mathbb{N}$. In other words, \[ \liminf_{n \to \infty} u(n) = \sup_{n \in \mathbb{N}} \inf_{i \in \mathbb{N}} u(i + n). \]

Filter.HasBasis.liminf_eq_iSup_iInf theorem

 {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) :
  liminf u f = ⨆ (i) (_ : p i), ⨅ a ∈ s i, u a

Full source

theorem HasBasis.liminf_eq_iSup_iInf {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α}
    (h : f.HasBasis p s) : liminf u f = ⨆ (i) (_ : p i), ⨅ a ∈ s i, u a :=
  HasBasis.limsup_eq_iInf_iSup (α := αᵒᵈ) h

Limit Inferior as Supremum of Infima over Filter Basis

Informal description

Let $f$ be a filter on $\beta$ with a basis consisting of sets $s_i$ indexed by $\iota$ with a predicate $p : \iota \to \text{Prop}$, and let $u : \beta \to \alpha$ be a function into a conditionally complete lattice $\alpha$. Then the limit inferior of $u$ along $f$ is equal to the supremum over all indices $i$ satisfying $p_i$ of the infimum of $u$ over $s_i$, i.e., \[ \liminf_{f} u = \bigsqcup_{i, p_i} \bigsqcap_{a \in s_i} u(a). \]

Filter.bliminf_eq_iSup_biInf theorem

{f : Filter β} {p : β → Prop} {u : β → α} : bliminf u f p = ⨆ s ∈ f, ⨅ (b) (_ : p b ∧ b ∈ s), u b

Full source

theorem bliminf_eq_iSup_biInf {f : Filter β} {p : β → Prop} {u : β → α} :
    bliminf u f p = ⨆ s ∈ f, ⨅ (b) (_ : p b ∧ b ∈ s), u b :=
  @blimsup_eq_iInf_biSup αᵒᵈ β _ f p u

Bounded Limit Inferior as Supremum of Infima over Filter Sets: $\text{bliminf}_f(u,p) = \sup_{s \in f} \inf_{\substack{b \in s \\ p(b)}} u(b)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, $p : \beta \to \text{Prop}$ a predicate, and $u : \beta \to \alpha$ a function. The bounded limit inferior of $u$ with respect to $p$ along $f$ is equal to the supremum over all sets $s$ in $f$ of the infimum of $u(b)$ over all $b \in s$ that satisfy $p(b)$. In other words: \[ \text{bliminf}_f(u, p) = \bigsqcup_{s \in f} \bigsqcap_{\substack{b \in s \\ p(b)}} u(b). \]

Filter.bliminf_eq_iSup_biInf_of_nat theorem

{p : ℕ → Prop} {u : ℕ → α} : bliminf u atTop p = ⨆ i, ⨅ (j) (_ : p j ∧ i ≤ j), u j

Full source

theorem bliminf_eq_iSup_biInf_of_nat {p : ℕ → Prop} {u : ℕ → α} :
    bliminf u atTop p = ⨆ i, ⨅ (j) (_ : p j ∧ i ≤ j), u j :=
  @blimsup_eq_iInf_biSup_of_nat αᵒᵈ _ p u

Bounded Limit Inferior of a Sequence as Supremum of Tail Infima with Predicate: $\text{bliminf}_{\text{atTop}}(u, p) = \sup_{i} \inf_{\substack{j \geq i \\ p(j)}} u(j)$

Informal description

For a sequence $ u : \mathbb{N} \to \alpha $ in a conditionally complete lattice $ \alpha $ and a predicate $ p : \mathbb{N} \to \text{Prop} $, the bounded limit inferior of $ u $ with respect to $ p $ along the cofinite filter `atTop` is equal to the supremum over all $ i \in \mathbb{N} $ of the infimum of $ u(j) $ over all $ j \geq i $ satisfying $ p(j) $. In other words: \[ \text{bliminf}_{\text{atTop}}(u, p) = \sup_{i \in \mathbb{N}} \inf_{\substack{j \geq i \\ p(j)}} u(j). \]

Filter.limsup_eq_sInf_sSup theorem

 {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) : limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)

Full source

theorem limsup_eq_sInf_sSup {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) :
    limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets) := by
  apply le_antisymm
  · rw [limsup_eq]
    refine sInf_le_sInf fun x hx => ?_
    rcases (mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
    filter_upwards [I_mem_F] with i hi
    exact hI ▸ le_sSup (mem_image_of_mem _ hi)
  · refine le_sInf fun b hb => sInf_le_of_le (mem_image_of_mem _ hb) <| sSup_le ?_
    rintro _ ⟨_, h, rfl⟩
    exact h

Limit Superior as Infimum of Suprema over Filter Sets

Informal description

Let $ι$ and $R$ be types, $F$ a filter on $ι$, and $R$ a complete lattice. For any function $a : ι \to R$, the limit superior of $a$ along $F$ is equal to the infimum of the set of suprema of $a$ over all sets in $F$. In symbols: \[ \limsup_{F} a = \inf \{\sup a(I) \mid I \in F\}. \]

Filter.liminf_eq_sSup_sInf theorem

 {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) : liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets)

Full source

theorem liminf_eq_sSup_sInf {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) :
    liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets) :=
  @Filter.limsup_eq_sInf_sSup ι (OrderDual R) _ _ a

Limit Inferior as Supremum of Infima over Filter Sets

Informal description

Let $ι$ and $R$ be types, $F$ a filter on $ι$, and $R$ a complete lattice. For any function $a : ι \to R$, the limit inferior of $a$ along $F$ is equal to the supremum of the set of infima of $a$ over all sets in $F$. In symbols: \[ \liminf_{F} a = \sup \{\inf a(I) \mid I \in F\}. \]

Filter.liminf_le_of_frequently_le' theorem

{α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ a in f, u a ≤ x) : liminf u f ≤ x

Full source

theorem liminf_le_of_frequently_le' {α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β}
    (h : ∃ᶠ a in f, u a ≤ x) : liminf u f ≤ x := by
  rw [liminf_eq]
  refine sSup_le fun b hb => ?_
  have hbx : ∃ᶠ _ in f, b ≤ x := by
    revert h
    rw [← not_imp_not, not_frequently, not_frequently]
    exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
  exact hbx.exists.choose_spec

Limit Inferior Bounded by Frequently Occurring Upper Bounds

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ a complete lattice, $f$ a filter on $\alpha$, $u : \alpha \to \beta$ a function, and $x \in \beta$. If there exists a frequently occurring set of $a \in \alpha$ in the filter $f$ such that $u(a) \leq x$, then the limit inferior of $u$ along $f$ satisfies $\liminf_f u \leq x$.

Filter.le_limsup_of_frequently_le' theorem

{α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ a in f, x ≤ u a) : x ≤ limsup u f

Full source

theorem le_limsup_of_frequently_le' {α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β}
    (h : ∃ᶠ a in f, x ≤ u a) : x ≤ limsup u f :=
  liminf_le_of_frequently_le' (β := βᵒᵈ) h

Lower Bound of Frequently Occurring Values is Below Limit Superior

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ a complete lattice, $f$ a filter on $\alpha$, $u : \alpha \to \beta$ a function, and $x \in \beta$. If there exists a frequently occurring set of $a \in \alpha$ in the filter $f$ such that $x \leq u(a)$, then $x$ is less than or equal to the limit superior of $u$ along $f$, i.e., $x \leq \limsup_f u$.

CompleteLatticeHom.apply_limsup_iterate theorem

(f : CompleteLatticeHom α α) (a : α) : f (limsup (fun n => f^[n] a) atTop) = limsup (fun n => f^[n] a) atTop

Full source

/-- If `f : α → α` is a morphism of complete lattices, then the limsup of its iterates of any
`a : α` is a fixed point. -/
@[simp]
theorem _root_.CompleteLatticeHom.apply_limsup_iterate (f : CompleteLatticeHom α α) (a : α) :
    f (limsup (fun n => f^[n] a) atTop) = limsup (fun n => f^[n] a) atTop := by
  rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
  simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f,
    ← Nat.add_succ]
  conv_rhs => rw [iInf_split _ (0 < ·)]
  simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
  refine (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_
  simp only [zero_add, Function.comp_apply, iSup_le_iff]
  exact fun i => le_iSup (fun i => f^[i] a) (i + 1)

Fixed Point Property of Limsup for Complete Lattice Homomorphisms

Informal description

Let $\alpha$ be a complete lattice and $f : \alpha \to \alpha$ be a complete lattice homomorphism. For any element $a \in \alpha$, the limit superior of the sequence $(f^{[n]}(a))_{n \in \mathbb{N}}$ along the cofinite filter is a fixed point of $f$, i.e., \[ f\left(\limsup_{n \to \infty} f^{[n]}(a)\right) = \limsup_{n \to \infty} f^{[n]}(a), \] where $f^{[n]}$ denotes the $n$-th iterate of $f$.

CompleteLatticeHom.apply_liminf_iterate theorem

(f : CompleteLatticeHom α α) (a : α) : f (liminf (fun n => f^[n] a) atTop) = liminf (fun n => f^[n] a) atTop

Full source

/-- If `f : α → α` is a morphism of complete lattices, then the liminf of its iterates of any
`a : α` is a fixed point. -/
theorem _root_.CompleteLatticeHom.apply_liminf_iterate (f : CompleteLatticeHom α α) (a : α) :
    f (liminf (fun n => f^[n] a) atTop) = liminf (fun n => f^[n] a) atTop :=
  (CompleteLatticeHom.dual f).apply_limsup_iterate _

Fixed Point Property of Liminf for Complete Lattice Homomorphisms

Informal description

Let $\alpha$ be a complete lattice and $f \colon \alpha \to \alpha$ be a complete lattice homomorphism. For any element $a \in \alpha$, the limit inferior of the iterates $(f^{[n]}(a))_{n \in \mathbb{N}}$ along the cofinite filter is a fixed point of $f$, i.e., \[ f\left(\liminf_{n \to \infty} f^{[n]}(a)\right) = \liminf_{n \to \infty} f^{[n]}(a), \] where $f^{[n]}$ denotes the $n$-th iterate of $f$.

Filter.blimsup_mono theorem

(h : ∀ x, p x → q x) : blimsup u f p ≤ blimsup u f q

Full source

theorem blimsup_mono (h : ∀ x, p x → q x) : blimsup u f p ≤ blimsup u f q :=
  sInf_le_sInf fun a ha => ha.mono <| by tauto

Monotonicity of Bounded Limit Superior with Respect to Predicate Inclusion

Informal description

For any function $u : \beta \to \alpha$, filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, if $p(x)$ implies $q(x)$ for all $x \in \beta$, then the bounded limit superior satisfies $\text{blimsup}\ u\ f\ p \leq \text{blimsup}\ u\ f\ q$.

Filter.bliminf_antitone theorem

(h : ∀ x, p x → q x) : bliminf u f q ≤ bliminf u f p

Full source

theorem bliminf_antitone (h : ∀ x, p x → q x) : bliminf u f q ≤ bliminf u f p :=
  sSup_le_sSup fun a ha => ha.mono <| by tauto

Antitonicity of Bounded Limit Inferior with Respect to Predicate Inclusion

Informal description

For any function $u : \beta \to \alpha$ and filter $f$ on $\beta$, if predicates $p, q : \beta \to \text{Prop}$ satisfy $p(x) \to q(x)$ for all $x \in \beta$, then the bounded limit inferior satisfies $\text{bliminf}_f u q \leq \text{bliminf}_f u p$.

Filter.mono_blimsup' theorem

(h : ∀ᶠ x in f, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p

Full source

theorem mono_blimsup' (h : ∀ᶠ x in f, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p :=
  sInf_le_sInf fun _ ha => (ha.and h).mono fun _ hx hx' => (hx.2 hx').trans (hx.1 hx')

Monotonicity of Bounded Limit Superior under Eventual Pointwise Inequality

Informal description

Let $u, v : \beta \to \alpha$ be functions, $f$ a filter on $\beta$, and $p : \beta \to \text{Prop}$ a predicate. If for $f$-almost all $x$, $p x$ implies $u x \leq v x$, then the bounded limit superior of $u$ with respect to $p$ along $f$ is less than or equal to the bounded limit superior of $v$ with respect to $p$ along $f$. In symbols: \[ (\forall^f x, p x \to u x \leq v x) \implies \text{blimsup}_{f} u p \leq \text{blimsup}_{f} v p. \]

Filter.mono_blimsup theorem

(h : ∀ x, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p

Full source

theorem mono_blimsup (h : ∀ x, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p :=
  mono_blimsup' <| Eventually.of_forall h

Monotonicity of Bounded Limit Superior under Pointwise Inequality

Informal description

Let $f$ be a filter on a type $\beta$, and let $u, v : \beta \to \alpha$ be functions into a conditionally complete lattice $\alpha$. If for all $x$, the predicate $p(x)$ implies $u(x) \leq v(x)$, then the bounded limit superior satisfies $\text{blimsup}_{f} u p \leq \text{blimsup}_{f} v p$.

Filter.mono_bliminf' theorem

(h : ∀ᶠ x in f, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p

Full source

theorem mono_bliminf' (h : ∀ᶠ x in f, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p :=
  sSup_le_sSup fun _ ha => (ha.and h).mono fun _ hx hx' => (hx.1 hx').trans (hx.2 hx')

Monotonicity of Bounded Limit Inferior under Pointwise Inequality Almost Everywhere

Informal description

Let $f$ be a filter on a type $\beta$, and let $u, v : \beta \to \alpha$ be functions into a conditionally complete lattice $\alpha$. If for $f$-almost all $x$, the implication $p(x) \to u(x) \leq v(x)$ holds, then the bounded limit inferior of $u$ with respect to $f$ and $p$ is less than or equal to the bounded limit inferior of $v$ with respect to $f$ and $p$. In other words, if $u(x) \leq v(x)$ whenever $p(x)$ holds for all $x$ in a set that is eventually in $f$, then $\text{bliminf}_{x \to f, p(x)} u(x) \leq \text{bliminf}_{x \to f, p(x)} v(x)$.

Filter.mono_bliminf theorem

(h : ∀ x, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p

Full source

theorem mono_bliminf (h : ∀ x, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p :=
  mono_bliminf' <| Eventually.of_forall h

Monotonicity of Bounded Limit Inferior under Pointwise Inequality

Informal description

Let $f$ be a filter on a type $\beta$, and let $u, v : \beta \to \alpha$ be functions into a conditionally complete lattice $\alpha$. If for all $x$, the implication $p(x) \to u(x) \leq v(x)$ holds, then the bounded limit inferior of $u$ with respect to $f$ and $p$ is less than or equal to the bounded limit inferior of $v$ with respect to $f$ and $p$. In other words, if $u(x) \leq v(x)$ whenever $p(x)$ holds for all $x$, then $\text{bliminf}_{x \to f, p(x)} u(x) \leq \text{bliminf}_{x \to f, p(x)} v(x)$.

Filter.bliminf_antitone_filter theorem

(h : f ≤ g) : bliminf u g p ≤ bliminf u f p

Full source

theorem bliminf_antitone_filter (h : f ≤ g) : bliminf u g p ≤ bliminf u f p :=
  sSup_le_sSup fun _ ha => ha.filter_mono h

Antitone Property of Bounded Limit Inferior with Respect to Filter Ordering

Informal description

Let $f$ and $g$ be filters on a type $\beta$ such that $f \leq g$, and let $u : \beta \to \alpha$ be a function taking values in a conditionally complete lattice $\alpha$. For any predicate $p : \beta \to \text{Prop}$, the bounded limit inferior satisfies the antitone property with respect to the filter ordering, i.e., \[ \text{bliminf}_g\, u\, p \leq \text{bliminf}_f\, u\, p. \]

Filter.blimsup_monotone_filter theorem

(h : f ≤ g) : blimsup u f p ≤ blimsup u g p

Full source

theorem blimsup_monotone_filter (h : f ≤ g) : blimsup u f p ≤ blimsup u g p :=
  sInf_le_sInf fun _ ha => ha.filter_mono h

Monotonicity of Bounded Limit Superior with Respect to Filter Inclusion

Informal description

Let $f$ and $g$ be filters on a type $\beta$ such that $f \leq g$. For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any predicate $p : \beta \to \text{Prop}$, the bounded limit superior satisfies $\text{blimsup}_p u f \leq \text{blimsup}_p u g$.

Filter.blimsup_and_le_inf theorem

: (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f p ⊓ blimsup u f q

Full source

theorem blimsup_and_le_inf : (blimsup u f fun x => p x ∧ q x) ≤ blimsupblimsup u f p ⊓ blimsup u f q :=
  le_inf (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

Bounded Limit Superior of Conjunction is Bounded by Infimum of Individual Bounds

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit superior of $u$ with respect to the conjunction $p \land q$ satisfies \[ \text{blimsup}_f\, u\, (p \land q) \leq \text{blimsup}_f\, u\, p \sqcap \text{blimsup}_f\, u\, q. \]

Filter.bliminf_sup_le_inf_aux_left theorem

: (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f p

Full source

@[simp]
theorem bliminf_sup_le_inf_aux_left :
    (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f p :=
  blimsup_and_le_inf.trans inf_le_left

Bounded Limit Superior of Conjunction is Bounded by First Predicate's Limit Superior

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit superior of $u$ with respect to the conjunction $p \land q$ satisfies \[ \text{blimsup}_f\, u\, (p \land q) \leq \text{blimsup}_f\, u\, p. \]

Filter.bliminf_sup_le_inf_aux_right theorem

: (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f q

Full source

@[simp]
theorem bliminf_sup_le_inf_aux_right :
    (blimsup u f fun x => p x ∧ q x) ≤ blimsup u f q :=
  blimsup_and_le_inf.trans inf_le_right

Right Inequality for Bounded Limit Superior of Conjunction

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit superior of $u$ with respect to the conjunction $p \land q$ satisfies \[ \text{blimsup}_f\, u\, (p \land q) \leq \text{blimsup}_f\, u\, q. \]

Filter.bliminf_sup_le_and theorem

: bliminf u f p ⊔ bliminf u f q ≤ bliminf u f fun x => p x ∧ q x

Full source

theorem bliminf_sup_le_and : bliminfbliminf u f p ⊔ bliminf u f q ≤ bliminf u f fun x => p x ∧ q x :=
  blimsup_and_le_inf (α := αᵒᵈ)

Supremum of Bounded Limit Inferiors is Bounded by Bounded Limit Inferior of Conjunction

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the supremum of the bounded limit inferiors of $u$ with respect to $p$ and $q$ is bounded above by the bounded limit inferior of $u$ with respect to the conjunction $p \land q$. In other words: \[ \text{bliminf}_f\, u\, p \sqcup \text{bliminf}_f\, u\, q \leq \text{bliminf}_f\, u\, (p \land q). \]

Filter.bliminf_sup_le_and_aux_left theorem

: bliminf u f p ≤ bliminf u f fun x => p x ∧ q x

Full source

@[simp]
theorem bliminf_sup_le_and_aux_left : bliminf u f p ≤ bliminf u f fun x => p x ∧ q x :=
  le_sup_left.trans bliminf_sup_le_and

Left Inequality for Bounded Limit Inferior of Conjunction

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior of $u$ with respect to $p$ is bounded above by the bounded limit inferior of $u$ with respect to the conjunction $p \land q$. In other words: \[ \text{bliminf}_f\, u\, p \leq \text{bliminf}_f\, u\, (p \land q). \]

Filter.bliminf_sup_le_and_aux_right theorem

: bliminf u f q ≤ bliminf u f fun x => p x ∧ q x

Full source

@[simp]
theorem bliminf_sup_le_and_aux_right : bliminf u f q ≤ bliminf u f fun x => p x ∧ q x :=
  le_sup_right.trans bliminf_sup_le_and

Right Inequality for Bounded Limit Inferior of Conjunction

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior of $u$ with respect to $q$ is bounded above by the bounded limit inferior of $u$ with respect to the conjunction $p \land q$. In other words: \[ \text{bliminf}_f\, u\, q \leq \text{bliminf}_f\, u\, (p \land q). \]

Filter.blimsup_sup_le_or theorem

: blimsup u f p ⊔ blimsup u f q ≤ blimsup u f fun x => p x ∨ q x

Full source

/-- See also `Filter.blimsup_or_eq_sup`. -/
theorem blimsup_sup_le_or : blimsupblimsup u f p ⊔ blimsup u f q ≤ blimsup u f fun x => p x ∨ q x :=
  sup_le (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

Supremum of Bounded Limit Superiors is Bounded by Limit Superior of Disjunction

Informal description

For any function $u : \beta \to \alpha$, filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, the supremum of the bounded limit superiors satisfies \[ \text{blimsup}\ u\ f\ p \sqcup \text{blimsup}\ u\ f\ q \leq \text{blimsup}\ u\ f\ (\lambda x, p x \lor q x). \]

Filter.bliminf_sup_le_or_aux_left theorem

: blimsup u f p ≤ blimsup u f fun x => p x ∨ q x

Full source

@[simp]
theorem bliminf_sup_le_or_aux_left : blimsup u f p ≤ blimsup u f fun x => p x ∨ q x :=
  le_sup_left.trans blimsup_sup_le_or

Bounded Limit Superior with Predicate is Bounded by Disjunctive Predicate

Informal description

For any function $ u : \beta \to \alpha $, filter $ f $ on $ \beta $, and predicates $ p, q : \beta \to \text{Prop} $, the bounded limit superior with respect to $ p $ is less than or equal to the bounded limit superior with respect to the disjunction $ p \lor q $. That is, \[ \text{blimsup}\ u\ f\ p \leq \text{blimsup}\ u\ f\ (\lambda x, p x \lor q x). \]

Filter.bliminf_sup_le_or_aux_right theorem

: blimsup u f q ≤ blimsup u f fun x => p x ∨ q x

Full source

@[simp]
theorem bliminf_sup_le_or_aux_right : blimsup u f q ≤ blimsup u f fun x => p x ∨ q x :=
  le_sup_right.trans blimsup_sup_le_or

Bounded Limit Superior with Respect to One Predicate is Bounded by Limit Superior of Disjunction

Informal description

For any function $u : \beta \to \alpha$, filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, the bounded limit superior with respect to $q$ satisfies \[ \text{blimsup}\ u\ f\ q \leq \text{blimsup}\ u\ f\ (\lambda x, p x \lor q x). \]

Filter.bliminf_or_le_inf theorem

: (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q

Full source

/-- See also `Filter.bliminf_or_eq_inf`. -/
theorem bliminf_or_le_inf : (bliminf u f fun x => p x ∨ q x) ≤ bliminfbliminf u f p ⊓ bliminf u f q :=
  blimsup_sup_le_or (α := αᵒᵈ)

Bounded Limit Inferior of Disjunction is Bounded by Infimum of Bounded Limit Inferiors

Informal description

For any function $u : \beta \to \alpha$, filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior with respect to the disjunction $p \lor q$ satisfies \[ \text{bliminf}\ u\ f\ (\lambda x, p x \lor q x) \leq \text{bliminf}\ u\ f\ p \sqcap \text{bliminf}\ u\ f\ q. \]

Filter.bliminf_or_le_inf_aux_left theorem

: (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f p

Full source

@[simp]
theorem bliminf_or_le_inf_aux_left : (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f p :=
  bliminf_or_le_inf.trans inf_le_left

Bounded Limit Inferior of Disjunction is Bounded by Left Predicate's Limit Inferior

Informal description

For any function $u : \beta \to \alpha$ from a type $\beta$ to a conditionally complete lattice $\alpha$, any filter $f$ on $\beta$, and any predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior of $u$ with respect to the disjunction $p \lor q$ is bounded above by the bounded limit inferior of $u$ with respect to $p$ alone. In other words, \[ \text{bliminf}_{f} u (p \lor q) \leq \text{bliminf}_{f} u p. \]

Filter.bliminf_or_le_inf_aux_right theorem

: (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f q

Full source

@[simp]
theorem bliminf_or_le_inf_aux_right : (bliminf u f fun x => p x ∨ q x) ≤ bliminf u f q :=
  bliminf_or_le_inf.trans inf_le_right

Bounded Limit Inferior of Disjunction is Bounded by Right Bounded Limit Inferior

Informal description

For any function $u : \beta \to \alpha$, filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior with respect to the disjunction $p \lor q$ satisfies \[ \text{bliminf}\ u\ f\ (\lambda x, p x \lor q x) \leq \text{bliminf}\ u\ f\ q. \]

OrderIso.apply_blimsup theorem

[CompleteLattice γ] (e : α ≃o γ) : e (blimsup u f p) = blimsup (e ∘ u) f p

Full source

theorem _root_.OrderIso.apply_blimsup [CompleteLattice γ] (e : α ≃o γ) :
    e (blimsup u f p) = blimsup (e ∘ u) f p := by
  simp only [blimsup_eq, map_sInf, Function.comp_apply, e.image_eq_preimage,
    Set.preimage_setOf_eq, e.le_symm_apply]

Order Isomorphism Preserves Bounded Limit Superior: $e(\text{blimsup}\ u\ f\ p) = \text{blimsup}\ (e \circ u)\ f\ p$

Informal description

Let $\alpha$ and $\gamma$ be complete lattices, and let $e : \alpha \simeq_o \gamma$ be an order isomorphism between them. For any function $u : \beta \to \alpha$, any filter $f$ on $\beta$, and any predicate $p : \beta \to \text{Prop}$, the image of the bounded limit superior $\text{blimsup}\ u\ f\ p$ under $e$ is equal to the bounded limit superior of the composition $e \circ u$ with respect to $f$ and $p$, i.e., \[ e(\text{blimsup}\ u\ f\ p) = \text{blimsup}\ (e \circ u)\ f\ p. \]

OrderIso.apply_bliminf theorem

[CompleteLattice γ] (e : α ≃o γ) : e (bliminf u f p) = bliminf (e ∘ u) f p

Full source

theorem _root_.OrderIso.apply_bliminf [CompleteLattice γ] (e : α ≃o γ) :
    e (bliminf u f p) = bliminf (e ∘ u) f p :=
  e.dual.apply_blimsup

Order Isomorphism Preserves Bounded Limit Inferior: $e(\text{bliminf}\ u\ f\ p) = \text{bliminf}\ (e \circ u)\ f\ p$

Informal description

Let $\alpha$ and $\gamma$ be complete lattices, and let $e : \alpha \simeq_o \gamma$ be an order isomorphism between them. For any function $u : \beta \to \alpha$, any filter $f$ on $\beta$, and any predicate $p : \beta \to \text{Prop}$, the image of the bounded limit inferior $\text{bliminf}\ u\ f\ p$ under $e$ is equal to the bounded limit inferior of the composition $e \circ u$ with respect to $f$ and $p$, i.e., \[ e(\text{bliminf}\ u\ f\ p) = \text{bliminf}\ (e \circ u)\ f\ p. \]

sSupHom.apply_blimsup_le theorem

[CompleteLattice γ] (g : sSupHom α γ) : g (blimsup u f p) ≤ blimsup (g ∘ u) f p

Full source

theorem _root_.sSupHom.apply_blimsup_le [CompleteLattice γ] (g : sSupHom α γ) :
    g (blimsup u f p) ≤ blimsup (g ∘ u) f p := by
  simp only [blimsup_eq_iInf_biSup, Function.comp]
  refine ((OrderHomClass.mono g).map_iInf₂_le _).trans ?_
  simp only [_root_.map_iSup, le_refl]

Supremum-Preserving Functions are Non-Increasing on Bounded Limit Superiors: $g(\text{blimsup}_f(u,p)) \leq \text{blimsup}_f(g \circ u, p)$

Informal description

Let $\alpha$ and $\gamma$ be complete lattices, and let $g : \alpha \to \gamma$ be a supremum-preserving function. For any function $u : \beta \to \alpha$, any filter $f$ on $\beta$, and any predicate $p : \beta \to \text{Prop}$, the image of the bounded limit superior $\text{blimsup}_f(u, p)$ under $g$ is less than or equal to the bounded limit superior of the composition $g \circ u$ with respect to $f$ and $p$, i.e., \[ g(\text{blimsup}_f(u, p)) \leq \text{blimsup}_f(g \circ u, p). \]

sInfHom.le_apply_bliminf theorem

[CompleteLattice γ] (g : sInfHom α γ) : bliminf (g ∘ u) f p ≤ g (bliminf u f p)

Full source

theorem _root_.sInfHom.le_apply_bliminf [CompleteLattice γ] (g : sInfHom α γ) :
    bliminf (g ∘ u) f p ≤ g (bliminf u f p) :=
  (sInfHom.dual g).apply_blimsup_le

Infimum-Preserving Functions are Non-Decreasing on Bounded Limit Inferiors: $\text{bliminf}_f(g \circ u, p) \leq g(\text{bliminf}_f(u, p))$

Informal description

Let $\alpha$ and $\gamma$ be complete lattices, and let $g : \alpha \to \gamma$ be an infimum-preserving function. For any function $u : \beta \to \alpha$, any filter $f$ on $\beta$, and any predicate $p : \beta \to \text{Prop}$, the bounded limit inferior of the composition $g \circ u$ with respect to $f$ and $p$ is less than or equal to the image of the bounded limit inferior of $u$ under $g$, i.e., \[ \text{bliminf}_f (g \circ u, p) \leq g(\text{bliminf}_f(u, p)). \]

Filter.limsup_sup_filter theorem

{g} : limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Full source

lemma limsup_sup_filter {g} : limsup u (f ⊔ g) = limsuplimsup u f ⊔ limsup u g := by
  refine le_antisymm ?_
    (sup_le (limsup_le_limsup_of_le le_sup_left) (limsup_le_limsup_of_le le_sup_right))
  simp_rw [limsup_eq, sInf_sup_eq, sup_sInf_eq, mem_setOf_eq, le_iInf₂_iff]
  intro a ha b hb
  exact sInf_le ⟨ha.mono fun _ h ↦ h.trans le_sup_left, hb.mono fun _ h ↦ h.trans le_sup_right⟩

Limit Superior Distributes Over Supremum of Filters

Informal description

For any function $u : \beta \to \alpha$ mapping into a conditionally complete lattice $\alpha$, and any filters $f$ and $g$ on $\beta$, the limit superior of $u$ with respect to the filter $f \sqcup g$ is equal to the supremum of the limit superiors of $u$ with respect to $f$ and $g$ separately. In other words: \[ \limsup_{f \sqcup g} u = \limsup_f u \sqcup \limsup_g u \]

Filter.liminf_sup_filter theorem

{g} : liminf u (f ⊔ g) = liminf u f ⊓ liminf u g

Full source

lemma liminf_sup_filter {g} : liminf u (f ⊔ g) = liminfliminf u f ⊓ liminf u g :=
  limsup_sup_filter (α := αᵒᵈ)

Limit Inferior Distributes Over Infimum of Filters

Informal description

For any function $u : \beta \to \alpha$ mapping into a conditionally complete lattice $\alpha$, and any filters $f$ and $g$ on $\beta$, the limit inferior of $u$ with respect to the filter $f \sqcup g$ is equal to the infimum of the limit inferiors of $u$ with respect to $f$ and $g$ separately. In other words: \[ \liminf_{f \sqcup g} u = \liminf_f u \sqcap \liminf_g u \]

Filter.blimsup_or_eq_sup theorem

: (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

Full source

@[simp]
theorem blimsup_or_eq_sup : (blimsup u f fun x => p x ∨ q x) = blimsupblimsup u f p ⊔ blimsup u f q := by
  simp only [blimsup_eq_limsup, ← limsup_sup_filter, ← inf_sup_left, sup_principal, setOf_or]

Bounded Limit Superior of Disjunction Equals Supremum of Bounded Limit Superiors

Informal description

Let $f$ be a filter on a type $\beta$, $u : \beta \to \alpha$ a function into a conditionally complete lattice $\alpha$, and $p, q : \beta \to \text{Prop}$ predicates. Then the bounded limit superior of $u$ with respect to the predicate $p \lor q$ (i.e., $p(x) \lor q(x)$ for all $x$) along $f$ is equal to the supremum of the bounded limit superiors of $u$ with respect to $p$ and $q$ separately along $f$. In other words: \[ \text{blimsup}_f u (p \lor q) = \text{blimsup}_f u p \sqcup \text{blimsup}_f u q \]

Filter.bliminf_or_eq_inf theorem

: (bliminf u f fun x => p x ∨ q x) = bliminf u f p ⊓ bliminf u f q

Full source

@[simp]
theorem bliminf_or_eq_inf : (bliminf u f fun x => p x ∨ q x) = bliminfbliminf u f p ⊓ bliminf u f q :=
  blimsup_or_eq_sup (α := αᵒᵈ)

Bounded Limit Inferior of Disjunction Equals Infimum of Bounded Limit Inferiors

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, any filter $f$ on $\beta$, and predicates $p, q : \beta \to \text{Prop}$, the bounded limit inferior of $u$ with respect to the disjunction $p \lor q$ along $f$ equals the infimum of the bounded limit inferiors of $u$ with respect to $p$ and $q$ separately along $f$. In symbols: \[ \text{bliminf}_f u (p \lor q) = \text{bliminf}_f u p \sqcap \text{bliminf}_f u q \]

Filter.blimsup_sup_not theorem

: blimsup u f p ⊔ blimsup u f (¬p ·) = limsup u f

Full source

@[simp]
lemma blimsup_sup_not : blimsupblimsup u f p ⊔ blimsup u f (¬p ·) = limsup u f := by
  simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]

Supremum of Bounded Limit Superiors with Predicate and its Negation Equals Limit Superior

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any filter $f$ on $\beta$, the supremum of the bounded limit superior of $u$ with respect to a predicate $p$ and the bounded limit superior of $u$ with respect to the negation of $p$ equals the limit superior of $u$ along $f$. In symbols: \[ \text{blimsup}_{x \to f} \, u(x) \, p \sqcup \text{blimsup}_{x \to f} \, u(x) \, (\neg p) = \text{limsup}_{x \to f} \, u(x) \]

Filter.bliminf_inf_not theorem

: bliminf u f p ⊓ bliminf u f (¬p ·) = liminf u f

Full source

@[simp]
lemma bliminf_inf_not : bliminfbliminf u f p ⊓ bliminf u f (¬p ·) = liminf u f :=
  blimsup_sup_not (α := αᵒᵈ)

Infimum of Bounded Limit Inferiors with Predicate and its Negation Equals Limit Inferior

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any filter $f$ on $\beta$, the infimum of the bounded limit inferior of $u$ with respect to a predicate $p$ and the bounded limit inferior of $u$ with respect to the negation of $p$ equals the limit inferior of $u$ along $f$. In symbols: \[ \text{bliminf}_{x \to f} \, u(x) \, p \sqcap \text{bliminf}_{x \to f} \, u(x) \, (\neg p) = \text{liminf}_{x \to f} \, u(x) \]

Filter.blimsup_not_sup theorem

: blimsup u f (¬p ·) ⊔ blimsup u f p = limsup u f

Full source

@[simp]
lemma blimsup_not_sup : blimsupblimsup u f (¬p ·) ⊔ blimsup u f p = limsup u f := by
  simpa only [not_not] using blimsup_sup_not (p := (¬p ·))

Supremum of Bounded Limit Superiors with Negated Predicate and Original Predicate Equals Limit Superior

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any filter $f$ on $\beta$, the supremum of the bounded limit superior of $u$ with respect to the negation of a predicate $p$ and the bounded limit superior of $u$ with respect to $p$ equals the limit superior of $u$ along $f$. In symbols: \[ \text{blimsup}_{x \to f} \, u(x) \, (\neg p) \sqcup \text{blimsup}_{x \to f} \, u(x) \, p = \text{limsup}_{x \to f} \, u(x) \]

Filter.bliminf_not_inf theorem

: bliminf u f (¬p ·) ⊓ bliminf u f p = liminf u f

Full source

@[simp]
lemma bliminf_not_inf : bliminfbliminf u f (¬p ·) ⊓ bliminf u f p = liminf u f :=
  blimsup_not_sup (α := αᵒᵈ)

Infimum of Bounded Limit Inferiors with Negated Predicate and Original Predicate Equals Limit Inferior

Informal description

For any function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice, and any filter $f$ on $\beta$, the infimum of the bounded limit inferior of $u$ with respect to the negation of a predicate $p$ and the bounded limit inferior of $u$ with respect to $p$ equals the limit inferior of $u$ along $f$. In symbols: \[ \text{bliminf}_{x \to f} \, u(x) \, (\neg p) \sqcap \text{bliminf}_{x \to f} \, u(x) \, p = \text{liminf}_{x \to f} \, u(x) \]

Filter.limsup_piecewise theorem

 {s : Set β} [DecidablePred (· ∈ s)] {v} : limsup (s.piecewise u v) f = blimsup u f (· ∈ s) ⊔ blimsup v f (· ∉ s)

Full source

lemma limsup_piecewise {s : Set β} [DecidablePred (· ∈ s)] {v} :
    limsup (s.piecewise u v) f = blimsupblimsup u f (· ∈ s) ⊔ blimsup v f (· ∉ s) := by
  rw [← blimsup_sup_not (p := (· ∈ s))]
  refine congr_arg₂ _ (blimsup_congr ?_) (blimsup_congr ?_) <;>
    filter_upwards with _ h using by simp [h]

Limit Superior of Piecewise Function: $\limsup_f (s.\text{piecewise}\ u\ v) = \text{blimsup}_f u (\cdot \in s) \sqcup \text{blimsup}_f v (\cdot \notin s)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $f$ a filter on $\beta$, and $s \subseteq \beta$ a set with decidable membership. For functions $u, v : \beta \to \alpha$, the limit superior of the piecewise function $s.\text{piecewise}\ u\ v$ along $f$ equals the supremum of the bounded limit superior of $u$ with respect to membership in $s$ and the bounded limit superior of $v$ with respect to non-membership in $s$. In symbols: \[ \limsup_{f} (s.\text{piecewise}\ u\ v) = \text{blimsup}_{f} u (\cdot \in s) \sqcup \text{blimsup}_{f} v (\cdot \notin s) \]

Filter.liminf_piecewise theorem

 {s : Set β} [DecidablePred (· ∈ s)] {v} : liminf (s.piecewise u v) f = bliminf u f (· ∈ s) ⊓ bliminf v f (· ∉ s)

Full source

lemma liminf_piecewise {s : Set β} [DecidablePred (· ∈ s)] {v} :
    liminf (s.piecewise u v) f = bliminfbliminf u f (· ∈ s) ⊓ bliminf v f (· ∉ s) :=
  limsup_piecewise (α := αᵒᵈ)

Limit Inferior of Piecewise Function: $\liminf_f (s.\text{piecewise}\ u\ v) = \text{bliminf}_f u (\cdot \in s) \sqcap \text{bliminf}_f v (\cdot \notin s)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a type, $f$ a filter on $\beta$, and $s \subseteq \beta$ a set with decidable membership. For functions $u, v : \beta \to \alpha$, the limit inferior of the piecewise function \[ (s.\text{piecewise}\ u\ v)(x) = \begin{cases} u(x) & \text{if } x \in s, \\ v(x) & \text{otherwise}, \end{cases} \] along $f$ equals the infimum of the bounded limit inferior of $u$ with respect to membership in $s$ and the bounded limit inferior of $v$ with respect to non-membership in $s$. In symbols: \[ \liminf_{f} (s.\text{piecewise}\ u\ v) = \text{bliminf}_{f} u (\cdot \in s) \sqcap \text{bliminf}_{f} v (\cdot \notin s). \]

Filter.sup_limsup theorem

[NeBot f] (a : α) : a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f

Full source

theorem sup_limsup [NeBot f] (a : α) : a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f := by
  simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
  congr; ext s; congr; ext hs; congr
  exact (biSup_const (nonempty_of_mem hs)).symm

Supremum with Limit Superior: $a \sqcup \limsup_{f} u = \limsup_{f} (a \sqcup u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a non-trivial filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the supremum of $a$ with the limit superior of $u$ along $f$ equals the limit superior of the function $x \mapsto a \sqcup u(x)$ along $f$, i.e., \[ a \sqcup \limsup_{f} u = \limsup_{f} (x \mapsto a \sqcup u(x)). \]

Filter.inf_liminf theorem

[NeBot f] (a : α) : a ⊓ liminf u f = liminf (fun x => a ⊓ u x) f

Full source

theorem inf_liminf [NeBot f] (a : α) : a ⊓ liminf u f = liminf (fun x => a ⊓ u x) f :=
  sup_limsup (α := αᵒᵈ) a

Infimum with Limit Inferior: $a \sqcap \liminf_{f} u = \liminf_{f} (a \sqcap u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a non-trivial filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the infimum of $a$ with the limit inferior of $u$ along $f$ equals the limit inferior of the function $x \mapsto a \sqcap u(x)$ along $f$, i.e., \[ a \sqcap \liminf_{f} u = \liminf_{f} (x \mapsto a \sqcap u(x)). \]

Filter.sup_liminf theorem

(a : α) : a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f

Full source

theorem sup_liminf (a : α) : a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f := by
  simp only [liminf_eq_iSup_iInf]
  rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

Supremum with Limit Inferior: $a \sqcup \liminf_{f} u = \liminf_{f} (a \sqcup u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the supremum of $a$ with the limit inferior of $u$ along $f$ equals the limit inferior of the function $x \mapsto a \sqcup u(x)$ along $f$, i.e., \[ a \sqcup \liminf_{f} u = \liminf_{f} (x \mapsto a \sqcup u(x)). \]

Filter.inf_limsup theorem

(a : α) : a ⊓ limsup u f = limsup (fun x => a ⊓ u x) f

Full source

theorem inf_limsup (a : α) : a ⊓ limsup u f = limsup (fun x => a ⊓ u x) f :=
  sup_liminf (α := αᵒᵈ) a

Infimum with Limit Superior: $a \sqcap \limsup_{f} u = \limsup_{f} (a \sqcap u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the infimum of $a$ with the limit superior of $u$ along $f$ equals the limit superior of the function $x \mapsto a \sqcap u(x)$ along $f$, i.e., \[ a \sqcap \limsup_{f} u = \limsup_{f} (x \mapsto a \sqcap u(x)). \]

Filter.limsup_compl theorem

: (limsup u f)ᶜ = liminf (compl ∘ u) f

Full source

theorem limsup_compl : (limsup u f)ᶜ = liminf (complcompl ∘ u) f := by
  simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Complement of Limit Superior Equals Limit Inferior of Complements: $(\limsup_f u)^\complement = \liminf_f (u^\complement)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. The complement of the limit superior of $u$ along $f$ is equal to the limit inferior of the complement of $u$ along $f$, i.e., \[ (\limsup_{f} u)^\complement = \liminf_{f} (x \mapsto u(x)^\complement). \]

Filter.liminf_compl theorem

: (liminf u f)ᶜ = limsup (compl ∘ u) f

Full source

theorem liminf_compl : (liminf u f)ᶜ = limsup (complcompl ∘ u) f := by
  simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Complement of Limit Inferior Equals Limit Superior of Complement: $(\liminf_f u)^\complement = \limsup_f (u^\complement)$

Informal description

For a function $u : \beta \to \alpha$ and a filter $f$ on $\beta$, where $\alpha$ is a conditionally complete lattice, the complement of the limit inferior of $u$ along $f$ is equal to the limit superior of the complement of $u$ along $f$, i.e., \[ (\liminf_{f} u)^\complement = \limsup_{f} (u^\complement). \]

Filter.limsup_sdiff theorem

(a : α) : limsup u f \ a = limsup (fun b => u b \ a) f

Full source

theorem limsup_sdiff (a : α) : limsuplimsup u f \ a = limsup (fun b => u b \ a) f := by
  simp only [limsup_eq_iInf_iSup, sdiff_eq]
  rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
  simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]

Limit Superior and Set Difference: $\limsup_f u \setminus a = \limsup_f (u \setminus a)$

Informal description

For any element $a$ in a conditionally complete lattice $\alpha$ and a function $u : \beta \to \alpha$ along a filter $f$ on $\beta$, the set difference between the limit superior of $u$ along $f$ and $a$ is equal to the limit superior of the function $\lambda b, u(b) \setminus a$ along $f$, i.e., \[ \limsup_f u \setminus a = \limsup_f (\lambda b, u(b) \setminus a). \]

Filter.liminf_sdiff theorem

[NeBot f] (a : α) : liminf u f \ a = liminf (fun b => u b \ a) f

Full source

theorem liminf_sdiff [NeBot f] (a : α) : liminfliminf u f \ a = liminf (fun b => u b \ a) f := by
  simp only [sdiff_eq, inf_comm _ aᶜ, inf_liminf]

Limit Inferior and Set Difference: $\liminf_f u \setminus a = \liminf_f (u \setminus a)$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a non-trivial filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the set difference between the limit inferior of $u$ along $f$ and $a$ is equal to the limit inferior of the function $x \mapsto u(x) \setminus a$ along $f$, i.e., \[ \liminf_{f} u \setminus a = \liminf_{f} (x \mapsto u(x) \setminus a). \]

Filter.sdiff_limsup theorem

[NeBot f] (a : α) : a \ limsup u f = liminf (fun b => a \ u b) f

Full source

theorem sdiff_limsup [NeBot f] (a : α) : a \ limsup u f = liminf (fun b => a \ u b) f := by
  rw [← compl_inj_iff]
  simp only [sdiff_eq, liminf_compl, comp_def, compl_inf, compl_compl, sup_limsup]

Set Difference with Limit Superior Equals Limit Inferior of Set Differences: $a \setminus \limsup_f u = \liminf_f (a \setminus u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a non-trivial filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the set difference between $a$ and the limit superior of $u$ along $f$ equals the limit inferior of the function $x \mapsto a \setminus u(x)$ along $f$, i.e., \[ a \setminus \limsup_{f} u = \liminf_{f} (x \mapsto a \setminus u(x)). \]

Filter.sdiff_liminf theorem

(a : α) : a \ liminf u f = limsup (fun b => a \ u b) f

Full source

theorem sdiff_liminf (a : α) : a \ liminf u f = limsup (fun b => a \ u b) f := by
  rw [← compl_inj_iff]
  simp only [sdiff_eq, limsup_compl, comp_def, compl_inf, compl_compl, sup_liminf]

Set Difference with Limit Inferior Equals Limit Superior of Differences: $a \setminus \liminf_f u = \limsup_f (a \setminus u(\cdot))$

Informal description

Let $\alpha$ be a conditionally complete lattice, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. For any element $a \in \alpha$, the set difference between $a$ and the limit inferior of $u$ along $f$ is equal to the limit superior of the function $x \mapsto a \setminus u(x)$ along $f$, i.e., \[ a \setminus \liminf_{f} u = \limsup_{f} (x \mapsto a \setminus u(x)). \]

Filter.mem_liminf_iff_eventually_mem theorem

: (a ∈ liminf s 𝓕) ↔ (∀ᶠ i in 𝓕, a ∈ s i)

Full source

lemma mem_liminf_iff_eventually_mem : (a ∈ liminf s 𝓕) ↔ (∀ᶠ i in 𝓕, a ∈ s i) := by
  simpa only [liminf_eq_iSup_iInf, iSup_eq_iUnion, iInf_eq_iInter, mem_iUnion, mem_iInter]
    using ⟨fun ⟨S, hS, hS'⟩ ↦ mem_of_superset hS (by tauto), fun h ↦ ⟨{i | a ∈ s i}, h, by tauto⟩⟩

Characterization of Limit Inferior Membership via Eventual Membership: $a \in \liminf_{\mathcal{F}} s \iff \forall^\mathcal{F} i, a \in s_i$

Informal description

For an element $a$ in a complete lattice $\alpha$, a filter $\mathcal{F}$ on an index set, and a family of sets $s_i \subseteq \alpha$ indexed by $\mathcal{F}$, we have that $a$ belongs to the limit inferior $\liminf_{\mathcal{F}} s$ if and only if $a \in s_i$ holds eventually for $i$ in $\mathcal{F}$. In other words: \[ a \in \liminf_{\mathcal{F}} s \iff \exists F \in \mathcal{F}, \forall i \in F, a \in s_i. \]

Filter.mem_limsup_iff_frequently_mem theorem

: (a ∈ limsup s 𝓕) ↔ (∃ᶠ i in 𝓕, a ∈ s i)

Full source

lemma mem_limsup_iff_frequently_mem : (a ∈ limsup s 𝓕) ↔ (∃ᶠ i in 𝓕, a ∈ s i) := by
  simp only [Filter.Frequently, iff_not_comm, ← mem_compl_iff, limsup_compl, comp_apply,
    mem_liminf_iff_eventually_mem]

Characterization of Limit Superior Membership via Frequent Membership: $a \in \limsup_{\mathcal{F}} s \iff \exists^\mathcal{F} i, a \in s_i$

Informal description

For an element $a$ in a complete lattice $\alpha$, a filter $\mathcal{F}$ on an index set, and a family of sets $s_i \subseteq \alpha$ indexed by $\mathcal{F}$, we have that $a$ belongs to the limit superior $\limsup_{\mathcal{F}} s$ if and only if $a \in s_i$ holds frequently for $i$ in $\mathcal{F}$. In other words: \[ a \in \limsup_{\mathcal{F}} s \iff \forall F \in \mathcal{F}, \exists i \in F, a \in s_i. \]

Filter.cofinite.blimsup_set_eq theorem

: blimsup s cofinite p = {x | {n | p n ∧ x ∈ s n}.Infinite}

Full source

theorem cofinite.blimsup_set_eq :
    blimsup s cofinite p = { x | { n | p n ∧ x ∈ s n }.Infinite } := by
  simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
  ext x
  refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose! h
  · simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
    exact ⟨{x}ᶜ, by simpa using h, by simp⟩
  · exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩

Bounded Limit Superior Characterization for Cofinite Filter: $\text{blimsup}_{n \to \infty} s_n p = \{x \mid \text{infinitely many } n \text{ satisfy } p(n) \text{ and } x \in s_n\}$

Informal description

For a family of sets $s_n$ indexed by natural numbers and a predicate $p$, the bounded limit superior with respect to the cofinite filter is equal to the set of all elements $x$ such that the set $\{n \mid p(n) \text{ and } x \in s_n\}$ is infinite. In other words, \[ \text{blimsup}_{n \to \infty} s_n p = \{x \mid \text{there exist infinitely many } n \text{ such that } p(n) \text{ and } x \in s_n\}. \]

Filter.cofinite.bliminf_set_eq theorem

: bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}

Full source

theorem cofinite.bliminf_set_eq : bliminf s cofinite p = { x | { n | p n ∧ x ∉ s n }.Finite } := by
  rw [← compl_inj_iff]
  simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
    cofinite.blimsup_set_eq]
  rfl

Bounded Limit Inferior Characterization for Cofinite Filter: $\text{bliminf}_{n \to \infty} s_n p = \{x \mid x \in s_n \text{ for all but finitely many } n \text{ with } p(n)\}$

Informal description

For a family of sets $(s_n)_{n \in \mathbb{N}}$ and a predicate $p$ on $\mathbb{N}$, the bounded limit inferior with respect to the cofinite filter is the set of all elements $x$ such that the set $\{n \mid p(n) \text{ and } x \notin s_n\}$ is finite. In other words, \[ \text{bliminf}_{n \to \infty} s_n p = \{x \mid x \in s_n \text{ for all but finitely many } n \text{ satisfying } p(n)\}. \]

Filter.cofinite.limsup_set_eq theorem

: limsup s cofinite = {x | {n | x ∈ s n}.Infinite}

Full source

/-- In other words, `limsup cofinite s` is the set of elements lying inside the family `s`
infinitely often. -/
theorem cofinite.limsup_set_eq : limsup s cofinite = { x | { n | x ∈ s n }.Infinite } := by
  simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

Characterization of Set Limit Superior under Cofinite Filter: $\limsup_{n \to \infty} s_n = \{x \mid x \in s_n \text{ infinitely often}\}$

Informal description

For a sequence of sets $(s_n)_{n \in \mathbb{N}}$, the limit superior with respect to the cofinite filter is the set of all elements $x$ that belong to infinitely many sets $s_n$. In other words, \[ \limsup_{n \to \infty} s_n = \{x \mid x \in s_n \text{ for infinitely many } n\}. \]

Filter.cofinite.liminf_set_eq theorem

: liminf s cofinite = {x | {n | x ∉ s n}.Finite}

Full source

/-- In other words, `liminf cofinite s` is the set of elements lying outside the family `s`
finitely often. -/
theorem cofinite.liminf_set_eq : liminf s cofinite = { x | { n | x ∉ s n }.Finite } := by
  simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

Characterization of Set Limit Inferior under Cofinite Filter: $\liminf_{n \to \infty} s_n = \{x \mid x \in s_n \text{ for all but finitely many } n\}$

Informal description

For a sequence of sets $(s_n)_{n \in \mathbb{N}}$, the limit inferior with respect to the cofinite filter is the set of all elements $x$ such that the set $\{n \mid x \notin s_n\}$ is finite. In other words, \[ \liminf_{n \to \infty} s_n = \{x \mid x \in s_n \text{ for all but finitely many } n\}. \]

Filter.exists_forall_mem_of_hasBasis_mem_blimsup theorem

 {l : Filter β} {b : ι → Set β} {q : ι → Prop} (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α}
  (hx : x ∈ blimsup u l p) : ∃ f : {i | q i} → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Full source

theorem exists_forall_mem_of_hasBasis_mem_blimsup {l : Filter β} {b : ι → Set β} {q : ι → Prop}
    (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ blimsup u l p) :
    ∃ f : { i | q i } → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i := by
  rw [blimsup_eq_iInf_biSup] at hx
  simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx
  choose g hg hg' using hx
  refine ⟨fun i : { i | q i } => g (b i) (hl.mem_of_mem i.2), fun i => ⟨?_, ?_⟩⟩
  · exact hg' (b i) (hl.mem_of_mem i.2)
  · exact hg (b i) (hl.mem_of_mem i.2)

Existence of Witnesses for Bounded Limit Superior Membership via Filter Basis

Informal description

Let $l$ be a filter on $\beta$ with a basis $\{b_i\}_{i \in \iota}$ indexed by a predicate $q : \iota \to \text{Prop}$. Let $u : \beta \to \text{Set } \alpha$ be a function and $p : \beta \to \text{Prop}$ a predicate. If $x$ belongs to the bounded limit superior $\text{blimsup}_l(u, p)$, then there exists a function $f : \{i \mid q(i)\} \to \beta$ such that for every $i$ with $q(i)$, the following hold: 1. $x \in u(f(i))$, 2. $p(f(i))$ is true, and 3. $f(i) \in b_i$.

Filter.exists_forall_mem_of_hasBasis_mem_blimsup' theorem

 {l : Filter β} {b : ι → Set β} (hl : l.HasBasis (fun _ => True) b) {u : β → Set α} {p : β → Prop} {x : α}
  (hx : x ∈ blimsup u l p) : ∃ f : ι → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

Full source

theorem exists_forall_mem_of_hasBasis_mem_blimsup' {l : Filter β} {b : ι → Set β}
    (hl : l.HasBasis (fun _ => True) b) {u : β → Set α} {p : β → Prop} {x : α}
    (hx : x ∈ blimsup u l p) : ∃ f : ι → β, ∀ i, x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i := by
  obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
  exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩

Existence of Witnesses for Bounded Limit Superior Membership via Trivial Filter Basis

Informal description

Let $l$ be a filter on $\beta$ with a basis $\{b_i\}_{i \in \iota}$ (where the index predicate is always true). Let $u : \beta \to \mathcal{P}(\alpha)$ be a set-valued function and $p : \beta \to \text{Prop}$ a predicate. If $x$ belongs to the bounded limit superior $\text{blimsup}_l(u, p)$, then there exists a function $f : \iota \to \beta$ such that for every $i \in \iota$, the following hold: 1. $x \in u(f(i))$, 2. $p(f(i))$ is true, and 3. $f(i) \in b_i$.

Filter.eventually_lt_add_pos_of_limsup_le theorem

 [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder LE.le atTop u)
  (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) : ∀ᶠ b : β in atTop, u b < x + ε

Full source

/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, eventually we have `u b < x + ε`. -/
theorem eventually_lt_add_pos_of_limsup_le [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x)
    (hε : 0 < ε) :
    ∀ᶠ b : β in atTop, u b < x + ε :=
  eventually_lt_of_limsup_lt (lt_of_le_of_lt hu (lt_add_of_pos_right x hε)) hu_bdd

Eventual Upper Bound for Functions Below Limit Superior

Informal description

Let $\alpha$ be a conditionally complete linear order with an additive zero class structure and left-strictly monotone addition, and let $\beta$ be a preorder. For a function $u : \beta \to \alpha$ that is bounded above along the filter `atTop`, if $\limsup u \leq x$ and $\varepsilon > 0$, then eventually for $b$ in `atTop`, we have $u(b) < x + \varepsilon$.

Filter.eventually_add_neg_lt_of_le_liminf theorem

 [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder GE.ge atTop u)
  (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) : ∀ᶠ b : β in atTop, x + ε < u b

Full source

/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, eventually we have `x + ε < u b`. -/
theorem eventually_add_neg_lt_of_le_liminf [Preorder β] [AddZeroClass α] [AddLeftStrictMono α]
    {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop)
    (hε : ε < 0) :
    ∀ᶠ b : β in atTop, x + ε < u b :=
  eventually_lt_of_lt_liminf (lt_of_lt_of_le (add_lt_of_neg_right x hε) hu) hu_bdd

Eventual Lower Bound for Functions Below Limit Inferior

Informal description

Let $\alpha$ be a conditionally complete linear order with an additive zero class structure and left-strictly monotone addition, and let $\beta$ be a preorder. For a function $u : \beta \to \alpha$ that is bounded below along the filter `atTop`, if $x \leq \liminf u$ and $\varepsilon < 0$, then eventually for $b$ in `atTop`, we have $x + \varepsilon < u(b)$.

Filter.exists_lt_of_limsup_le theorem

 [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : IsBoundedUnder LE.le atTop u)
  (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) : ∃ n : PNat, u n < x + ε

Full source

/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, there exists a positive natural
number `n` such that `u n < x + ε`. -/
theorem exists_lt_of_limsup_le [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
    (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) :
    ∃ n : PNat, u n < x + ε := by
  have h : ∀ᶠ n : ℕ in atTop, u n < x + ε := eventually_lt_add_pos_of_limsup_le hu_bdd hu hε
  simp only [eventually_atTop] at h
  obtain ⟨n, hn⟩ := h
  exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Existence of Positive Natural Number Below Limit Superior with Positive Perturbation

Informal description

Let $\alpha$ be a conditionally complete linear order with an additive zero class structure and left-strictly monotone addition. For a function $u : \mathbb{N} \to \alpha$ that is bounded above along the filter `atTop`, if $\limsup u \leq x$ and $\varepsilon > 0$, then there exists a positive natural number $n$ such that $u(n) < x + \varepsilon$.

Filter.exists_lt_of_le_liminf theorem

 [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : IsBoundedUnder GE.ge atTop u)
  (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) : ∃ n : PNat, x + ε < u n

Full source

/-- If `x ≤ Filter.liminf u atTop`, then for all `ε < 0`, there exists a positive natural
number `n` such that ` x + ε < u n`. -/
theorem exists_lt_of_le_liminf [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
    (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) :
    ∃ n : PNat, x + ε < u n := by
  have h : ∀ᶠ n : ℕ in atTop, x + ε < u n := eventually_add_neg_lt_of_le_liminf hu_bdd hu hε
  simp only [eventually_atTop] at h
  obtain ⟨n, hn⟩ := h
  exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Existence of Positive Natural Number Below Limit Inferior with Negative Perturbation

Informal description

Let $\alpha$ be a conditionally complete linear order with an additive zero class structure and left-strictly monotone addition. For a function $u : \mathbb{N} \to \alpha$ that is bounded below along the filter `atTop`, if $x \leq \liminf u$ and $\varepsilon < 0$, then there exists a positive natural number $n$ such that $x + \varepsilon < u(n)$.

Filter.lt_mem_sets_of_limsSup_lt theorem

(h : f.IsBounded (· ≤ ·)) (l : f.limsSup < b) : ∀ᶠ a in f, a < b

Full source

theorem lt_mem_sets_of_limsSup_lt (h : f.IsBounded (· ≤ ·)) (l : f.limsSup < b) :
    ∀ᶠ a in f, a < b :=
  let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_csInf_lt h l
  mem_of_superset h fun _a => hcb.trans_le'

Eventual Upper Bound from Strict Limsup Inequality

Informal description

Let $f$ be a filter on a conditionally complete linear order $\alpha$ that is bounded above. If the limit superior of $f$ is strictly less than an element $b \in \alpha$, then eventually all elements in $f$ are less than $b$. In other words, $\limsup f < b$ implies $\forall^\ast a \in f, a < b$.

Filter.gt_mem_sets_of_limsInf_gt theorem

: f.IsBounded (· ≥ ·) → b < f.limsInf → ∀ᶠ a in f, b < a

Full source

theorem gt_mem_sets_of_limsInf_gt : f.IsBounded (· ≥ ·) → b < f.limsInf → ∀ᶠ a in f, b < a :=
  @lt_mem_sets_of_limsSup_lt αᵒᵈ _ _ _

Eventual Lower Bound from Strict Liminf Inequality

Informal description

Let $\alpha$ be a conditionally complete linear order and $f$ a filter on $\alpha$ that is bounded below. If an element $b \in \alpha$ is strictly less than the limit inferior of $f$, then eventually all elements in $f$ are greater than $b$. In other words, $b < \liminf f$ implies $\forall^\ast a \in f, b < a$.

Filter.liminf_reparam definition

 (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p

Full source

/-- Given an indexed family of sets `s j` over `j : Subtype p` and a function `f`, then
`liminf_reparam j` is equal to `j` if `f` is bounded below on `s j`, and otherwise to some
index `k` such that `f` is bounded below on `s k` (if there exists one).
To ensure good measurability behavior, this index `k` is chosen as the minimal suitable index.
This function is used to write down a liminf in a measurable way,
in `Filter.HasBasis.liminf_eq_ciSup_ciInf` and `Filter.HasBasis.liminf_eq_ite`. -/
noncomputable def liminf_reparam
    (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)]
    (j : Subtype p) : Subtype p :=
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  let g : ℕ → Subtype p := (exists_surjective_nat _).choose
  have Z : ∃ n, g n ∈ m ∨ ∀ j, j ∉ m := by
    by_cases H : ∃ j, j ∈ m
    · rcases H with ⟨j, hj⟩
      rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩
      exact ⟨n, Or.inl hj⟩
    · push_neg at H
      exact ⟨0, Or.inr H⟩
  if j ∈ m then j else g (Nat.find Z)

Reparameterization for liminf computation

Informal description

Given a countable family of sets $ s_j $ indexed by $ j \in \{j' \mid p j'\} $ and a function $ f : \iota \to \alpha $ where $ \alpha $ is a conditionally complete linear order, the function `liminf_reparam` maps an index $ j $ to itself if $ f $ is bounded below on $ s_j $, and otherwise to some index $ k $ such that $ f $ is bounded below on $ s_k $ (if such an index exists). The choice of $ k $ is made minimally to ensure good measurability properties. This function is used to express the liminf in a measurable way in subsequent theorems.

Filter.HasBasis.liminf_eq_ciSup_ciInf theorem

 {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s)
  {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty) (H : ∃ (j : Subtype p), BddBelow (range (fun (i : s j) ↦ f i))) :
  liminf f v = ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i

Full source

/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below. -/
theorem HasBasis.liminf_eq_ciSup_ciInf {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)]
    (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty)
    (H : ∃ (j : Subtype p), BddBelow (range (fun (i : s j) ↦ f i))) :
    liminf f v = ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i := by
  classical
  rcases H with ⟨j0, hj0⟩
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)
  have A : ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) =
         ⋃ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) := by
    apply Subset.antisymm
    · apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminf_reparam f s p j := by simp only [m, liminf_reparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_setOf_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]
    · apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminf_reparam f s p j)
  have B : ∀ (j : Subtype p), ⋂ (i : s (liminf_reparam f s p j)), Iic (f i) =
                                Iic (⨅ (i : s (liminf_reparam f s p j)), f i) := by
    intro j
    apply (Iic_ciInf _).symm
    change liminf_reparamliminf_reparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminf_reparam, if_pos Hj] using Hj
    · simp only [m, liminf_reparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ|hZ
      · exact hZ
      · exact (hZ j0 hj0).elim
  simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]

Limit Inferior as Supremum of Infima via Reparameterization

Informal description

Let $\alpha$ be a conditionally complete linear order, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a countable basis consisting of nonempty sets $s(j)$ indexed by $j \in \{j' \mid p(j')\}$. Suppose there exists $j$ such that $f$ is bounded below on $s(j)$. Then the limit inferior of $f$ along $v$ equals the supremum over all $j$ of the infimum of $f$ over the set $s(k_j)$, where $k_j$ is the reparameterized index obtained from `liminf_reparam`. In symbols: \[ \liminf_{v} f = \sup_{j} \inf_{i \in s(k_j)} f(i). \]

Filter.HasBasis.liminf_eq_ite theorem

 {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s)
  (f : ι → α) :
  liminf f v =
    if ∃ (j : Subtype p), s j = ∅ then sSup univ
    else
      if ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i)) then sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i

Full source

/-- Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are
not bounded below. -/
theorem HasBasis.liminf_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι}
    [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) :
    liminf f v = if ∃ (j : Subtype p), s j = ∅ then sSup univ else
      if ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i)) then sSup ∅
      else ⨆ (j : Subtype p), ⨅ (i : s (liminf_reparam f s p j)), f i := by
  by_cases H : ∃ (j : Subtype p), s j = ∅
  · rw [if_pos H]
    rcases H with ⟨j, hj⟩
    simp [hv.liminf_eq_sSup_univ_of_empty j j.2 hj]
  rw [if_neg H]
  by_cases H' : ∀ (j : Subtype p), ¬BddBelow (range (fun (i : s j) ↦ f i))
  · have A : ∀ (j : Subtype p), ⋂ (i : s j), Iic (f i) = ∅ := by
      simp_rw [← not_nonempty_iff_eq_empty, nonempty_iInter_Iic_iff]
      exact H'
    simp_rw [if_pos H', hv.liminf_eq_sSup_iUnion_iInter, A, iUnion_empty]
  rw [if_neg H']
  apply hv.liminf_eq_ciSup_ciInf
  · push_neg at H
    simpa only [nonempty_iff_ne_empty] using H
  · push_neg at H'
    exact H'

Limit Inferior Formula via Cases for Filter Basis

Informal description

Let $\alpha$ be a conditionally complete linear order, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a countable basis consisting of sets $s(j)$ indexed by $j \in \{j' \mid p(j')\}$. Then the limit inferior of $f$ along $v$ is given by: \[ \liminf_{v} f = \begin{cases} \sup \text{univ} & \text{if } \exists j \text{ such that } s(j) = \emptyset, \\ \sup \emptyset & \text{if } \forall j, f \text{ is not bounded below on } s(j), \\ \sup_{j} \inf_{i \in s(k_j)} f(i) & \text{otherwise}, \end{cases} \] where $k_j$ is the reparameterized index obtained from `liminf_reparam`.

Filter.limsup_reparam definition

 (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p

Full source

/-- Given an indexed family of sets `s j` and a function `f`, then `limsup_reparam j` is equal
to `j` if `f` is bounded above on `s j`, and otherwise to some index `k` such that `f` is bounded
above on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is
chosen as the minimal suitable index. This function is used to write down a limsup in a measurable
way, in `Filter.HasBasis.limsup_eq_ciInf_ciSup` and `Filter.HasBasis.limsup_eq_ite`. -/
noncomputable def limsup_reparam
    (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)]
    (j : Subtype p) : Subtype p :=
  liminf_reparam (α := αᵒᵈ) f s p j

Reparameterization for limsup computation

Informal description

Given a countable family of sets $ s_j $ indexed by $ j \in \{j' \mid p j'\} $ and a function $ f : \iota \to \alpha $ where $ \alpha $ is a conditionally complete linear order, the function `limsup_reparam` maps an index $ j $ to itself if $ f $ is bounded above on $ s_j $, and otherwise to some index $ k $ such that $ f $ is bounded above on $ s_k $ (if such an index exists). The choice of $ k $ is made minimally to ensure good measurability properties. This function is used to express the limsup in a measurable way in subsequent theorems.

Filter.HasBasis.limsup_eq_ciInf_ciSup theorem

 {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s)
  {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty) (H : ∃ (j : Subtype p), BddAbove (range (fun (i : s j) ↦ f i))) :
  limsup f v = ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i

Full source

/-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are
not bounded above. -/
theorem HasBasis.limsup_eq_ciInf_ciSup {v : Filter ι}
    {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)]
    (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty)
    (H : ∃ (j : Subtype p), BddAbove (range (fun (i : s j) ↦ f i))) :
    limsup f v = ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i :=
  HasBasis.liminf_eq_ciSup_ciInf (α := αᵒᵈ) hv hs H

Limit Superior as Infimum of Suprema via Reparameterization

Informal description

Let $\alpha$ be a conditionally complete linear order, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a countable basis consisting of nonempty sets $s(j)$ indexed by $j \in \{j' \mid p(j')\}$. Suppose there exists $j$ such that $f$ is bounded above on $s(j)$. Then the limit superior of $f$ along $v$ equals the infimum over all $j$ of the supremum of $f$ over the set $s(k_j)$, where $k_j$ is the reparameterized index obtained from `limsup_reparam`. In symbols: \[ \limsup_{v} f = \inf_{j} \sup_{i \in s(k_j)} f(i). \]

Filter.HasBasis.limsup_eq_ite theorem

 {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s)
  (f : ι → α) :
  limsup f v =
    if ∃ (j : Subtype p), s j = ∅ then sInf univ
    else
      if ∀ (j : Subtype p), ¬BddAbove (range (fun (i : s j) ↦ f i)) then sInf ∅
      else ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i

Full source

/-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are
not bounded below. -/
theorem HasBasis.limsup_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι}
    [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) :
    limsup f v = if ∃ (j : Subtype p), s j = ∅ then sInf univ else
      if ∀ (j : Subtype p), ¬BddAbove (range (fun (i : s j) ↦ f i)) then sInf ∅
      else ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i :=
  HasBasis.liminf_eq_ite (α := αᵒᵈ) hv f

Limit Superior Formula via Cases for Filter Basis

Informal description

Let $\alpha$ be a conditionally complete linear order, $\iota$ and $\iota'$ types, $f : \iota \to \alpha$ a function, and $v$ a filter on $\iota$ with a countable basis consisting of sets $s(j)$ indexed by $j \in \{j' \mid p(j')\}$. Then the limit superior of $f$ along $v$ is given by: \[ \limsup_{v} f = \begin{cases} \inf \text{univ} & \text{if } \exists j \text{ such that } s(j) = \emptyset, \\ \inf \emptyset & \text{if } \forall j, f \text{ is not bounded above on } s(j), \\ \inf_{j} \sup_{i \in s(k_j)} f(i) & \text{otherwise}, \end{cases} \] where $k_j$ is the reparameterized index obtained from `limsup_reparam`.