# mathlibdocumentation

order.liminf_limsup

# liminfs and limsups of functions and filters

Defines the Liminf/Limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.

We define f.Limsup (f.Liminf) where f is a filter taking values in a conditionally complete lattice. f.Limsup is the smallest element a such that, eventually, u ≤ a (and vice versa for f.Liminf). To work with the Limsup along a function u use (f.map u).Limsup.

Usually, one defines the Limsup as Inf (Sup s) where the Inf is taken over all sets in the filter. For instance, in ℕ along a function u, this is Inf_n (Sup_{k ≥ n} u k) (and the latter quantity decreases with n, so this is in fact a limit.). There is however a difficulty: it is well possible that u is not bounded on the whole space, only eventually (think of Limsup (λx, 1/x) on ℝ. Then there is no guarantee that the quantity above really decreases (the value of the Sup beforehand is not really well defined, as one can not use ∞), so that the Inf could be anything. So one can not use this Inf Sup ... definition in conditionally complete lattices, and one has to use a less tractable definition.

In conditionally complete lattices, the definition is only useful for filters which are eventually bounded above (otherwise, the Limsup would morally be +∞, which does not belong to the space) and which are frequently bounded below (otherwise, the Limsup would morally be -∞, which is not in the space either). We start with definitions of these concepts for arbitrary filters, before turning to the definitions of Limsup and Liminf.

In complete lattices, however, it coincides with the Inf Sup definition.

def filter.is_bounded {α : Type u_1} :
(α → α → Prop) → Prop

f.is_bounded (≺): the filter f is eventually bounded w.r.t. the relation ≺, i.e. eventually, it is bounded by some uniform bound. r will be usually instantiated with ≤ or ≥.

Equations
• = ∃ (b : α), ∀ᶠ (x : α) in f, r x b
def filter.is_bounded_under {α : Type u_1} {β : Type u_2} :
(α → α → Prop)(β → α) → Prop

f.is_bounded_under (≺) u: the image of the filter f under u is eventually bounded w.r.t. the relation ≺, i.e. eventually, it is bounded by some uniform bound.

Equations
• = f)
theorem filter.is_bounded_iff {α : Type u_1} {r : α → α → Prop} {f : filter α} :
∃ (s : set α) (H : s f.sets) (b : α), s {x : α | r x b}

f is eventually bounded if and only if, there exists an admissible set on which it is bounded.

theorem filter.is_bounded_under_of {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : filter β} {u : β → α} :
(∃ (b : α), ∀ (x : β), r (u x) b)

A bounded function u is in particular eventually bounded.

theorem filter.is_bounded_bot {α : Type u_1} {r : α → α → Prop} :

theorem filter.is_bounded_top {α : Type u_1} {r : α → α → Prop} :
∃ (t : α), ∀ (x : α), r x t

theorem filter.is_bounded_principal {α : Type u_1} {r : α → α → Prop} (s : set α) :
(𝓟 s) ∃ (t : α), ∀ (x : α), x sr x t

theorem filter.is_bounded_sup {α : Type u_1} {r : α → α → Prop} {f g : filter α} [ r] :
(∀ (b₁ b₂ : α), ∃ (b : α), r b₁ b r b₂ b) (f g)

theorem filter.is_bounded.mono {α : Type u_1} {r : α → α → Prop} {f g : filter α} :
f g

theorem filter.is_bounded_under.mono {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f g : filter β} {u : β → α} :
f g

theorem filter.is_bounded.is_bounded_under {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : filter α} {q : β → β → Prop} {u : α → β} :
(∀ (a₀ a₁ : α), r a₀ a₁q (u a₀) (u a₁))

def filter.is_cobounded {α : Type u_1} :
(α → α → Prop) → Prop

is_cobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥.

There is a subtlety in this definition: we want f.is_cobounded to hold for any f in the case of complete lattices. This will be relevant to deduce theorems on complete lattices from their versions on conditionally complete lattices with additional assumptions. We have to be careful in the edge case of the trivial filter containing the empty set: the other natural definition ¬ ∀ a, ∀ᶠ n in f, a ≤ n would not work as well in this case.

Equations
• = ∃ (b : α), ∀ (a : α), (∀ᶠ (x : α) in f, r x a)r b a
def filter.is_cobounded_under {α : Type u_1} {β : Type u_2} :
(α → α → Prop)(β → α) → Prop

is_cobounded_under (≺) f u states that the image of the filter f under the map u does not tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥.

Equations
• = f)
theorem filter.is_cobounded.mk {α : Type u_1} {r : α → α → Prop} {f : filter α} [ r] (a : α) :
(∀ (s : set α), s f(∃ (x : α) (H : x s), r a x))

To check that a filter is frequently bounded, it suffices to have a witness which bounds f at some point for every admissible set.

This is only an implication, as the other direction is wrong for the trivial filter.

