Mathlib.Topology.Algebra.Order.LiminfLimsup

BoundedLENhdsClass structure

(α : Type*) [Preorder α] [TopologicalSpace α]

Full source

/-- Ad hoc typeclass stating that neighborhoods are eventually bounded above. -/
class BoundedLENhdsClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
  isBounded_le_nhds (a : α) : (𝓝 a).IsBounded (· ≤ ·)

Neighborhoods eventually bounded above

Informal description

A typeclass stating that for any element $a$ in a preorder $\alpha$ equipped with a topology, the neighborhood filter of $a$ is eventually bounded above with respect to the order $\leq$. This means there exists some upper bound for all elements sufficiently close to $a$.

BoundedGENhdsClass structure

(α : Type*) [Preorder α] [TopologicalSpace α]

Full source

/-- Ad hoc typeclass stating that neighborhoods are eventually bounded below. -/
class BoundedGENhdsClass (α : Type*) [Preorder α] [TopologicalSpace α] : Prop where
  isBounded_ge_nhds (a : α) : (𝓝 a).IsBounded (· ≥ ·)

Neighborhoods eventually bounded below

Informal description

A typeclass stating that for any element $a$ in a preorder $\alpha$ with a topology, the neighborhood filter of $a$ is eventually bounded below with respect to the order $\leq$. In other words, there exists a neighborhood of $a$ where all elements are greater than or equal to some common lower bound.

isBounded_le_nhds theorem

(a : α) : (𝓝 a).IsBounded (· ≤ ·)

Full source

theorem isBounded_le_nhds (a : α) : (𝓝 a).IsBounded (· ≤ ·) :=
  BoundedLENhdsClass.isBounded_le_nhds _

Neighborhood filter is eventually bounded above

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a topology, the neighborhood filter of $a$ is bounded above with respect to the order $\leq$. That is, there exists an upper bound $b$ such that all elements sufficiently close to $a$ satisfy $x \leq b$.

Filter.Tendsto.isBoundedUnder_le theorem

(h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≤ ·) u

Full source

theorem Filter.Tendsto.isBoundedUnder_le (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≤ ·) u :=
  (isBounded_le_nhds a).mono h

Boundedness Under Tendency to a Point in a Preordered Topological Space

Informal description

Let $\alpha$ be a topological space with a preorder $\leq$, and let $u : \beta \to \alpha$ be a function. If $u$ tends to $a$ under the filter $f$ (i.e., $\text{Tendsto } u f (\mathfrak{N} a)$), then $f$ is bounded under $\leq$ with respect to $u$. That is, there exists some $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $u(x) \leq b$.

Filter.Tendsto.bddAbove_range_of_cofinite theorem

[IsDirected α (· ≤ ·)] (h : Tendsto u cofinite (𝓝 a)) : BddAbove (Set.range u)

Full source

theorem Filter.Tendsto.bddAbove_range_of_cofinite [IsDirected α (· ≤ ·)]
    (h : Tendsto u cofinite (𝓝 a)) : BddAbove (Set.range u) :=
  h.isBoundedUnder_le.bddAbove_range_of_cofinite

Range of a Function Tending to a Point under Cofinite Filter is Bounded Above

Informal description

Let $\alpha$ be a topological space with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$. Given a function $u \colon \alpha \to \alpha$ and a point $a \in \alpha$, if $u$ tends to $a$ under the cofinite filter, then the range of $u$ is bounded above in $\alpha$.

Filter.Tendsto.bddAbove_range theorem

[IsDirected α (· ≤ ·)] {u : ℕ → α} (h : Tendsto u atTop (𝓝 a)) : BddAbove (Set.range u)

Full source

theorem Filter.Tendsto.bddAbove_range [IsDirected α (· ≤ ·)] {u : ℕ → α}
    (h : Tendsto u atTop (𝓝 a)) : BddAbove (Set.range u) :=
  h.isBoundedUnder_le.bddAbove_range

Range of a Function Tending to a Point under `atTop` Filter is Bounded Above

Informal description

Let $\alpha$ be a topological space with a preorder $\leq$ such that $\alpha$ is directed with respect to $\leq$. Given a function $u \colon \mathbb{N} \to \alpha$ and a point $a \in \alpha$, if $u$ tends to $a$ under the `atTop` filter on $\mathbb{N}$, then the range of $u$ is bounded above in $\alpha$.

isCobounded_ge_nhds theorem

(a : α) : (𝓝 a).IsCobounded (· ≥ ·)

Full source

theorem isCobounded_ge_nhds (a : α) : (𝓝 a).IsCobounded (· ≥ ·) :=
  (isBounded_le_nhds a).isCobounded_flip

Neighborhood Filter is Cobounded Below with Respect to $\geq$

Informal description

For any element $a$ in a preorder $\alpha$ equipped with a topology, the neighborhood filter of $a$ is cobounded with respect to the relation $\geq$. That is, there exists a lower bound $b$ such that for all elements sufficiently close to $a$, the set $\{x \mid x \geq b\}$ is nonempty and does not contain the empty set.

Filter.Tendsto.isCoboundedUnder_ge theorem

[NeBot f] (h : Tendsto u f (𝓝 a)) : f.IsCoboundedUnder (· ≥ ·) u

Full source

theorem Filter.Tendsto.isCoboundedUnder_ge [NeBot f] (h : Tendsto u f (𝓝 a)) :
    f.IsCoboundedUnder (· ≥ ·) u :=
  h.isBoundedUnder_le.isCobounded_flip

