# 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 limsSup f (limsInf f) where f is a filter taking values in a conditionally complete lattice. limsSup f is the smallest element a such that, eventually, u ≤ a (and vice versa for limsInf f). To work with the Limsup along a function u use limsSup (map u f).

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 (fun 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.IsBounded {α : Type u_1} (r : ααProp) (f : ) :

f.IsBounded (≺): 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
Instances For
def Filter.IsBoundedUnder {α : Type u_1} {β : Type u_2} (r : ααProp) (f : ) (u : βα) :

f.IsBoundedUnder (≺) 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
Instances For
theorem Filter.isBounded_iff {α : Type u_1} {r : ααProp} {f : } :
sf.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.isBoundedUnder_of {α : Type u_1} {β : Type u_2} {r : ααProp} {f : } {u : βα} :
(∃ (b : α), ∀ (x : β), r (u x) b)

A bounded function u is in particular eventually bounded.

theorem Filter.isBounded_bot {α : Type u_1} {r : ααProp} :
theorem Filter.isBounded_top {α : Type u_1} {r : ααProp} :
∃ (t : α), ∀ (x : α), r x t
theorem Filter.isBounded_principal {α : Type u_1} {r : ααProp} (s : Set α) :
∃ (t : α), xs, r x t
theorem Filter.isBounded_sup {α : Type u_1} {r : ααProp} {f : } {g : } [IsTrans α r] [] :
Filter.IsBounded r (f g)
theorem Filter.IsBounded.mono {α : Type u_1} {r : ααProp} {f : } {g : } (h : f g) :
theorem Filter.IsBoundedUnder.mono {α : Type u_1} {β : Type u_2} {r : ααProp} {f : } {g : } {u : βα} (h : f g) :
theorem Filter.IsBoundedUnder.mono_le {α : Type u_1} {β : Type u_2} [] {l : } {u : αβ} {v : αβ} (hu : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l u) (hv : v ≤ᶠ[l] u) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l v
theorem Filter.IsBoundedUnder.mono_ge {α : Type u_1} {β : Type u_2} [] {l : } {u : αβ} {v : αβ} (hu : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l u) (hv : u ≤ᶠ[l] v) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l v
theorem Filter.isBoundedUnder_const {α : Type u_1} {β : Type u_2} {r : ααProp} [IsRefl α r] {l : } {a : α} :
Filter.IsBoundedUnder r l fun (x : β) => a
theorem Filter.IsBounded.isBoundedUnder {α : Type u_1} {β : Type u_2} {r : ααProp} {f : } {q : ββProp} {u : αβ} (hu : ∀ (a₀ a₁ : α), r a₀ a₁q (u a₀) (u a₁)) :
theorem Filter.IsBoundedUnder.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : ααProp} {l : } {q : ββProp} {u : γα} {v : αβ} (hv : ∀ (a₀ a₁ : α), r a₀ a₁q (v a₀) (v a₁)) :
Filter.IsBoundedUnder q l (v u)
theorem BddAbove.isBoundedUnder {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u

A bounded above function u is in particular eventually bounded above.

theorem BddBelow.isBoundedUnder {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u

A bounded below function u is in particular eventually bounded below.

theorem Monotone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {l : } {u : γα} {v : αβ} (hv : ) (hl : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l (v u)
theorem Monotone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {l : } {u : γα} {v : αβ} (hv : ) (hl : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l (v u)
theorem Antitone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {l : } {u : γα} {v : αβ} (hv : ) (hl : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l (v u)
theorem Antitone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {l : } {u : γα} {v : αβ} (hv : ) (hl : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l (v u)
theorem Filter.not_isBoundedUnder_of_tendsto_atTop {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {l : } [l.NeBot] (hf : Filter.Tendsto f l Filter.atTop) :
¬Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem Filter.not_isBoundedUnder_of_tendsto_atBot {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {l : } [l.NeBot] (hf : Filter.Tendsto f l Filter.atBot) :
¬Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite {α : Type u_1} {β : Type u_2} [] [IsDirected β fun (x x_1 : β) => x x_1] {f : αβ} (hf : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) Filter.cofinite f) :
theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite {α : Type u_1} {β : Type u_2} [] [IsDirected β fun (x x_1 : β) => x x_1] {f : αβ} (hf : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) Filter.cofinite f) :
theorem Filter.IsBoundedUnder.bddAbove_range {β : Type u_2} [] [IsDirected β fun (x x_1 : β) => x x_1] {f : β} (hf : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) Filter.atTop f) :
theorem Filter.IsBoundedUnder.bddBelow_range {β : Type u_2} [] [IsDirected β fun (x x_1 : β) => x x_1] {f : β} (hf : Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) Filter.atTop f) :
def Filter.IsCobounded {α : Type u_1} (r : ααProp) (f : ) :

IsCobounded (≺) 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.IsCobounded 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
Instances For
def Filter.IsCoboundedUnder {α : Type u_1} {β : Type u_2} (r : ααProp) (f : ) (u : βα) :

IsCoboundedUnder (≺) 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
Instances For
theorem Filter.IsCobounded.mk {α : Type u_1} {r : ααProp} {f : } [IsTrans α r] (a : α) (h : sf, xs, 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.IsBounded.isCobounded_flip {α : Type u_1} {r : ααProp} {f : } [IsTrans α r] [f.NeBot] :

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.IsBounded.isCobounded_ge {α : Type u_1} {f : } [] [f.NeBot] (h : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) f
theorem Filter.IsBounded.isCobounded_le {α : Type u_1} {f : } [] [f.NeBot] (h : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) f
theorem Filter.IsBoundedUnder.isCoboundedUnder_flip {α : Type u_1} {γ : Type u_3} {r : ααProp} {u : γα} {l : } [IsTrans α r] [l.NeBot] (h : ) :
theorem Filter.IsBoundedUnder.isCoboundedUnder_le {α : Type u_1} {γ : Type u_3} {u : γα} {l : } [] [l.NeBot] (h : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l u
theorem Filter.IsBoundedUnder.isCoboundedUnder_ge {α : Type u_1} {γ : Type u_3} {u : γα} {l : } [] [l.NeBot] (h : Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l u
theorem Filter.isCoboundedUnder_le_of_eventually_le {α : Type u_1} {ι : Type u_4} [] (l : ) [l.NeBot] {f : ια} {x : α} (hf : ∀ᶠ (i : ι) in l, x f i) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l f
theorem Filter.isCoboundedUnder_ge_of_eventually_le {α : Type u_1} {ι : Type u_4} [] (l : ) [l.NeBot] {f : ια} {x : α} (hf : ∀ᶠ (i : ι) in l, f i x) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l f
theorem Filter.isCoboundedUnder_le_of_le {α : Type u_1} {ι : Type u_4} [] (l : ) [l.NeBot] {f : ια} {x : α} (hf : ∀ (i : ι), x f i) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l f
theorem Filter.isCoboundedUnder_ge_of_le {α : Type u_1} {ι : Type u_4} [] (l : ) [l.NeBot] {f : ια} {x : α} (hf : ∀ (i : ι), f i x) :
Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) l f
theorem Filter.isCobounded_bot {α : Type u_1} {r : ααProp} :
∃ (b : α), ∀ (x : α), r b x
theorem Filter.isCobounded_top {α : Type u_1} {r : ααProp} :
theorem Filter.isCobounded_principal {α : Type u_1} {r : ααProp} (s : Set α) :
∃ (b : α), ∀ (a : α), (xs, r x a)r b a
theorem Filter.IsCobounded.mono {α : Type u_1} {r : ααProp} {f : } {g : } (h : f g) :
theorem Filter.isBounded_le_atBot {α : Type u_1} [] [] :
Filter.IsBounded (fun (x x_1 : α) => x x_1) Filter.atBot
theorem Filter.isBounded_ge_atTop {α : Type u_1} [] [] :
Filter.IsBounded (fun (x x_1 : α) => x x_1) Filter.atTop
theorem Filter.Tendsto.isBoundedUnder_le_atBot {α : Type u_1} {β : Type u_2} [] [] {f : } {u : βα} (h : Filter.Tendsto u f Filter.atBot) :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
theorem Filter.Tendsto.isBoundedUnder_ge_atTop {α : Type u_1} {β : Type u_2} [] [] {f : } {u : βα} (h : Filter.Tendsto u f Filter.atTop) :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u
theorem Filter.bddAbove_range_of_tendsto_atTop_atBot {α : Type u_1} [] [] [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (hx : Filter.Tendsto u Filter.atTop Filter.atBot) :
theorem Filter.bddBelow_range_of_tendsto_atTop_atTop {α : Type u_1} [] [] [IsDirected α fun (x x_1 : α) => x x_1] {u : α} (hx : Filter.Tendsto u Filter.atTop Filter.atTop) :
theorem Filter.isCobounded_le_of_bot {α : Type u_1} [] [] {f : } :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) f
theorem Filter.isCobounded_ge_of_top {α : Type u_1} [] [] {f : } :
Filter.IsCobounded (fun (x x_1 : α) => x x_1) f
theorem Filter.isBounded_le_of_top {α : Type u_1} [] [] {f : } :
Filter.IsBounded (fun (x x_1 : α) => x x_1) f
theorem Filter.isBounded_ge_of_bot {α : Type u_1} [] [] {f : } :
Filter.IsBounded (fun (x x_1 : α) => x x_1) f
@[simp]
theorem OrderIso.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (e : α ≃o β) {l : } {u : γα} :
(Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l fun (x : γ) => e (u x)) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
@[simp]
theorem OrderIso.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (e : α ≃o β) {l : } {u : γα} :
(Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l fun (x : γ) => e (u x)) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
@[simp]
theorem Filter.isBoundedUnder_le_neg {α : Type u_1} {β : Type u_2} {l : } {u : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l fun (x : β) => -u x) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
@[simp]
theorem Filter.isBoundedUnder_le_inv {α : Type u_1} {β : Type u_2} [] {l : } {u : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l fun (x : β) => (u x)⁻¹) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
@[simp]
theorem Filter.isBoundedUnder_ge_neg {α : Type u_1} {β : Type u_2} {l : } {u : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l fun (x : β) => -u x) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
@[simp]
theorem Filter.isBoundedUnder_ge_inv {α : Type u_1} {β : Type u_2} [] {l : } {u : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l fun (x : β) => (u x)⁻¹) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) l u
theorem Filter.IsBoundedUnder.sup {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} {v : βα} :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f uFilter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f vFilter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f fun (a : β) => u a v a
@[simp]
theorem Filter.isBoundedUnder_le_sup {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} {v : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f fun (a : β) => u a v a) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f v
theorem Filter.IsBoundedUnder.inf {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} {v : βα} :
Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f uFilter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f vFilter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f fun (a : β) => u a v a
@[simp]
theorem Filter.isBoundedUnder_ge_inf {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} {v : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f fun (a : β) => u a v a) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f v
theorem Filter.isBoundedUnder_le_abs {α : Type u_1} {β : Type u_2} {f : } {u : βα} :
(Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f fun (a : β) => |u a|) Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u

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 isBoundedDefault in the statements, in the form (hf : f.IsBounded (≥) := by isBoundedDefault).

Equations
Instances For
def Filter.limsSup {α : Type u_1} (f : ) :
α

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

Equations
• f.limsSup = sInf {a : α | ∀ᶠ (n : α) in f, n a}
Instances For
def Filter.limsInf {α : Type u_1} (f : ) :
α

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

Equations
• f.limsInf = sSup {a : α | ∀ᶠ (n : α) in f, a n}
Instances For
def Filter.limsup {α : Type u_1} {β : Type u_2} (u : βα) (f : ) :
α

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
• = ().limsSup
Instances For
def Filter.liminf {α : Type u_1} {β : Type u_2} (u : βα) (f : ) :
α

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
• = ().limsInf
Instances For
def Filter.blimsup {α : Type u_1} {β : Type u_2} (u : βα) (f : ) (p : βProp) :
α

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.

Equations
• = sInf {a : α | ∀ᶠ (x : β) in f, p xu x a}
Instances For
def Filter.bliminf {α : Type u_1} {β : Type u_2} (u : βα) (f : ) (p : βProp) :
α

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.

Equations
• = sSup {a : α | ∀ᶠ (x : β) in f, p xa u x}
Instances For
theorem Filter.limsup_eq {α : Type u_1} {β : Type u_2} {f : } {u : βα} :
= sInf {a : α | ∀ᶠ (n : β) in f, u n a}
theorem Filter.liminf_eq {α : Type u_1} {β : Type u_2} {f : } {u : βα} :
= sSup {a : α | ∀ᶠ (n : β) in f, a u n}
theorem Filter.blimsup_eq {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= sInf {a : α | ∀ᶠ (x : β) in f, p xu x a}
theorem Filter.bliminf_eq {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= sSup {a : α | ∀ᶠ (x : β) in f, p xa u x}
theorem Filter.liminf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (u : βα) (v : γβ) (f : ) :
theorem Filter.limsup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (u : βα) (v : γβ) (f : ) :
@[simp]
theorem Filter.blimsup_true {α : Type u_1} {β : Type u_2} (f : ) (u : βα) :
(Filter.blimsup u f fun (x : β) => True) =
@[simp]
theorem Filter.bliminf_true {α : Type u_1} {β : Type u_2} (f : ) (u : βα) :
(Filter.bliminf u f fun (x : β) => True) =
theorem Filter.blimsup_eq_limsup {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= Filter.limsup u (f Filter.principal {x : β | p x})
theorem Filter.bliminf_eq_liminf {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= Filter.liminf u (f Filter.principal {x : β | p x})
theorem Filter.blimsup_eq_limsup_subtype {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= Filter.limsup (u Subtype.val) (Filter.comap Subtype.val f)
theorem Filter.bliminf_eq_liminf_subtype {α : Type u_1} {β : Type u_2} {f : } {u : βα} {p : βProp} :
= Filter.liminf (u Subtype.val) (Filter.comap Subtype.val f)
theorem Filter.limsSup_le_of_le {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : ∀ᶠ (n : α) in f, n a) :
f.limsSup a
theorem Filter.le_limsInf_of_le {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : ∀ᶠ (n : α) in f, a n) :
a f.limsInf
theorem Filter.limsup_le_of_le {α : Type u_1} {β : Type u_2} {f : } {u : βα} {a : α} (hf : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h : ∀ᶠ (n : β) in f, u n a) :
a
theorem Filter.le_liminf_of_le {α : Type u_1} {β : Type u_2} {f : } {u : βα} {a : α} (hf : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h : ∀ᶠ (n : β) in f, a u n) :
a
theorem Filter.le_limsSup_of_le {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : ∀ (b : α), (∀ᶠ (n : α) in f, n b)a b) :
a f.limsSup
theorem Filter.limsInf_le_of_le {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : ∀ (b : α), (∀ᶠ (n : α) in f, b n)b a) :
f.limsInf a
theorem Filter.le_limsup_of_le {α : Type u_1} {β : Type u_2} {f : } {u : βα} {a : α} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h : ∀ (b : α), (∀ᶠ (n : β) in f, u n b)a b) :
a
theorem Filter.liminf_le_of_le {α : Type u_1} {β : Type u_2} {f : } {u : βα} {a : α} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h : ∀ (b : α), (∀ᶠ (n : β) in f, b u n)b a) :
a
theorem Filter.limsInf_le_limsSup {α : Type u_1} {f : } [f.NeBot] (h₁ : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h₂ : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) :
f.limsInf f.limsSup
theorem Filter.liminf_le_limsup {α : Type u_1} {β : Type u_2} {f : } [f.NeBot] {u : βα} (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x x_1) f u) _auto✝) :
theorem Filter.limsSup_le_limsSup {α : Type u_1} {f : } {g : } (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (hg : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) g) _auto✝) (h : ∀ (a : α), (∀ᶠ (n : α) in g, n a)∀ᶠ (n : α) in f, n a) :
f.limsSup g.limsSup
theorem Filter.limsInf_le_limsInf {α : Type u_1} {f : } {g : } (hf : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) (hg : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) g) _auto✝) (h : ∀ (a : α), (∀ᶠ (n : α) in f, a n)∀ᶠ (n : α) in g, a n) :
f.limsInf g.limsInf
theorem Filter.limsup_le_limsup {β : Type u_2} {α : Type u_6} {f : } {u : αβ} {v : αβ} (h : u ≤ᶠ[f] v) (hu : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hv : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) :
theorem Filter.liminf_le_liminf {β : Type u_2} {α : Type u_6} {f : } {u : αβ} {v : αβ} (h : ∀ᶠ (a : α) in f, u a v a) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hv : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) :
theorem Filter.limsSup_le_limsSup_of_le {α : Type u_1} {f : } {g : } (h : f g) (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (hg : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) g) _auto✝) :
f.limsSup g.limsSup
theorem Filter.limsInf_le_limsInf_of_le {α : Type u_1} {f : } {g : } (h : g f) (hf : autoParam (Filter.IsBounded (fun (x x_1 : α) => x x_1) f) _auto✝) (hg : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) g) _auto✝) :
f.limsInf g.limsInf
theorem Filter.limsup_le_limsup_of_le {α : Type u_6} {β : Type u_7} {f : } {g : } (h : f g) {u : αβ} (hf : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hg : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) g u) _auto✝) :
theorem Filter.liminf_le_liminf_of_le {α : Type u_6} {β : Type u_7} {f : } {g : } (h : g f) {u : αβ} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hg : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) g u) _auto✝) :
theorem Filter.limsSup_principal {α : Type u_1} {s : Set α} (h : ) (hs : s.Nonempty) :
().limsSup = sSup s
theorem Filter.limsInf_principal {α : Type u_1} {s : Set α} (h : ) (hs : s.Nonempty) :
().limsInf = sInf s
theorem Filter.limsup_congr {β : Type u_2} {α : Type u_6} {f : } {u : αβ} {v : αβ} (h : ∀ᶠ (a : α) in f, u a = v a) :
=
theorem Filter.blimsup_congr {α : Type u_1} {β : Type u_2} {f : } {u : βα} {v : βα} {p : βProp} (h : ∀ᶠ (a : β) in f, p au a = v a) :
=
theorem Filter.bliminf_congr {α : Type u_1} {β : Type u_2} {f : } {u : βα} {v : βα} {p : βProp} (h : ∀ᶠ (a : β) in f, p au a = v a) :
=
theorem Filter.liminf_congr {β : Type u_2} {α : Type u_6} {f : } {u : αβ} {v : αβ} (h : ∀ᶠ (a : α) in f, u a = v a) :
=
@[simp]
theorem Filter.limsup_const {β : Type u_2} {α : Type u_6} {f : } [f.NeBot] (b : β) :
Filter.limsup (fun (x : α) => b) f = b
@[simp]
theorem Filter.liminf_const {β : Type u_2} {α : Type u_6} {f : } [f.NeBot] (b : β) :
Filter.liminf (fun (x : α) => b) f = b
theorem Filter.HasBasis.liminf_eq_sSup_iUnion_iInter {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {f : ια} {v : } {p : ι'Prop} {s : ι'Set ι} (hv : v.HasBasis p s) :
= sSup (⋃ (j : ), ⋂ (i : (s j)), Set.Iic (f i))
theorem Filter.HasBasis.liminf_eq_sSup_univ_of_empty {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {f : ια} {v : } {p : ι'Prop} {s : ι'Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ) :
= sSup Set.univ
theorem Filter.HasBasis.limsup_eq_sInf_iUnion_iInter {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {f : ια} {v : } {p : ι'Prop} {s : ι'Set ι} (hv : v.HasBasis p s) :
= sInf (⋃ (j : ), ⋂ (i : (s j)), Set.Ici (f i))
theorem Filter.HasBasis.limsup_eq_sInf_univ_of_empty {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {f : ια} {v : } {p : ι'Prop} {s : ι'Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ) :
= sInf Set.univ
@[simp]
theorem Filter.liminf_nat_add {α : Type u_1} (f : α) (k : ) :
Filter.liminf (fun (i : ) => f (i + k)) Filter.atTop = Filter.liminf f Filter.atTop
@[simp]
theorem Filter.limsup_nat_add {α : Type u_1} (f : α) (k : ) :
Filter.limsup (fun (i : ) => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop
@[simp]
theorem Filter.limsSup_bot {α : Type u_1} [] :
.limsSup =
@[simp]
theorem Filter.limsup_bot {α : Type u_1} {β : Type u_2} [] (f : βα) :
@[simp]
theorem Filter.limsInf_bot {α : Type u_1} [] :
.limsInf =
@[simp]
theorem Filter.liminf_bot {α : Type u_1} {β : Type u_2} [] (f : βα) :
@[simp]
theorem Filter.limsSup_top {α : Type u_1} [] :
.limsSup =
@[simp]
theorem Filter.limsInf_top {α : Type u_1} [] :
.limsInf =
@[simp]
theorem Filter.blimsup_false {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
(Filter.blimsup u f fun (x : β) => False) =
@[simp]
theorem Filter.bliminf_false {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
(Filter.bliminf u f fun (x : β) => False) =
@[simp]
theorem Filter.limsup_const_bot {α : Type u_1} {β : Type u_2} [] {f : } :
Filter.limsup (fun (x : β) => ) f =

Same as limsup_const applied to ⊥ but without the NeBot f assumption

@[simp]
theorem Filter.liminf_const_top {α : Type u_1} {β : Type u_2} [] {f : } :
Filter.liminf (fun (x : β) => ) f =

Same as limsup_const applied to ⊤ but without the NeBot f assumption

theorem Filter.HasBasis.limsSup_eq_iInf_sSup {α : Type u_1} [] {ι : Sort u_6} {p : ιProp} {s : ιSet α} {f : } (h : f.HasBasis p s) :
f.limsSup = ⨅ (i : ι), ⨅ (_ : p i), sSup (s i)
theorem Filter.HasBasis.limsInf_eq_iSup_sInf {α : Type u_1} {ι : Type u_4} [] {p : ιProp} {s : ιSet α} {f : } (h : f.HasBasis p s) :
f.limsInf = ⨆ (i : ι), ⨆ (_ : p i), sInf (s i)
theorem Filter.limsSup_eq_iInf_sSup {α : Type u_1} [] {f : } :
f.limsSup = sf, sSup s
theorem Filter.limsInf_eq_iSup_sInf {α : Type u_1} [] {f : } :
f.limsInf = sf, sInf s
theorem Filter.limsup_le_iSup {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
⨆ (n : β), u n
theorem Filter.iInf_le_liminf {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
⨅ (n : β), u n
theorem Filter.limsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
= sf, as, 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_iInf_iSup_of_nat {α : Type u_1} [] {u : α} :
Filter.limsup u Filter.atTop = ⨅ (n : ), ⨆ (i : ), ⨆ (_ : i n), u i
theorem Filter.limsup_eq_iInf_iSup_of_nat' {α : Type u_1} [] {u : α} :
Filter.limsup u Filter.atTop = ⨅ (n : ), ⨆ (i : ), u (i + n)
theorem Filter.HasBasis.limsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {p : ιProp} {s : ιSet β} {f : } {u : βα} (h : f.HasBasis p s) :
= ⨅ (i : ι), ⨅ (_ : p i), as i, u a
theorem Filter.blimsup_congr' {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} (h : ∀ᶠ (x : β) in f, u x (p x q x)) :
=
theorem Filter.bliminf_congr' {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} (h : ∀ᶠ (x : β) in f, u x (p x q x)) :
=
theorem Filter.HasBasis.blimsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {p : ιProp} {s : ιSet β} {f : } {u : βα} (hf : f.HasBasis p s) {q : βProp} :
= ⨅ (i : ι), ⨅ (_ : p i), as i, ⨆ (_ : q a), u a
theorem Filter.blimsup_eq_iInf_biSup {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} :
= sf, ⨆ (b : β), ⨆ (_ : p b b s), u b
theorem Filter.blimsup_eq_iInf_biSup_of_nat {α : Type u_1} [] {p : } {u : α} :
Filter.blimsup u Filter.atTop p = ⨅ (i : ), ⨆ (j : ), ⨆ (_ : p j i j), u j
theorem Filter.liminf_eq_iSup_iInf {α : Type u_1} {β : Type u_2} [] {f : } {u : βα} :
= sf, as, 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_iSup_iInf_of_nat {α : Type u_1} [] {u : α} :
Filter.liminf u Filter.atTop = ⨆ (n : ), ⨅ (i : ), ⨅ (_ : i n), u i
theorem Filter.liminf_eq_iSup_iInf_of_nat' {α : Type u_1} [] {u : α} :
Filter.liminf u Filter.atTop = ⨆ (n : ), ⨅ (i : ), u (i + n)
theorem Filter.HasBasis.liminf_eq_iSup_iInf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {p : ιProp} {s : ιSet β} {f : } {u : βα} (h : f.HasBasis p s) :
= ⨆ (i : ι), ⨆ (_ : p i), as i, u a
theorem Filter.bliminf_eq_iSup_biInf {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} :
= sf, ⨅ (b : β), ⨅ (_ : p b b s), u b
theorem Filter.bliminf_eq_iSup_biInf_of_nat {α : Type u_1} [] {p : } {u : α} :
Filter.bliminf u Filter.atTop p = ⨆ (i : ), ⨅ (j : ), ⨅ (_ : p j i j), u j
theorem Filter.limsup_eq_sInf_sSup {ι : Type u_6} {R : Type u_7} (F : ) [] (a : ιR) :
= sInf ((fun (I : Set ι) => sSup (a '' I)) '' F.sets)
theorem Filter.liminf_eq_sSup_sInf {ι : Type u_6} {R : Type u_7} (F : ) [] (a : ιR) :
= sSup ((fun (I : Set ι) => sInf (a '' I)) '' F.sets)
theorem Filter.liminf_le_of_frequently_le' {α : Type u_6} {β : Type u_7} [] {f : } {u : αβ} {x : β} (h : ∃ᶠ (a : α) in f, u a x) :
x
theorem Filter.le_limsup_of_frequently_le' {α : Type u_6} {β : Type u_7} [] {f : } {u : αβ} {x : β} (h : ∃ᶠ (a : α) in f, x u a) :
x
@[simp]
theorem Filter.CompleteLatticeHom.apply_limsup_iterate {α : Type u_1} [] (f : ) (a : α) :
f (Filter.limsup (fun (n : ) => (f)^[n] a) Filter.atTop) = Filter.limsup (fun (n : ) => (f)^[n] a) Filter.atTop

If f : α → α is a morphism of complete lattices, then the limsup of its iterates of any a : α is a fixed point.

theorem Filter.CompleteLatticeHom.apply_liminf_iterate {α : Type u_1} [] (f : ) (a : α) :
f (Filter.liminf (fun (n : ) => (f)^[n] a) Filter.atTop) = Filter.liminf (fun (n : ) => (f)^[n] a) Filter.atTop

If f : α → α is a morphism of complete lattices, then the liminf of its iterates of any a : α is a fixed point.

theorem Filter.blimsup_mono {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} (h : ∀ (x : β), p xq x) :
theorem Filter.bliminf_antitone {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} (h : ∀ (x : β), p xq x) :
theorem Filter.mono_blimsup' {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} {v : βα} (h : ∀ᶠ (x : β) in f, p xu x v x) :
theorem Filter.mono_blimsup {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} {v : βα} (h : ∀ (x : β), p xu x v x) :
theorem Filter.mono_bliminf' {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} {v : βα} (h : ∀ᶠ (x : β) in f, p xu x v x) :
theorem Filter.mono_bliminf {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {u : βα} {v : βα} (h : ∀ (x : β), p xu x v x) :
theorem Filter.bliminf_antitone_filter {α : Type u_1} {β : Type u_2} [] {f : } {g : } {p : βProp} {u : βα} (h : f g) :
theorem Filter.blimsup_monotone_filter {α : Type u_1} {β : Type u_2} [] {f : } {g : } {p : βProp} {u : βα} (h : f g) :
theorem Filter.blimsup_and_le_inf {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.blimsup u f fun (x : β) => p x q x)
@[simp]
theorem Filter.bliminf_sup_le_inf_aux_left {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.blimsup u f fun (x : β) => p x q x)
@[simp]
theorem Filter.bliminf_sup_le_inf_aux_right {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.blimsup u f fun (x : β) => p x q x)
theorem Filter.bliminf_sup_le_and {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.bliminf u f fun (x : β) => p x q x
@[simp]
theorem Filter.bliminf_sup_le_and_aux_left {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.bliminf u f fun (x : β) => p x q x
@[simp]
theorem Filter.bliminf_sup_le_and_aux_right {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.bliminf u f fun (x : β) => p x q x
theorem Filter.blimsup_sup_le_or {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.blimsup u f fun (x : β) => p x q x

See also Filter.blimsup_or_eq_sup.

@[simp]
theorem Filter.bliminf_sup_le_or_aux_left {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.blimsup u f fun (x : β) => p x q x
@[simp]
theorem Filter.bliminf_sup_le_or_aux_right {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
Filter.blimsup u f fun (x : β) => p x q x
theorem Filter.bliminf_or_le_inf {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.bliminf u f fun (x : β) => p x q x)

See also Filter.bliminf_or_eq_inf.

@[simp]
theorem Filter.bliminf_or_le_inf_aux_left {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.bliminf u f fun (x : β) => p x q x)
@[simp]
theorem Filter.bliminf_or_le_inf_aux_right {α : Type u_1} {β : Type u_2} [] {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.bliminf u f fun (x : β) => p x q x)
theorem Filter.OrderIso.apply_blimsup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : } {p : βProp} {u : βα} [] (e : α ≃o γ) :
e () = Filter.blimsup (e u) f p
theorem Filter.OrderIso.apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : } {p : βProp} {u : βα} [] (e : α ≃o γ) :
e () = Filter.bliminf (e u) f p
theorem Filter.SupHom.apply_blimsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : } {p : βProp} {u : βα} [] (g : sSupHom α γ) :
g () Filter.blimsup (g u) f p
theorem Filter.InfHom.le_apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] {f : } {p : βProp} {u : βα} [] (g : sInfHom α γ) :
Filter.bliminf (g u) f p g ()
theorem Filter.limsup_sup_filter {α : Type u_1} {β : Type u_2} {f : } {u : βα} {g : } :
theorem Filter.liminf_sup_filter {α : Type u_1} {β : Type u_2} {f : } {u : βα} {g : } :
@[simp]
theorem Filter.blimsup_or_eq_sup {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.blimsup u f fun (x : β) => p x q x) =
@[simp]
theorem Filter.bliminf_or_eq_inf {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {q : βProp} {u : βα} :
(Filter.bliminf u f fun (x : β) => p x q x) =
@[simp]
theorem Filter.blimsup_sup_not {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {u : βα} :
( Filter.blimsup u f fun (x : β) => ¬p x) =
@[simp]
theorem Filter.bliminf_inf_not {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {u : βα} :
( Filter.bliminf u f fun (x : β) => ¬p x) =
@[simp]
theorem Filter.blimsup_not_sup {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {u : βα} :
(Filter.blimsup u f fun (x : β) => ¬p x) =
@[simp]
theorem Filter.bliminf_not_inf {α : Type u_1} {β : Type u_2} {f : } {p : βProp} {u : βα} :
(Filter.bliminf u f fun (x : β) => ¬p x) =
theorem Filter.limsup_piecewise {α : Type u_1} {β : Type u_2} {f : } {u : βα} {s : Set β} [DecidablePred fun (x : β) => x s] {v : βα} :
Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun (x : β) => x s) Filter.blimsup v f fun (x : β) => xs
theorem Filter.liminf_piecewise {α : Type u_1} {β : Type u_2} {f : } {u : βα} {s : Set β} [DecidablePred fun (x : β) => x s] {v : βα} :
Filter.liminf (s.piecewise u v) f = (Filter.bliminf u f fun (x : β) => x s) Filter.bliminf v f fun (x : β) => xs
theorem Filter.sup_limsup {α : Type u_1} {β : Type u_2} {f : } {u : βα} [f.NeBot] (a : α) :
a = Filter.limsup (fun (x : β) => a u x) f
theorem Filter.inf_liminf {α : Type u_1} {β : Type u_2} {f : } {u : βα} [f.NeBot] (a : α) :
a = Filter.liminf (fun (x : β) => a u x) f
theorem Filter.sup_liminf {α : Type u_1} {β : Type u_2} {f : } {u : βα} (a : α) :
a = Filter.liminf (fun (x : β) => a u x) f
theorem Filter.inf_limsup {α : Type u_1} {β : Type u_2} {f : } {u : βα} (a : α) :
a = Filter.limsup (fun (x : β) => a u x) f
theorem Filter.limsup_compl {α : Type u_1} {β : Type u_2} (f : ) (u : βα) :
() = Filter.liminf (compl u) f
theorem Filter.liminf_compl {α : Type u_1} {β : Type u_2} (f : ) (u : βα) :
() = Filter.limsup (compl u) f
theorem Filter.limsup_sdiff {α : Type u_1} {β : Type u_2} (f : ) (u : βα) (a : α) :
\ a = Filter.limsup (fun (b : β) => u b \ a) f
theorem Filter.liminf_sdiff {α : Type u_1} {β : Type u_2} (f : ) (u : βα) [f.NeBot] (a : α) :
\ a = Filter.liminf (fun (b : β) => u b \ a) f
theorem Filter.sdiff_limsup {α : Type u_1} {β : Type u_2} (f : ) (u : βα) [f.NeBot] (a : α) :
a \ = Filter.liminf (fun (b : β) => a \ u b) f
theorem Filter.sdiff_liminf {α : Type u_1} {β : Type u_2} (f : ) (u : βα) (a : α) :
a \ = Filter.limsup (fun (b : β) => a \ u b) f
theorem Filter.mem_liminf_iff_eventually_mem {α : Type u_1} {ι : Type u_4} {s : ιSet α} {𝓕 : } {a : α} :
a ∀ᶠ (i : ι) in 𝓕, a s i
theorem Filter.mem_limsup_iff_frequently_mem {α : Type u_1} {ι : Type u_4} {s : ιSet α} {𝓕 : } {a : α} :
a ∃ᶠ (i : ι) in 𝓕, a s i
theorem Filter.cofinite.blimsup_set_eq {α : Type u_1} {ι : Type u_4} {p : ιProp} {s : ιSet α} :
Filter.blimsup s Filter.cofinite p = {x : α | {n : ι | p n x s n}.Infinite}
theorem Filter.cofinite.bliminf_set_eq {α : Type u_1} {ι : Type u_4} {p : ιProp} {s : ιSet α} :
Filter.bliminf s Filter.cofinite p = {x : α | {n : ι | p n xs n}.Finite}
theorem Filter.cofinite.limsup_set_eq {α : Type u_1} {ι : Type u_4} {s : ιSet α} :
Filter.limsup s Filter.cofinite = {x : α | {n : ι | x s n}.Infinite}

In other words, limsup cofinite s is the set of elements lying inside the family s infinitely often.

theorem Filter.cofinite.liminf_set_eq {α : Type u_1} {ι : Type u_4} {s : ιSet α} :
Filter.liminf s Filter.cofinite = {x : α | {n : ι | xs n}.Finite}

In other words, liminf cofinite s is the set of elements lying outside the family s finitely often.

theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : } {b : ιSet β} {q : ιProp} (hl : l.HasBasis q b) {u : βSet α} {p : βProp} {x : α} (hx : x ) :
∃ (f : {i : ι | q i}β), ∀ (i : {i : ι | q i}), x u (f i) p (f i) f i b i
theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : } {b : ιSet β} (hl : l.HasBasis (fun (x : ι) => True) b) {u : βSet α} {p : βProp} {x : α} (hx : x ) :
∃ (f : ιβ), ∀ (i : ι), x u (f i) p (f i) f i b i
theorem Filter.frequently_lt_of_lt_limsSup {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : a < f.limsSup) :
∃ᶠ (n : α) in f, a < n
theorem Filter.frequently_lt_of_limsInf_lt {α : Type u_1} {f : } {a : α} (hf : autoParam (Filter.IsCobounded (fun (x x_1 : α) => x x_1) f) _auto✝) (h : f.limsInf < a) :
∃ᶠ (n : α) in f, n < a
theorem Filter.eventually_lt_of_lt_liminf {α : Type u_1} {β : Type u_2} {f : } {u : αβ} {b : β} (h : b < ) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
∀ᶠ (a : α) in f, b < u a
theorem Filter.eventually_lt_of_limsup_lt {α : Type u_1} {β : Type u_2} {f : } {u : αβ} {b : β} (h : < b) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
∀ᶠ (a : α) in f, u a < b
theorem Filter.le_limsup_of_frequently_le {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {b : β} (hu_le : ∃ᶠ (x : α) in f, b u x) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
b
theorem Filter.liminf_le_of_frequently_le {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {b : β} (hu_le : ∃ᶠ (x : α) in f, u x b) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
b
theorem Filter.frequently_lt_of_lt_limsup {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {b : β} (hu : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h : b < ) :
∃ᶠ (x : α) in f, b < u x
theorem Filter.frequently_lt_of_liminf_lt {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {b : β} (hu : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h : < b) :
∃ᶠ (x : α) in f, u x < b
theorem Filter.limsup_le_iff {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {x : β} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
x y > x, ∀ᶠ (a : α) in f, u a < y
theorem Filter.le_limsup_iff {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {x : β} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
x y < x, ∃ᶠ (a : α) in f, y < u a
theorem Filter.le_liminf_iff {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {x : β} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
x y < x, ∀ᶠ (a : α) in f, y < u a
theorem Filter.liminf_le_iff {α : Type u_6} {β : Type u_7} {f : } {u : αβ} {x : β} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) :
x y > x, ∃ᶠ (a : α) in f, u a < y
theorem Filter.lt_mem_sets_of_limsSup_lt {α : Type u_1} {f : } {b : α} (h : Filter.IsBounded (fun (x x_1 : α) => x x_1) f) (l : f.limsSup < b) :
∀ᶠ (a : α) in f, a < b
theorem Filter.gt_mem_sets_of_limsInf_gt {α : Type u_1} {f : } {b : α} :
Filter.IsBounded (fun (x x_1 : α) => x x_1) fb < f.limsInf∀ᶠ (a : α) in f, b < a
noncomputable def Filter.liminf_reparam {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} (f : ια) (s : ι'Set ι) (p : ι'Prop) [Countable ()] [Nonempty ()] (j : ) :

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.

Equations
• = let m := {j : | BddBelow (Set.range fun (i : (s j)) => f i)}; let g := .choose; let_fun Z := ; if j m then j else g ()
Instances For
theorem Filter.HasBasis.liminf_eq_ciSup_ciInf {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {v : } {p : ι'Prop} {s : ι'Set ι} [Countable ()] [Nonempty ()] (hv : v.HasBasis p s) {f : ια} (hs : ∀ (j : ), (s j).Nonempty) (H : ∃ (j : ), BddBelow (Set.range fun (i : (s j)) => f i)) :
= ⨆ (j : ), ⨅ (i : (s ())), f i

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 Filter.HasBasis.liminf_eq_ite {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {v : } {p : ι'Prop} {s : ι'Set ι} [Countable ()] [Nonempty ()] (hv : v.HasBasis p s) (f : ια) :
= if ∃ (j : ), s j = then sSup Set.univ else if ∀ (j : ), ¬BddBelow (Set.range fun (i : (s j)) => f i) then else ⨆ (j : ), ⨅ (i : (s ())), f i

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.

noncomputable def Filter.limsup_reparam {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} (f : ια) (s : ι'Set ι) (p : ι'Prop) [Countable ()] [Nonempty ()] (j : ) :

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.

Equations
Instances For
theorem Filter.HasBasis.limsup_eq_ciInf_ciSup {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {v : } {p : ι'Prop} {s : ι'Set ι} [Countable ()] [Nonempty ()] (hv : v.HasBasis p s) {f : ια} (hs : ∀ (j : ), (s j).Nonempty) (H : ∃ (j : ), BddAbove (Set.range fun (i : (s j)) => f i)) :
= ⨅ (j : ), ⨆ (i : (s ())), f i

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 Filter.HasBasis.limsup_eq_ite {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} {v : } {p : ι'Prop} {s : ι'Set ι} [Countable ()] [Nonempty ()] (hv : v.HasBasis p s) (f : ια) :
= if ∃ (j : ), s j = then sInf Set.univ else if ∀ (j : ), ¬BddAbove (Set.range fun (i : (s j)) => f i) then else ⨅ (j : ), ⨆ (i : (s ())), f i

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 Monotone.isBoundedUnder_le_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {g : βγ} {f : αβ} {l : } (hg : ) (hg' : Filter.Tendsto g Filter.atTop Filter.atTop) :
Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) l (g f) Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem Monotone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {g : βγ} {f : αβ} {l : } (hg : ) (hg' : Filter.Tendsto g Filter.atBot Filter.atBot) :
Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) l (g f) Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem Antitone.isBoundedUnder_le_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {g : βγ} {f : αβ} {l : } (hg : ) (hg' : Filter.Tendsto g Filter.atBot Filter.atTop) :
Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) l (g f) Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem Antitone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {g : βγ} {f : αβ} {l : } (hg : ) (hg' : Filter.Tendsto g Filter.atTop Filter.atBot) :
Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) l (g f) Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) l f
theorem GaloisConnection.l_limsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : } {v : αβ} {l : βγ} {u : γβ} (gc : ) (hlv : autoParam (Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) f fun (x : α) => l (v x)) _auto✝) (hv_co : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) :
l () Filter.limsup (fun (x : α) => l (v x)) f
theorem OrderIso.limsup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} {f : } {u : αβ} (g : β ≃o γ) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hu_co : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hgu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) f fun (x : α) => g (u x)) _auto✝) (hgu_co : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : γ) => x x_1) f fun (x : α) => g (u x)) _auto✝) :
g () = Filter.limsup (fun (x : α) => g (u x)) f
theorem OrderIso.liminf_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} {f : } {u : αβ} (g : β ≃o γ) (hu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hu_co : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (hgu : autoParam (Filter.IsBoundedUnder (fun (x x_1 : γ) => x x_1) f fun (x : α) => g (u x)) _auto✝) (hgu_co : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : γ) => x x_1) f fun (x : α) => g (u x)) _auto✝) :
g () = Filter.liminf (fun (x : α) => g (u x)) f
theorem isCoboundedUnder_le_max {α : Type u_1} {β : Type u_2} [] {f : } {u : αβ} {v : αβ} (h : Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f v) :
Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => max (u a) (v a)
theorem limsup_max {α : Type u_1} {β : Type u_2} {f : } {u : αβ} {v : αβ} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) (h₃ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₄ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) :
Filter.limsup (fun (a : α) => max (u a) (v a)) f = max () ()
theorem liminf_min {α : Type u_1} {β : Type u_2} {f : } {u : αβ} {v : αβ} (h₁ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₂ : autoParam (Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) (h₃ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f u) _auto✝) (h₄ : autoParam (Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f v) _auto✝) :
Filter.liminf (fun (a : α) => min (u a) (v a)) f = min () ()
theorem isBoundedUnder_le_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] [] {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h : is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
theorem isCoboundedUnder_le_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h : is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
theorem isBoundedUnder_le_finset_sup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] [] {f : } {F : ιαβ} {s : } (h : is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.sup fun (i : ι) => F i a
theorem isBoundedUnder_ge_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] [] {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h : is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
theorem isCoboundedUnder_ge_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h : is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
theorem isBoundedUnder_ge_finset_inf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] [] {f : } {F : ιαβ} {s : } (h : is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) :
Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f fun (a : α) => s.inf fun (i : ι) => F i a
theorem limsup_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h₁ : autoParam (is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) (h₂ : autoParam (is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) :
Filter.limsup (fun (a : α) => s.sup' hs fun (i : ι) => F i a) f = s.sup' hs fun (i : ι) => Filter.limsup (F i) f
theorem limsup_finset_sup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {f : } {F : ιαβ} {s : } (h₁ : autoParam (is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) (h₂ : autoParam (is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) :
Filter.limsup (fun (a : α) => s.sup fun (i : ι) => F i a) f = s.sup fun (i : ι) => Filter.limsup (F i) f
theorem liminf_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {f : } {F : ιαβ} {s : } (hs : s.Nonempty) (h₁ : autoParam (is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) (h₂ : autoParam (is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) :
Filter.liminf (fun (a : α) => s.inf' hs fun (i : ι) => F i a) f = s.inf' hs fun (i : ι) => Filter.liminf (F i) f
theorem liminf_finset_inf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [] {f : } {F : ιαβ} {s : } (h₁ : autoParam (is, Filter.IsCoboundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) (h₂ : autoParam (is, Filter.IsBoundedUnder (fun (x x_1 : β) => x x_1) f (F i)) _auto✝) :
Filter.liminf (fun (a : α) => s.inf fun (i : ι) => F i a) f = s.inf fun (i : ι) => Filter.liminf (F i) f