theorem filter.is_bounded.is_cobounded_flip {α : Type u_1} {r : α → α → Prop} {f : filter α} [ r] [f.ne_bot] :
f

A filter which is eventually bounded is in particular frequently bounded (in the opposite direction). At least if the filter is not trivial.

theorem filter.is_cobounded_bot {α : Type u_1} {r : α → α → Prop} :
∃ (b : α), ∀ (x : α), r b x

theorem filter.is_cobounded_top {α : Type u_1} {r : α → α → Prop} :

theorem filter.is_cobounded_principal {α : Type u_1} {r : α → α → Prop} (s : set α) :
(𝓟 s) ∃ (b : α), ∀ (a : α), (∀ (x : α), x sr x a)r b a

theorem filter.is_cobounded.mono {α : Type u_1} {r : α → α → Prop} {f g : filter α} :
f g

theorem filter.is_cobounded_le_of_bot {α : Type u_1} [order_bot α] {f : filter α} :

theorem filter.is_cobounded_ge_of_top {α : Type u_1} [order_top α] {f : filter α} :

theorem filter.is_bounded_le_of_top {α : Type u_1} [order_top α] {f : filter α} :

theorem filter.is_bounded_ge_of_bot {α : Type u_1} [order_bot α] {f : filter α} :

theorem filter.is_bounded_under_sup {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β → α} :
(λ (a : β), u a v a)

theorem filter.is_bounded_under_inf {α : Type u_1} {β : Type u_2} {f : filter β} {u v : β → α} :
(λ (a : β), u a v a)

Filters are automatically bounded or cobounded in complete lattices. To use the same statements in complete and conditionally complete lattices but let automation fill automatically the boundedness proofs in complete lattices, we use the tactic is_bounded_default in the statements, in the form (hf : f.is_bounded (≥) . is_bounded_default).

def filter.Limsup {α : Type u_1}  :
→ α

The Limsup of a filter f is the infimum of the a such that, eventually for f, holds x ≤ a.

Equations
def filter.Liminf {α : Type u_1}  :
→ α

The Liminf of a filter f is the supremum of the a such that, eventually for f, holds x ≥ a.

Equations
def filter.limsup {α : Type u_1} {β : Type u_2}  :
(β → α) → α

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.

Equations
def filter.liminf {α : Type u_1} {β : Type u_2}  :
(β → α) → α

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.

Equations
theorem filter.limsup_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β → α} :
f.limsup u = Inf {a : α | ∀ᶠ (n : β) in f, u n a}

theorem filter.liminf_eq {α : Type u_1} {β : Type u_2} {f : filter β} {u : β → α} :
f.liminf u = Sup {a : α | ∀ᶠ (n : β) in f, a u n}

theorem filter.Limsup_le_of_le {α : Type u_1} {f : filter α} {a : α} :
. "is_bounded_default")(∀ᶠ (n : α) in f, n a)f.Limsup a

theorem filter.le_Liminf_of_le {α : Type u_1} {f : filter α} {a : α} :
. "is_bounded_default")(∀ᶠ (n : α) in f, a n)a f.Liminf

theorem filter.le_Limsup_of_le {α : Type u_1} {f : filter α} {a : α} :
. "is_bounded_default")(∀ (b : α), (∀ᶠ (n : α) in f, n b)a b)a f.Limsup

theorem filter.Liminf_le_of_le {α : Type u_1} {f : filter α} {a : α} :
. "is_bounded_default")(∀ (b : α), (∀ᶠ (n : α) in f, b n)b a)f.Liminf a

theorem filter.Liminf_le_Limsup {α : Type u_1} {f : filter α} [f.ne_bot] :
. "is_bounded_default") . "is_bounded_default")f.Liminf f.Limsup

theorem filter.Liminf_le_Liminf {α : Type u_1} {f g : filter α} :
. "is_bounded_default") . "is_bounded_default")(∀ (a : α), (∀ᶠ (n : α) in f, a n)(∀ᶠ (n : α) in g, a n))f.Liminf g.Liminf

theorem filter.Limsup_le_Limsup {α : Type u_1} {f g : filter α} :
. "is_bounded_default") . "is_bounded_default")(∀ (a : α), (∀ᶠ (n : α) in g, n a)(∀ᶠ (n : α) in f, n a))f.Limsup g.Limsup

theorem filter.Limsup_le_Limsup_of_le {α : Type u_1} {f g : filter α} :
f g . "is_bounded_default") . "is_bounded_default")f.Limsup g.Limsup

theorem filter.Liminf_le_Liminf_of_le {α : Type u_1} {f g : filter α} :
g f . "is_bounded_default") . "is_bounded_default")f.Liminf g.Liminf

theorem filter.limsup_le_limsup {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α → β} :
u ≤ᶠ[f] v . "is_bounded_default") . "is_bounded_default")f.limsup u f.limsup v