Coboundedness Below for Functions Tending to a Point in a Preordered Topological Space

Informal description

Let $\alpha$ be a topological space with a preorder $\leq$, and let $u : \beta \to \alpha$ be a function. If $f$ is a non-trivial filter on $\beta$ and $u$ tends to $a$ under $f$ (i.e., $\text{Tendsto } u f (\mathfrak{N} a)$), then $f$ is cobounded under $\geq$ with respect to $u$. That is, there exists some $b \in \alpha$ such that the set $\{x \mid u(x) \geq b\}$ is frequently nonempty in $f$.

instBoundedGENhdsClassOrderDual instance

: BoundedGENhdsClass αᵒᵈ

Full source

instance : BoundedGENhdsClass αᵒᵈ := ⟨@isBounded_le_nhds α _ _ _⟩

Order Dual Preserves Neighborhood Boundedness Below

Informal description

For any preorder $\alpha$ with a topology, the order dual $\alpha^\text{op}$ satisfies the property that neighborhoods are eventually bounded below with respect to the dual order $\geq$.

Prod.instBoundedLENhdsClass instance

: BoundedLENhdsClass (α × β)

Full source

instance Prod.instBoundedLENhdsClass : BoundedLENhdsClass (α × β) := by
  refine ⟨fun x ↦ ?_⟩
  obtain ⟨a, ha⟩ := isBounded_le_nhds x.1
  obtain ⟨b, hb⟩ := isBounded_le_nhds x.2
  rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]
  exact ⟨(a, b), ha.prod_mk hb⟩

Product Spaces Preserve Neighborhood Boundedness Above

Informal description

For any two preordered topological spaces $\alpha$ and $\beta$ where neighborhoods are eventually bounded above, the product space $\alpha \times \beta$ also has neighborhoods that are eventually bounded above with respect to the product order. That is, for any point $(a, b) \in \alpha \times \beta$, there exists an upper bound $(u, v)$ such that all points in some neighborhood of $(a, b)$ satisfy $(x, y) \leq (u, v)$.

Pi.instBoundedLENhdsClass instance

 [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)] [∀ i, BoundedLENhdsClass (π i)] :
  BoundedLENhdsClass (∀ i, π i)

Full source