theorem filter.liminf_le_liminf {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α → β} :
(∀ᶠ (a : α) in f, u a v a) . "is_bounded_default") . "is_bounded_default")f.liminf u f.liminf v

theorem filter.Limsup_principal {α : Type u_1} {s : set α} :
s.nonempty(𝓟 s).Limsup = Sup s

theorem filter.Liminf_principal {α : Type u_1} {s : set α} :
s.nonempty(𝓟 s).Liminf = Inf s

theorem filter.limsup_congr {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α → β} :
(∀ᶠ (a : α) in f, u a = v a)f.limsup u = f.limsup v

theorem filter.liminf_congr {β : Type u_2} {α : Type u_1} {f : filter α} {u v : α → β} :
(∀ᶠ (a : α) in f, u a = v a)f.liminf u = f.liminf v

theorem filter.limsup_const {β : Type u_2} {α : Type u_1} {f : filter α} [f.ne_bot] (b : β) :
f.limsup (λ (x : α), b) = b

theorem filter.liminf_const {β : Type u_2} {α : Type u_1} {f : filter α} [f.ne_bot] (b : β) :
f.liminf (λ (x : α), b) = b

@[simp]
theorem filter.Limsup_bot {α : Type u_1}  :

@[simp]
theorem filter.Liminf_bot {α : Type u_1}  :

@[simp]
theorem filter.Limsup_top {α : Type u_1}  :

@[simp]
theorem filter.Liminf_top {α : Type u_1}  :

theorem filter.liminf_le_limsup {α : Type u_1} {β : Type u_2} {f : filter β} [f.ne_bot] {u : β → α} :
f.liminf u f.limsup u

theorem filter.has_basis.Limsup_eq_infi_Sup {α : Type u_1} {ι : Type u_2} {p : ι → Prop} {s : ι → set α} {f : filter α} :
f.has_basis p s(f.Limsup = ⨅ (i : ι) (hi : p i), Sup (s i))

theorem filter.has_basis.Liminf_eq_supr_Inf {α : Type u_1} {ι : Type u_3} {p : ι → Prop} {s : ι → set α} {f : filter α} :
f.has_basis p s(f.Liminf = ⨆ (i : ι) (hi : p i), Inf (s i))

theorem filter.Limsup_eq_infi_Sup {α : Type u_1} {f : filter α} :
f.Limsup = ⨅ (s : set α) (H : s f), Sup s

theorem filter.Liminf_eq_supr_Inf {α : Type u_1} {f : filter α} :
f.Liminf = ⨆ (s : set α) (H : s f), Inf s

theorem filter.limsup_eq_infi_supr {α : Type u_1} {β : Type u_2} {f : filter β} {u : β → α} :
f.limsup u = ⨅ (s : set β) (H : s f), ⨆ (a : β) (H : a s), u a

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 filter.limsup_eq_infi_supr_of_nat {α : Type u_1} {u : → α} :
= ⨅ (n : ), ⨆ (i : ) (H : i n), u i

theorem filter.limsup_eq_infi_supr_of_nat' {α : Type u_1} {u : → α} :
= ⨅ (n : ), ⨆ (i : ), u (i + n)

theorem filter.has_basis.limsup_eq_infi_supr {α : Type u_1} {β : Type u_2} {ι : Type u_3} {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α} :
f.has_basis p s(f.limsup u = ⨅ (i : ι) (hi : p i), ⨆ (a : β) (H : a s i), u a)

theorem filter.liminf_eq_supr_infi {α : Type u_1} {β : Type u_2} {f : filter β} {u : β → α} :
f.liminf u = ⨆ (s : set β) (H : s f), ⨅ (a : β) (H : a s), u a

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 filter.liminf_eq_supr_infi_of_nat {α : Type u_1} {u : → α} :
= ⨆ (n : ), ⨅ (i : ) (H : i n), u i

theorem filter.liminf_eq_supr_infi_of_nat' {α : Type u_1} {u : → α} :
= ⨆ (n : ), ⨅ (i : ), u (i + n)

theorem filter.has_basis.liminf_eq_supr_infi {α : Type u_1} {β : Type u_2} {ι : Type u_3} {p : ι → Prop} {s : ι → set β} {f : filter β} {u : β → α} :
f.has_basis p s(f.liminf u = ⨆ (i : ι) (hi : p i), ⨅ (a : β) (H : a s i), u a)

theorem filter.eventually_lt_of_lt_liminf {α : Type u_1} {β : Type u_2} {f : filter α} {u : α → β} {b : β} :
b < f.liminf u . "is_bounded_default")(∀ᶠ (a : α) in f, b < u a)

theorem filter.eventually_lt_of_limsup_lt {α : Type u_1} {β : Type u_2} {f : filter α} {u : α → β} {b : β} :
f.limsup u < b . "is_bounded_default")(∀ᶠ (a : α) in f, u a < b)