instance Pi.instBoundedLENhdsClass [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
    [∀ i, BoundedLENhdsClass (π i)] : BoundedLENhdsClass (∀ i, π i) := by
  refine ⟨fun x ↦ ?_⟩
  rw [nhds_pi]
  choose f hf using fun i ↦ isBounded_le_nhds (x i)
  exact ⟨f, eventually_pi hf⟩

Neighborhoods in Finite Product Spaces are Eventually Bounded Above

Informal description

For a finite index set $\iota$ and a family of preordered topological spaces $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ has neighborhoods eventually bounded above, the product space $\prod_{i \in \iota} \pi_i$ also has neighborhoods eventually bounded above with respect to the product order. That is, for any point $a = (a_i)_{i \in \iota}$ in the product space, there exists an upper bound $b = (b_i)_{i \in \iota}$ such that all points in some neighborhood of $a$ satisfy $x \leq b$ componentwise.

isBounded_ge_nhds theorem

(a : α) : (𝓝 a).IsBounded (· ≥ ·)

Full source

theorem isBounded_ge_nhds (a : α) : (𝓝 a).IsBounded (· ≥ ·) :=
  BoundedGENhdsClass.isBounded_ge_nhds _

Neighborhood Filter is Eventually Bounded Below

Informal description

For any element $a$ in a preorder $\alpha$ with a topology where neighborhoods are eventually bounded below (i.e., $\alpha$ satisfies `BoundedGENhdsClass`), the neighborhood filter $\mathcal{N}(a)$ is bounded below with respect to the order $\geq$. In other words, there exists an element $b \in \alpha$ such that for all $x$ in some neighborhood of $a$, $x \geq b$.

Filter.Tendsto.isBoundedUnder_ge theorem

(h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≥ ·) u

Full source

theorem Filter.Tendsto.isBoundedUnder_ge (h : Tendsto u f (𝓝 a)) : f.IsBoundedUnder (· ≥ ·) u :=
  (isBounded_ge_nhds a).mono h

Boundedness Below Under Tendency to a Point in a Preordered Topological Space

Informal description

Let $\alpha$ be a topological space with a preorder and suppose $\alpha$ satisfies `BoundedGENhdsClass`. Given a function $u : \beta \to \alpha$ and a filter $f$ on $\beta$, if $u$ tends to $a \in \alpha$ along $f$ (i.e., $\text{Tendsto } u f (\mathcal{N}(a))$), then the filter $f$ is bounded below under the relation $\geq$ with respect to $u$. In other words, there exists an element $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $u(x) \geq b$.

Filter.Tendsto.bddBelow_range_of_cofinite theorem

[IsDirected α (· ≥ ·)] (h : Tendsto u cofinite (𝓝 a)) : BddBelow (Set.range u)

Full source

theorem Filter.Tendsto.bddBelow_range_of_cofinite [IsDirected α (· ≥ ·)]
    (h : Tendsto u cofinite (𝓝 a)) : BddBelow (Set.range u) :=
  h.isBoundedUnder_ge.bddBelow_range_of_cofinite

Range of a Function Tending to a Point Along Cofinite Filter is Bounded Below

Informal description

Let $\alpha$ be a preordered topological space where the order $\geq$ is directed. Given a function $u \colon \alpha \to \alpha$ that tends to a point $a \in \alpha$ along the cofinite filter, the range of $u$ is bounded below in $\alpha$.

Filter.Tendsto.bddBelow_range theorem

[IsDirected α (· ≥ ·)] {u : ℕ → α} (h : Tendsto u atTop (𝓝 a)) : BddBelow (Set.range u)

Full source

theorem Filter.Tendsto.bddBelow_range [IsDirected α (· ≥ ·)] {u : ℕ → α}
    (h : Tendsto u atTop (𝓝 a)) : BddBelow (Set.range u) :=
  h.isBoundedUnder_ge.bddBelow_range

Range of a Sequence Tending to a Point is Bounded Below in a Directed Preorder

Informal description

Let $\alpha$ be a preordered topological space where the order $\geq$ is directed. Given a function $u \colon \mathbb{N} \to \alpha$ that tends to a point $a \in \alpha$ along the `atTop` filter on $\mathbb{N}$, the range of $u$ is bounded below in $\alpha$.

isCobounded_le_nhds theorem

(a : α) : (𝓝 a).IsCobounded (· ≤ ·)

Full source

theorem isCobounded_le_nhds (a : α) : (𝓝 a).IsCobounded (· ≤ ·) :=
  (isBounded_ge_nhds a).isCobounded_flip

Neighborhood Filter is Cobounded Above with Respect to $\leq$

Informal description

For any element $a$ in a preorder $\alpha$ with a topology, the neighborhood filter $\mathcal{N}(a)$ is cobounded with respect to the order $\leq$. That is, there exists an upper bound $b \in \alpha$ such that for all $x$ in some neighborhood of $a$, $x \leq b$.

Filter.Tendsto.isCoboundedUnder_le theorem

[NeBot f] (h : Tendsto u f (𝓝 a)) : f.IsCoboundedUnder (· ≤ ·) u

Full source

theorem Filter.Tendsto.isCoboundedUnder_le [NeBot f] (h : Tendsto u f (𝓝 a)) :
    f.IsCoboundedUnder (· ≤ ·) u :=
  h.isBoundedUnder_ge.isCobounded_flip

Coboundedness Above Under Tendency to a Point in a Preordered Topological Space

Informal description

Let $\alpha$ be a topological space with a preorder, and let $f$ be a non-trivial filter on a type $\beta$. Given a function $u : \beta \to \alpha$ that tends to a point $a \in \alpha$ along $f$, the filter $f$ is cobounded above under the relation $\leq$ with respect to $u$. That is, there exists an upper bound $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $u(x) \leq b$.

instBoundedLENhdsClassOrderDual instance

: BoundedLENhdsClass αᵒᵈ

Full source

instance : BoundedLENhdsClass αᵒᵈ := ⟨@isBounded_ge_nhds α _ _ _⟩

Order Dual Preserves Bounded Above Neighborhoods

Informal description

For any preorder $\alpha$ with a topology, if $\alpha$ satisfies the condition that neighborhoods are eventually bounded above (i.e., $\alpha$ is an instance of `BoundedLENhdsClass`), then the order dual $\alpha^\text{op}$ also satisfies this condition. In other words, the neighborhood filter of any point in $\alpha^\text{op}$ is eventually bounded above with respect to the dual order $\geq$.

Prod.instBoundedGENhdsClass instance

: BoundedGENhdsClass (α × β)

Full source

instance Prod.instBoundedGENhdsClass : BoundedGENhdsClass (α × β) :=
  ⟨(Prod.instBoundedLENhdsClass (α := αᵒᵈ) (β := βᵒᵈ)).isBounded_le_nhds⟩

Product Spaces Preserve Neighborhood Boundedness Below

Informal description

For any two preordered topological spaces $\alpha$ and $\beta$ where neighborhoods are eventually bounded below, the product space $\alpha \times \beta$ also has neighborhoods that are eventually bounded below with respect to the product order. That is, for any point $(a, b) \in \alpha \times \beta$, there exists a lower bound $(l, m)$ such that all points in some neighborhood of $(a, b)$ satisfy $(x, y) \geq (l, m)$.

Pi.instBoundedGENhdsClass instance

 [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)] [∀ i, BoundedGENhdsClass (π i)] :
  BoundedGENhdsClass (∀ i, π i)

Full source

instance Pi.instBoundedGENhdsClass [Finite ι] [∀ i, Preorder (π i)] [∀ i, TopologicalSpace (π i)]
    [∀ i, BoundedGENhdsClass (π i)] : BoundedGENhdsClass (∀ i, π i) :=
  ⟨(Pi.instBoundedLENhdsClass (π := fun i ↦ (π i)ᵒᵈ)).isBounded_le_nhds⟩

Neighborhoods in Finite Product Spaces are Eventually Bounded Below

Informal description

For a finite index set $\iota$ and a family of preordered topological spaces $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ has neighborhoods eventually bounded below, the product space $\prod_{i \in \iota} \pi_i$ also has neighborhoods eventually bounded below with respect to the product order. That is, for any point $a = (a_i)_{i \in \iota}$ in the product space, there exists a lower bound $b = (b_i)_{i \in \iota}$ such that all points in some neighborhood of $a$ satisfy $x \geq b$ componentwise.

OrderTop.to_BoundedLENhdsClass instance

[OrderTop α] : BoundedLENhdsClass α

Full source

instance (priority := 100) OrderTop.to_BoundedLENhdsClass [OrderTop α] : BoundedLENhdsClass α :=
  ⟨fun _a ↦ isBounded_le_of_top⟩

Neighborhood Filters in Order-Top Spaces are Eventually Bounded Above

Informal description

For any preorder $\alpha$ with a greatest element $\top$ and equipped with a topology, the neighborhood filter of any point is eventually bounded above with respect to the order $\leq$.

OrderBot.to_BoundedGENhdsClass instance

[OrderBot α] : BoundedGENhdsClass α

Full source

instance (priority := 100) OrderBot.to_BoundedGENhdsClass [OrderBot α] : BoundedGENhdsClass α :=
  ⟨fun _a ↦ isBounded_ge_of_bot⟩

Neighborhoods in Orders with Bottom Elements are Eventually Bounded Below

Informal description

Every preorder $\alpha$ with a bottom element $\bot$ and a topological structure satisfies the property that neighborhoods are eventually bounded below. That is, for any element $a \in \alpha$, there exists a neighborhood of $a$ where all elements are greater than or equal to some common lower bound.

BoundedLENhdsClass.of_closedIciTopology instance

[LinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] : BoundedLENhdsClass α

Full source

instance (priority := 100) BoundedLENhdsClass.of_closedIciTopology [LinearOrder α]
    [TopologicalSpace α] [ClosedIciTopology α] : BoundedLENhdsClass α :=
  ⟨fun a ↦ ((isTop_or_exists_gt a).elim fun h ↦ ⟨a, Eventually.of_forall h⟩) <|
    Exists.imp fun _b ↦ eventually_le_nhds⟩

Closed Upper Interval Topology Implies Eventually Bounded Above Neighborhoods

Informal description

For any linearly ordered topological space $\alpha$ where the closed upper intervals $[a, \infty)$ are closed sets, the neighborhood filter of any point is eventually bounded above with respect to the order $\leq$.

BoundedGENhdsClass.of_closedIicTopology instance

[LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] : BoundedGENhdsClass α

Full source

instance (priority := 100) BoundedGENhdsClass.of_closedIicTopology [LinearOrder α]
    [TopologicalSpace α] [ClosedIicTopology α] : BoundedGENhdsClass α :=
  inferInstanceAs <| BoundedGENhdsClass αᵒᵈαᵒᵈᵒᵈ

Closed Lower Interval Topology Implies Eventually Bounded Below Neighborhoods

Informal description

For any linearly ordered topological space $\alpha$ where the closed lower intervals $(-\infty, a]$ are closed sets, the neighborhood filter of any point is eventually bounded below with respect to the order $\leq$.

le_nhds_of_limsSup_eq_limsInf theorem

 {f : Filter α} {a : α} (hl : f.IsBounded (· ≤ ·)) (hg : f.IsBounded (· ≥ ·)) (hs : f.limsSup = a)
  (hi : f.limsInf = a) : f ≤ 𝓝 a

Full source

/-- If the liminf and the limsup of a filter coincide, then this filter converges to
their common value, at least if the filter is eventually bounded above and below. -/
theorem le_nhds_of_limsSup_eq_limsInf {f : Filter α} {a : α} (hl : f.IsBounded (· ≤ ·))
    (hg : f.IsBounded (· ≥ ·)) (hs : f.limsSup = a) (hi : f.limsInf = a) : f ≤ 𝓝 a :=
  tendsto_order.2 ⟨fun _ hb ↦ gt_mem_sets_of_limsInf_gt hg <| hi.symm ▸ hb,
    fun _ hb ↦ lt_mem_sets_of_limsSup_lt hl <| hs.symm ▸ hb⟩

Convergence Criterion via Coinciding Limsup and Liminf in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f$ be a filter on $\alpha$ that is both bounded above and below. If the limit superior and limit inferior of $f$ coincide and equal $a \in \alpha$, then $f$ converges to $a$ in the order topology. In other words, if $\limsup f = \liminf f = a$, then $f \leq \mathcal{N}(a)$, where $\mathcal{N}(a)$ denotes the neighborhood filter of $a$.

limsSup_nhds theorem

(a : α) : limsSup (𝓝 a) = a

Full source

theorem limsSup_nhds (a : α) : limsSup (𝓝 a) = a :=
  csInf_eq_of_forall_ge_of_forall_gt_exists_lt (isBounded_le_nhds a)
    (fun a' (h : { n : α | n ≤ a' }{ n : α | n ≤ a' } ∈ 𝓝 a) ↦ show a ≤ a' from @mem_of_mem_nhds _ _ a _ h)
    fun b (hba : a < b) ↦
    show ∃ c, { n : α | n ≤ c } ∈ 𝓝 a ∧ c < b from
      match dense_or_discrete a b with
      | Or.inl ⟨c, hac, hcb⟩ => ⟨c, ge_mem_nhds hac, hcb⟩
      | Or.inr ⟨_, h⟩ => ⟨a, (𝓝 a).sets_of_superset (gt_mem_nhds hba) h, hba⟩

Limit Superior of Neighborhood Filter Equals Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order equipped with the order topology. For any element $a \in \alpha$, the limit superior of the neighborhood filter of $a$ equals $a$, i.e., $\limsup \mathcal{N}(a) = a$.

limsInf_nhds theorem

(a : α) : limsInf (𝓝 a) = a

Full source

theorem limsInf_nhds (a : α) : limsInf (𝓝 a) = a :=
  limsSup_nhds (α := αᵒᵈ) a

Limit Inferior of Neighborhood Filter Equals Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order equipped with the order topology. For any element $a \in \alpha$, the limit inferior of the neighborhood filter of $a$ equals $a$, i.e., $\liminf \mathcal{N}(a) = a$.

limsInf_eq_of_le_nhds theorem

{f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsInf = a

Full source

/-- If a filter is converging, its limsup coincides with its limit. -/
theorem limsInf_eq_of_le_nhds {f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsInf = a :=
  have hb_ge : IsBounded (· ≥ ·) f := (isBounded_ge_nhds a).mono h
  have hb_le : IsBounded (· ≤ ·) f := (isBounded_le_nhds a).mono h
  le_antisymm
    (calc
      f.limsInf ≤ f.limsSup := limsInf_le_limsSup hb_le hb_ge
      _ ≤ (𝓝 a).limsSup := limsSup_le_limsSup_of_le h hb_ge.isCobounded_flip (isBounded_le_nhds a)
      _ = a := limsSup_nhds a)
    (calc
      a = (𝓝 a).limsInf := (limsInf_nhds a).symm
      _ ≤ f.limsInf := limsInf_le_limsInf_of_le h (isBounded_ge_nhds a) hb_le.isCobounded_flip)

Limit Inferior of Convergent Filter Equals Limit Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f$ be a non-trivial filter on $\alpha$. If $f$ converges to a point $a \in \alpha$ (i.e., $f \leq \mathcal{N}(a)$, where $\mathcal{N}(a)$ is the neighborhood filter of $a$), then the limit inferior of $f$ equals $a$, i.e., $\liminf f = a$.

limsSup_eq_of_le_nhds theorem

{f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsSup = a

Full source

/-- If a filter is converging, its liminf coincides with its limit. -/
theorem limsSup_eq_of_le_nhds {f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsSup = a :=
  limsInf_eq_of_le_nhds (α := αᵒᵈ) h

Limit Superior of Convergent Filter Equals Limit Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $f$ be a non-trivial filter on $\alpha$. If $f$ converges to a point $a \in \alpha$ (i.e., $f \leq \mathcal{N}(a)$, where $\mathcal{N}(a)$ is the neighborhood filter of $a$), then the limit superior of $f$ equals $a$, i.e., $\limsup f = a$.

Filter.Tendsto.limsup_eq theorem

{f : Filter β} {u : β → α} {a : α} [NeBot f] (h : Tendsto u f (𝓝 a)) : limsup u f = a

Full source

/-- If a function has a limit, then its limsup coincides with its limit. -/
theorem Filter.Tendsto.limsup_eq {f : Filter β} {u : β → α} {a : α} [NeBot f]
    (h : Tendsto u f (𝓝 a)) : limsup u f = a :=
  limsSup_eq_of_le_nhds h

Limit Superior of Convergent Function Equals Limit Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $u : \beta \to \alpha$ be a function. For any non-trivial filter $f$ on $\beta$, if $u$ tends to $a \in \alpha$ along $f$ (i.e., $\lim_{x \to f} u(x) = a$), then the limit superior of $u$ along $f$ equals $a$, i.e., $\limsup_{f} u = a$.

Filter.Tendsto.liminf_eq theorem

{f : Filter β} {u : β → α} {a : α} [NeBot f] (h : Tendsto u f (𝓝 a)) : liminf u f = a

Full source

/-- If a function has a limit, then its liminf coincides with its limit. -/
theorem Filter.Tendsto.liminf_eq {f : Filter β} {u : β → α} {a : α} [NeBot f]
    (h : Tendsto u f (𝓝 a)) : liminf u f = a :=
  limsInf_eq_of_le_nhds h

Limit Inferior of Convergent Function Equals Limit Point in Order Topology

Informal description

Let $\alpha$ be a conditionally complete linear order with the order topology, and let $u : \beta \to \alpha$ be a function. For any non-trivial filter $f$ on $\beta$, if $u$ tends to $a \in \alpha$ along $f$ (i.e., $\text{Tendsto } u f (\mathcal{N}(a))$), then the limit inferior of $u$ along $f$ equals $a$, i.e., $\liminf_{f} u = a$.

limsup_eq_bot theorem

: f.limsup u = ⊥ ↔ u =ᶠ[f] ⊥

Full source

@[simp]
theorem limsup_eq_bot : f.limsup u = ⊥ ↔ u =ᶠ[f] ⊥ :=
  ⟨fun h =>
    (EventuallyLE.trans eventually_le_limsup <| Eventually.of_forall fun _ => h.le).mono fun _ hx =>
      le_antisymm hx bot_le,
    fun h => by
    rw [limsup_congr h]
    exact limsup_const_bot⟩

Limit Superior Equals Bottom if and only if Function is Eventually Bottom

Informal description

For a filter $f$ on a type $\beta$ and a function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice with a bottom element $\bot$, the limit superior of $u$ along $f$ equals $\bot$ if and only if $u$ is eventually equal to $\bot$ with respect to $f$. In other words, \[ \limsup_{x \to f} u(x) = \bot \quad \text{if and only if} \quad u(x) = \bot \text{ for } f\text{-almost all } x. \]

liminf_eq_top theorem

: f.liminf u = ⊤ ↔ u =ᶠ[f] ⊤

Full source

@[simp]
theorem liminf_eq_top : f.liminf u = ⊤ ↔ u =ᶠ[f] ⊤ :=
  limsup_eq_bot (α := αᵒᵈ)

Limit Inferior Equals Top if and only if Function is Eventually Top

Informal description

For a filter $f$ on a type $\beta$ and a function $u : \beta \to \alpha$ where $\alpha$ is a conditionally complete lattice with a top element $\top$, the limit inferior of $u$ along $f$ equals $\top$ if and only if $u$ is eventually equal to $\top$ with respect to $f$. In other words, \[ \liminf_{x \to f} u(x) = \top \quad \text{if and only if} \quad u(x) = \top \text{ for } f\text{-almost all } x. \]

le_limsup_mul theorem

 (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
  (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) : (limsup u f) * liminf v f ≤ limsup (u * v) f

Full source

lemma le_limsup_mul (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
    (limsup u f) * liminf v f ≤ limsup (u * v) f := by
  have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
  have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
  have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁ h₂
  have uv : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le ((h₁.and_eventually h₃).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv) h'
  refine mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_
  refine (le_limsup_iff h h').2 fun c c_ab ↦ ?_
  replace h₁ := IsCoboundedUnder.of_frequently_ge h₁ -- Pre-compute it to gain 4 s.
  have h₅ := frequently_lt_of_lt_limsup h₁ au
  have h₆ := eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)
  apply (h₅.and_eventually (h₆.and h₃)).mono
  exact fun x ⟨xa, ⟨xb, _⟩⟩ ↦ c_ab.trans_le <| mul_le_mul xa.le xb.le b0 (a0.trans xa.le)

Inequality for limit superior of product: $(\limsup u) \cdot (\liminf v) \leq \limsup (u \cdot v)$

Informal description

Let $f$ be a filter on a type $\beta$, and let $u, v : \beta \to \mathbb{R}$ be functions such that: 1. The set $\{x \mid 0 \leq u(x)\}$ is frequently in $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. The set $\{x \mid 0 \leq v(x)\}$ is eventually in $f$, 4. $v$ is bounded above under $f$ with respect to $\leq$. Then the following inequality holds: \[ (\limsup_{x \to f} u(x)) \cdot (\liminf_{x \to f} v(x)) \leq \limsup_{x \to f} (u(x) \cdot v(x)). \]

limsup_mul_le theorem

 (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
  (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) : limsup (u * v) f ≤ (limsup u f) * limsup v f

Full source

lemma limsup_mul_le (h₁ : ∃ᶠ x in f, 0 ≤ u x) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
    limsup (u * v) f ≤ (limsup u f) * limsup v f := by
  have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
  have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
  refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, h₃]
    with x x_a x_b v_0
  apply lt_of_le_of_lt _ c_ab
  rcases lt_or_ge (u x) 0 with u_0 | u_0
  · apply (mul_nonpos_of_nonpos_of_nonneg u_0.le v_0).trans
    exact mul_nonneg ((le_limsup_of_frequently_le h₁ h₂).trans a_u.le) (v_0.trans x_b.le)
  · exact mul_le_mul x_a.le x_b.le v_0 (u_0.trans x_a.le)

Inequality for limit superior of product of nonnegative functions

Informal description

Let $f$ be a filter on a type $\iota$, and let $u, v : \iota \to \mathbb{R}$ be functions such that: 1. The set $\{x \mid 0 \leq u(x)\}$ is frequently in $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. The set $\{x \mid 0 \leq v(x)\}$ is eventually in $f$, 4. $v$ is bounded above under $f$ with respect to $\leq$. Then the limit superior of the product function $u \cdot v$ along $f$ satisfies: \[ \limsup_{x \to f} (u(x) \cdot v(x)) \leq \left(\limsup_{x \to f} u(x)\right) \cdot \left(\limsup_{x \to f} v(x)\right). \]

le_liminf_mul theorem

 [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
  (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) : (liminf u f) * liminf v f ≤ liminf (u * v) f

Full source

lemma le_liminf_mul [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
    (liminf u f) * liminf v f ≤ liminf (u * v) f := by
  have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
  have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0
  apply mul_le_of_forall_lt_of_nonneg (le_liminf_of_le h₂.isCoboundedUnder_ge h₁)
    (le_liminf_of_le h ((h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0))
  intro a a0 au b b0 bv
  refine (le_liminf_iff h h').2 fun c c_ab ↦ ?_
  filter_upwards [eventually_lt_of_lt_liminf au (isBoundedUnder_of_eventually_ge h₁),
    eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)] with x xa xb
  exact c_ab.trans_le (mul_le_mul xa.le xb.le b0 (a0.trans xa.le))

Lower Bound on Limit Inferior of Product of Nonnegative Functions

Informal description

Let $f$ be a non-trivial filter on a type $\iota$, and let $u, v : \iota \to \mathbb{R}$ be functions such that: 1. $u(x) \geq 0$ holds eventually under $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. $v(x) \geq 0$ holds eventually under $f$, 4. $v$ is cobounded below under $f$ with respect to $\geq$. Then the product of the limit inferior of $u$ and the limit inferior of $v$ is less than or equal to the limit inferior of the product function $u \cdot v$, i.e., $$(\liminf_{f} u) \cdot (\liminf_{f} v) \leq \liminf_{f} (u \cdot v).$$

liminf_mul_le theorem

 [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
  (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) : liminf (u * v) f ≤ (limsup u f) * liminf v f

Full source

lemma liminf_mul_le [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
    liminf (u * v) f ≤ (limsup u f) * liminf v f := by
  have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
  have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
  refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_
  refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
  exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

Inequality for Limit Inferior of Product of Nonnegative Functions

Informal description

Let $\alpha$ be a linearly ordered type with a multiplication operation and a zero element, where left and right multiplication by nonnegative elements are monotone. Let $f$ be a non-trivial filter on a type $\iota$, and let $u, v : \iota \to \alpha$ be functions such that: 1. $u(x) \geq 0$ holds eventually under $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. $v(x) \geq 0$ holds eventually under $f$, 4. $v$ is cobounded below under $f$ with respect to $\geq$. Then the limit inferior of the product function $u \cdot v$ under $f$ is bounded above by the product of the limit superior of $u$ and the limit inferior of $v$ under $f$, i.e., \[ \liminf_{f} (u \cdot v) \leq (\limsup_{f} u) \cdot (\liminf_{f} v). \]

limsup_const_add theorem

 (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R)
  (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
  Filter.limsup (fun i ↦ c + f i) F = c + Filter.limsup f F

Full source

/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
lemma limsup_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
    [AddLeftMono R] (f : ι → R) (c : R)
    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
    Filter.limsup (fun i ↦ c + f i) F = c + Filter.limsup f F :=
  (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c + x)
    (fun _ _ h ↦ add_le_add_left h c) (continuous_add_left c).continuousAt bdd_above cobdd).symm

Limit Superior of Constant Plus Function: $\limsup (c + f) = c + \limsup f$

Informal description

Let $R$ be a topological space with a continuous addition operation that is left-monotone with respect to a partial order. Let $F$ be a non-trivial filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is bounded above under $F$ with respect to $\leq$, 2. $f$ is cobounded under $F$ with respect to $\leq$. Then for any constant $c \in R$, the limit superior of the function $i \mapsto c + f(i)$ under $F$ is equal to $c$ plus the limit superior of $f$ under $F$, i.e., $$\limsup_{F} (c + f) = c + \limsup_{F} f.$$

limsup_add_const theorem

 (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R)
  (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
  Filter.limsup (fun i ↦ f i + c) F = Filter.limsup f F + c

Full source

/-- `limsup (xᵢ + c) = (limsup xᵢ) + c`. -/
lemma limsup_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
    [AddRightMono R] (f : ι → R) (c : R)
    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
    Filter.limsup (fun i ↦ f i + c) F = Filter.limsup f F + c :=
  (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c)
    (fun _ _ h ↦ add_le_add_right h c) (continuous_add_right c).continuousAt bdd_above cobdd).symm

Limit Superior of Shifted Function: $\limsup (f + c) = (\limsup f) + c$

Informal description

Let $R$ be a topological space equipped with a continuous addition operation that is right-monotonic with respect to a partial order. Let $F$ be a non-trivial filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is bounded above under $F$ with respect to $\leq$, 2. $f$ is cobounded above under $F$ with respect to $\leq$. Then, for any constant $c \in R$, the limit superior of the function $(f + c)$ under $F$ equals the sum of the limit superior of $f$ under $F$ and $c$, i.e., \[ \limsup_{F} (f + c) = (\limsup_{F} f) + c. \]

liminf_const_add theorem

 (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R)
  (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
  Filter.liminf (fun i ↦ c + f i) F = c + Filter.liminf f F

Full source

/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
lemma liminf_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
    [AddLeftMono R] (f : ι → R) (c : R)
    (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
    Filter.liminf (fun i ↦ c + f i) F = c + Filter.liminf f F :=
  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c + x)
    (fun _ _ h ↦ add_le_add_left h c) (continuous_add_left c).continuousAt cobdd bdd_below).symm

Limit Inferior of a Constant Plus a Function: $\liminf (c + f_i) = c + \liminf f_i$

Informal description

Let $R$ be a topological space with a continuous addition operation that is left-monotone with respect to a partial order, and let $F$ be a non-trivial filter on a type $\iota$. For any function $f : \iota \to R$ and constant $c \in R$, if $f$ is bounded below and cobounded below under $F$, then the limit inferior of the function $i \mapsto c + f(i)$ along $F$ equals $c$ plus the limit inferior of $f$ along $F$, i.e., \[ \liminf_{i \to F} (c + f(i)) = c + \liminf_{i \to F} f(i). \]

liminf_add_const theorem

 (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R)
  (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
  Filter.liminf (fun i ↦ f i + c) F = Filter.liminf f F + c

Full source

/-- `liminf (xᵢ + c) = (liminf xᵢ) + c`. -/
lemma liminf_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
    [AddRightMono R] (f : ι → R) (c : R)
    (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
    Filter.liminf (fun i ↦ f i + c) F = Filter.liminf f F + c :=
  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c)
    (fun _ _ h ↦ add_le_add_right h c) (continuous_add_right c).continuousAt cobdd bdd_below).symm

Limit Inferior of Shifted Function: $\liminf (f_i + c) = (\liminf f_i) + c$

Informal description

Let $R$ be a conditionally complete linear order with an addition operation that is continuous and right-monotonic. Given a non-trivial filter $F$ on a type $\iota$ and a function $f : \iota \to R$ that is bounded below and cobounded under $\geq$ with respect to $F$, and a constant $c \in R$, we have \[ \liminf_{i \in F} (f(i) + c) = (\liminf_{i \in F} f(i)) + c. \]

limsup_const_sub theorem

 (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R)
  (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
  Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F

Full source

/-- `limsup (c - xᵢ) = c - liminf xᵢ`. -/
lemma limsup_const_sub (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
    [AddLeftMono R] (f : ι → R) (c : R)
    (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F := by
  rcases F.eq_or_neBot with rfl | _
  · simp only [liminf, limsInf, limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
    simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
    rcases cobdd with ⟨x, hx⟩
    refine (csInf_le ?_ (Set.mem_univ _)).antisymm
      (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))
    · refine ⟨x - x, mem_lowerBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, true_implies]
      exact tsub_le_iff_tsub_le.1 (hx (x - y))
    · refine ⟨x, mem_upperBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, hx y, implies_true]
  · exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt cobdd bdd_below).symm

Limit Superior of Constant Minus Function: $\limsup (c - f_i) = c - \liminf f_i$

Informal description

Let $R$ be an additive commutative semigroup with a subtraction operation and a partial order, equipped with the order topology. Assume that: 1. $R$ has continuous subtraction, 2. The ordered subtraction property holds: $a - b \leq c \leftrightarrow a \leq c + b$ for all $a, b, c \in R$, 3. Addition is left-monotone: $b_1 \leq b_2 \rightarrow a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in R$. Let $F$ be a filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is co-bounded below under $F$ (i.e., $\forall b, \exists^F i, b \leq f(i)$), 2. $f$ is bounded below under $F$ (i.e., $\exists b, \forall^F i, b \leq f(i)$). Then for any constant $c \in R$, the limit superior satisfies: \[ \limsup_{i \in F} (c - f(i)) = c - \liminf_{i \in F} f(i). \]

limsup_sub_const theorem

 (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R)
  (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
  Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c

Full source

/-- `limsup (xᵢ - c) = (limsup xᵢ) - c`. -/
lemma limsup_sub_const (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
    (f : ι → R) (c : R)
    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c := by
  rcases F.eq_or_neBot with rfl | _
  · have {a : R} : sInf Set.univ ≤ a := by
      apply csInf_le _ (Set.mem_univ a)
      simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
      rcases cobdd with ⟨x, hx⟩
      refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
      simp only [Set.mem_univ, hx y, implies_true]
    simp only [limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
    exact this.antisymm (tsub_le_iff_right.2 this)
  · apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm
    · exact fun _ _ h ↦ tsub_le_tsub_right h c
    · exact (continuous_sub_right c).continuousAt

Limit Superior of Shifted Function: $\limsup (f_i - c) = (\limsup f_i) - c$

Informal description

Let $R$ be an additive commutative semigroup with a subtraction operation and a partial order, equipped with the order topology. Assume that: 1. $R$ has continuous subtraction, 2. The ordered subtraction property holds: $a - b \leq c \leftrightarrow a \leq c + b$ for all $a, b, c \in R$. Let $F$ be a filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is bounded above under $F$ (i.e., $\exists b, \forall^F i, f(i) \leq b$), 2. $f$ is co-bounded below under $F$ (i.e., $\forall b, \exists^F i, b \leq f(i)$). Then for any constant $c \in R$, the limit superior satisfies: \[ \limsup_{i \in F} (f(i) - c) = (\limsup_{i \in F} f(i)) - c. \]

liminf_const_sub theorem

 (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R)
  (c : R) (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
  Filter.liminf (fun i ↦ c - f i) F = c - Filter.limsup f F

Full source

/-- `liminf (c - xᵢ) = c - limsup xᵢ`. -/
lemma liminf_const_sub (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
    [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R)
    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
    Filter.liminf (fun i ↦ c - f i) F = c - Filter.limsup f F :=
  (Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt bdd_above cobdd).symm

Limit inferior of constant minus function: $\liminf (c - f_i) = c - \limsup f_i$

Informal description

Let $R$ be an additive commutative semigroup with a subtraction operation and a partial order, equipped with the order topology. Assume that: 1. $R$ has continuous subtraction, 2. The ordered subtraction property holds: $a - b \leq c \leftrightarrow a \leq c + b$ for all $a, b, c \in R$, 3. Addition is left-monotone: $b_1 \leq b_2 \rightarrow a + b_1 \leq a + b_2$ for all $a, b_1, b_2 \in R$. Let $F$ be a non-trivial filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is bounded above under $F$ (i.e., $\exists b, \forall^F i, f(i) \leq b$), 2. $f$ is co-bounded below under $F$ (i.e., $\forall b, \exists^F i, b \leq f(i)$). Then for any constant $c \in R$, the limit inferior satisfies: \[ \liminf_{i \in F} (c - f(i)) = c - \limsup_{i \in F} f(i). \]

liminf_sub_const theorem

 (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R)
  (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
  Filter.liminf (fun i ↦ f i - c) F = Filter.liminf f F - c

Full source

/-- `liminf (xᵢ - c) = (liminf xᵢ) - c`. -/
lemma liminf_sub_const (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
    [OrderedSub R] (f : ι → R) (c : R)
    (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
    Filter.liminf (fun i ↦ f i - c) F = Filter.liminf f F - c :=
  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt cobdd bdd_below).symm

Limit inferior of shifted function: $\liminf (f_i - c) = (\liminf f_i) - c$

Informal description

Let $R$ be an additive commutative semigroup with a subtraction operation and a partial order, equipped with the order topology. Assume that: 1. $R$ has continuous subtraction, 2. The ordered subtraction property holds: $a - b \leq c \leftrightarrow a \leq c + b$ for all $a, b, c \in R$. Let $F$ be a non-trivial filter on a type $\iota$, and let $f : \iota \to R$ be a function such that: 1. $f$ is bounded below under $F$ (i.e., $\exists b, \forall^F i, b \leq f(i)$), 2. $f$ is co-bounded above under $F$ (i.e., $\forall b, \exists^F i, f(i) \leq b$). Then for any constant $c \in R$, the limit inferior satisfies: \[ \liminf_{i \in F} (f(i) - c) = \left(\liminf_{i \in F} f(i)\right) - c. \]

Mathlib.Topology.Algebra.Order.LiminfLimsup

Main declarations

Implementation notes