HepLean Documentation

Mathlib.Order.LiminfLimsup

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.

theorem Filter.isBounded_iff {α : Type u_1} {r : α → α → Prop} {f : Filter α} :

Filter.IsBounded r f ↔ ∃ 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.isBoundedUnder_of {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter β} {u : β → α} :

(∃ (b : α), ∀ (x : β), r (u x) b) → Filter.IsBoundedUnder r f u

A bounded function u is in particular eventually bounded.

theorem Filter.isBounded_bot {α : Type u_1} {r : α → α → Prop} :

Filter.IsBounded r ⊥ ↔ Nonempty α

theorem Filter.isBounded_top {α : Type u_1} {r : α → α → Prop} :

Filter.IsBounded r ⊤ ↔ ∃ (t : α), ∀ (x : α), r x t

theorem Filter.isBounded_principal {α : Type u_1} {r : α → α → Prop} (s : Set α) :

Filter.IsBounded r (Filter.principal s) ↔ ∃ (t : α), ∀ x ∈ s, r x t

theorem Filter.isBounded_sup {α : Type u_1} {r : α → α → Prop} {f g : Filter α} [IsTrans α r] [IsDirected α r] :

Filter.IsBounded r f → Filter.IsBounded r g → Filter.IsBounded r (f ⊔ g)

theorem Filter.IsBounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) :

Filter.IsBounded r g → Filter.IsBounded r f

theorem Filter.IsBoundedUnder.mono {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f g : Filter β} {u : β → α} (h : f ≤ g) :

Filter.IsBoundedUnder r g u → Filter.IsBoundedUnder r f u

theorem Filter.IsBoundedUnder.mono_le {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l u) (hv : v ≤ᶠ[l] u) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l v

theorem Filter.IsBoundedUnder.mono_ge {α : Type u_1} {β : Type u_2} [Preorder β] {l : Filter α} {u v : α → β} (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l u) (hv : u ≤ᶠ[l] v) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l v

theorem Filter.isBoundedUnder_const {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsRefl α r] {l : Filter β} {a : α} :

Filter.IsBoundedUnder r l fun (x : β) => a

theorem Filter.IsBounded.isBoundedUnder {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter α} {q : β → β → Prop} {u : α → β} (hu : ∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁)) :

Filter.IsBounded r f → Filter.IsBoundedUnder q f u

theorem Filter.IsBoundedUnder.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {l : Filter γ} {q : β → β → Prop} {u : γ → α} {v : α → β} (hv : ∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁)) :

Filter.IsBoundedUnder r l u → Filter.IsBoundedUnder q l (v ∘ u)

theorem Filter.IsBoundedUnder.eventually_le {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) :

∃ (a : α), ∀ᶠ (x : β) in f, u x ≤ a

theorem Filter.IsBoundedUnder.eventually_ge {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) :

∃ (a : α), ∀ᶠ (x : β) in f, a ≤ u x

theorem Filter.isBoundedUnder_of_eventually_le {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {a : α} (h : ∀ᶠ (x : β) in f, u x ≤ a) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

theorem Filter.isBoundedUnder_of_eventually_ge {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {a : α} (h : ∀ᶠ (x : β) in f, a ≤ u x) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

theorem Filter.isBoundedUnder_iff_eventually_bddAbove {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ↔ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

theorem Filter.isBoundedUnder_iff_eventually_bddBelow {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u ↔ ∃ (s : Set β), BddBelow (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

theorem BddAbove.isBoundedUnder {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {s : Set β} (hs : s ∈ f) (hu : BddAbove (u '' s)) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

theorem BddAbove.isBoundedUnder_of_range {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (hu : BddAbove (Set.range u)) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

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

theorem BddBelow.isBoundedUnder {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} {s : Set β} (hs : s ∈ f) (hu : BddBelow (u '' s)) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

theorem BddBelow.isBoundedUnder_of_range {α : Type u_1} {β : Type u_2} [Preorder α] {f : Filter β} {u : β → α} (hu : BddBelow (Set.range u)) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

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

theorem Filter.IsBoundedUnder.le_of_finite {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Finite β] {f : Filter β} {u : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

theorem Filter.IsBoundedUnder.ge_of_finite {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Finite β] {f : Filter β} {u : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

theorem Monotone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)

theorem Monotone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)

theorem Antitone.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)

theorem Antitone.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)

theorem Filter.not_isBoundedUnder_of_tendsto_atTop {α : Type u_1} {β : Type u_2} [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Filter.Tendsto f l Filter.atTop) :

¬Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f

theorem Filter.not_isBoundedUnder_of_tendsto_atBot {α : Type u_1} {β : Type u_2} [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Filter.Tendsto f l Filter.atBot) :

¬Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f

theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite {α : Type u_1} {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : α → β} (hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) Filter.cofinite f) :

BddAbove (Set.range f)

theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite {α : Type u_1} {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : α → β} (hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) Filter.cofinite f) :

BddBelow (Set.range f)

theorem Filter.IsBoundedUnder.bddAbove_range {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≤ x2] {f : ℕ → β} (hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) Filter.atTop f) :

BddAbove (Set.range f)

theorem Filter.IsBoundedUnder.bddBelow_range {β : Type u_2} [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 ≥ x2] {f : ℕ → β} (hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) Filter.atTop f) :

BddBelow (Set.range f)

theorem Filter.IsCobounded.mk {α : Type u_1} {r : α → α → Prop} {f : Filter α} [IsTrans α r] (a : α) (h : ∀ s ∈ f, ∃ x ∈ s, r a x) :

Filter.IsCobounded r f

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 : Filter α} [IsTrans α r] [f.NeBot] :

Filter.IsBounded r f → Filter.IsCobounded (flip r) 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.IsBounded.isCobounded_ge {α : Type u_1} {f : Filter α} [Preorder α] [f.NeBot] (h : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f

theorem Filter.IsBounded.isCobounded_le {α : Type u_1} {f : Filter α} [Preorder α] [f.NeBot] (h : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f

theorem Filter.IsBoundedUnder.isCoboundedUnder_flip {α : Type u_1} {γ : Type u_3} {r : α → α → Prop} {u : γ → α} {l : Filter γ} [IsTrans α r] [l.NeBot] (h : Filter.IsBoundedUnder r l u) :

Filter.IsCoboundedUnder (flip r) l u

theorem Filter.IsBoundedUnder.isCoboundedUnder_le {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [Preorder α] [l.NeBot] (h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

theorem Filter.IsBoundedUnder.isCoboundedUnder_ge {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [Preorder α] [l.NeBot] (h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

theorem Filter.isCoboundedUnder_le_of_eventually_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ᶠ (i : ι) in l, x ≤ f i) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f

theorem Filter.isCoboundedUnder_ge_of_eventually_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ᶠ (i : ι) in l, f i ≤ x) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f

theorem Filter.isCoboundedUnder_le_of_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ (i : ι), x ≤ f i) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f

theorem Filter.isCoboundedUnder_ge_of_le {α : Type u_1} {ι : Type u_4} [Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀ (i : ι), f i ≤ x) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f

theorem Filter.isCobounded_bot {α : Type u_1} {r : α → α → Prop} :

Filter.IsCobounded r ⊥ ↔ ∃ (b : α), ∀ (x : α), r b x

theorem Filter.isCobounded_top {α : Type u_1} {r : α → α → Prop} :

Filter.IsCobounded r ⊤ ↔ Nonempty α

theorem Filter.isCobounded_principal {α : Type u_1} {r : α → α → Prop} (s : Set α) :

Filter.IsCobounded r (Filter.principal s) ↔ ∃ (b : α), ∀ (a : α), (∀ x ∈ s, r x a) → r b a

theorem Filter.IsCobounded.mono {α : Type u_1} {r : α → α → Prop} {f g : Filter α} (h : f ≤ g) :

Filter.IsCobounded r f → Filter.IsCobounded r g

theorem Filter.IsCobounded.frequently_ge {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) :

∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

For nontrivial filters in linear orders, coboundedness for ≤ implies frequent boundedness from below.

theorem Filter.IsCobounded.frequently_le {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f) :

∃ (u : α), ∃ᶠ (x : α) in f, x ≤ u

For nontrivial filters in linear orders, coboundedness for ≥ implies frequent boundedness from above.

theorem Filter.IsCobounded.of_frequently_ge {α : Type u_1} {f : Filter α} [LinearOrder α] {l : α} (freq_ge : ∃ᶠ (x : α) in f, l ≤ x) :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f

In linear orders, frequent boundedness from below implies coboundedness for ≤.

theorem Filter.IsCobounded.of_frequently_le {α : Type u_1} {f : Filter α} [LinearOrder α] {u : α} (freq_le : ∃ᶠ (r : α) in f, r ≤ u) :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f

In linear orders, frequent boundedness from above implies coboundedness for ≥.

theorem Filter.IsCoboundedUnder.frequently_ge {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) :

∃ (a : α), ∃ᶠ (x : ι) in f, a ≤ u x

theorem Filter.IsCoboundedUnder.frequently_le {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) :

∃ (a : α), ∃ᶠ (x : ι) in f, u x ≤ a

theorem Filter.IsCoboundedUnder.of_frequently_ge {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_ge : ∃ᶠ (x : ι) in f, a ≤ u x) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

theorem Filter.IsCoboundedUnder.of_frequently_le {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_le : ∃ᶠ (x : ι) in f, u x ≤ a) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

theorem Filter.isBoundedUnder_sum {α : Type u_6} {f : Filter α} {R : Type u_7} {κ : Type u_8} [AddCommMonoid R] {r : R → R → Prop} (hr : ∀ (v₁ v₂ : α → R), Filter.IsBoundedUnder r f v₁ → Filter.IsBoundedUnder r f v₂ → Filter.IsBoundedUnder r f (v₁ + v₂)) (hr₀ : r 0 0) {u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, Filter.IsBoundedUnder r f (u k)) :

Filter.IsBoundedUnder r f (∑ k ∈ s, u k)

theorem Filter.isBoundedUnder_ge_add {α : Type u_6} {f : Filter α} {R : Type u_7} [Preorder R] [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_ge : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f u) (v_bdd_ge : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f v) :

Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u + v)

theorem Filter.isBoundedUnder_le_add {α : Type u_6} {f : Filter α} {R : Type u_7} [Preorder R] [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_le : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f u) (v_bdd_le : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f v) :

Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u + v)

theorem Filter.isBoundedUnder_le_sum {α : Type u_6} {f : Filter α} {R : Type u_7} [Preorder R] {κ : Type u_8} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :

(∀ k ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u k)) → Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (∑ k ∈ s, u k)

theorem Filter.isBoundedUnder_ge_sum {α : Type u_6} {f : Filter α} {R : Type u_7} [Preorder R] {κ : Type u_8} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :

(∀ k ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u k)) → Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (∑ k ∈ s, u k)

theorem Filter.isCoboundedUnder_ge_add {α : Type u_6} {R : Type u_7} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [CovariantClass R R (fun (a b : R) => a + b) fun (x1 x2 : R) => x1 ≤ x2] [CovariantClass R R (fun (a b : R) => b + a) fun (x1 x2 : R) => x1 ≤ x2] {u v : α → R} (hu : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f u) (hv : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f v) :

Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u + v)

theorem Filter.isCoboundedUnder_le_add {α : Type u_6} {R : Type u_7} [LinearOrder R] [Add R] {f : Filter α} [f.NeBot] [CovariantClass R R (fun (a b : R) => a + b) fun (x1 x2 : R) => x1 ≤ x2] [CovariantClass R R (fun (a b : R) => b + a) fun (x1 x2 : R) => x1 ≤ x2] {u v : α → R} (hu : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f u) (hv : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f v) :

Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u + v)

theorem Filter.isBoundedUnder_le_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [Mul α] [Zero α] [Preorder α] [PosMulMono α] [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f (u * v)

theorem Filter.isCoboundedUnder_ge_mul_of_nonneg {α : Type u_1} {ι : Type u_4} [Mul α] [Zero α] [LinearOrder α] [PosMulMono α] [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v) :

Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f (u * v)

theorem Filter.isBounded_le_atBot {α : Type u_1} [Preorder α] [Nonempty α] :

Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) Filter.atBot

theorem Filter.isBounded_ge_atTop {α : Type u_1} [Preorder α] [Nonempty α] :

Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) Filter.atTop

theorem Filter.Tendsto.isBoundedUnder_le_atBot {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] {f : Filter β} {u : β → α} (h : Filter.Tendsto u f Filter.atBot) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u

theorem Filter.Tendsto.isBoundedUnder_ge_atTop {α : Type u_1} {β : Type u_2} [Preorder α] [Nonempty α] {f : Filter β} {u : β → α} (h : Filter.Tendsto u f Filter.atTop) :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

theorem Filter.bddAbove_range_of_tendsto_atTop_atBot {α : Type u_1} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] {u : ℕ → α} (hx : Filter.Tendsto u Filter.atTop Filter.atBot) :

BddAbove (Set.range u)

theorem Filter.bddBelow_range_of_tendsto_atTop_atTop {α : Type u_1} [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] {u : ℕ → α} (hx : Filter.Tendsto u Filter.atTop Filter.atTop) :

BddBelow (Set.range u)

theorem Filter.isCobounded_le_of_bot {α : Type u_1} [Preorder α] [OrderBot α] {f : Filter α} :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f

theorem Filter.isCobounded_ge_of_top {α : Type u_1} [Preorder α] [OrderTop α] {f : Filter α} :

Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f

theorem Filter.isBounded_le_of_top {α : Type u_1} [Preorder α] [OrderTop α] {f : Filter α} :

Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f

theorem Filter.isBounded_ge_of_bot {α : Type u_1} [Preorder α] [OrderBot α] {f : Filter α} :

Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f

@[simp]

theorem OrderIso.isBoundedUnder_le_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

@[simp]

theorem OrderIso.isBoundedUnder_ge_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

@[simp]

theorem Filter.isBoundedUnder_le_inv {α : Type u_1} {β : Type u_2} [OrderedCommGroup α] {l : Filter β} {u : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

@[simp]

theorem Filter.isBoundedUnder_le_neg {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup α] {l : Filter β} {u : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => -u x) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u

@[simp]

theorem Filter.isBoundedUnder_ge_inv {α : Type u_1} {β : Type u_2} [OrderedCommGroup α] {l : Filter β} {u : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

@[simp]

theorem Filter.isBoundedUnder_ge_neg {α : Type u_1} {β : Type u_2} [OrderedAddCommGroup α] {l : Filter β} {u : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => -u x) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u

theorem Filter.IsBoundedUnder.sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {f : Filter β} {u v : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u → Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v → Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a

@[simp]

theorem Filter.isBoundedUnder_le_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] {f : Filter β} {u v : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v

theorem Filter.IsBoundedUnder.inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] {f : Filter β} {u v : β → α} :

Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u → Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v → Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a

@[simp]

theorem Filter.isBoundedUnder_ge_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] {f : Filter β} {u v : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v

theorem Filter.isBoundedUnder_le_abs {α : Type u_1} {β : Type u_2} [LinearOrderedAddCommGroup α] {f : Filter β} {u : β → α} :

(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => |u a|) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u

def Filter.tacticIsBoundedDefault :

Lean.ParserDescr

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

Filter.tacticIsBoundedDefault = Lean.ParserDescr.node `Filter.tacticIsBoundedDefault 1024 (Lean.ParserDescr.nonReservedSymbol "isBoundedDefault" false)

Instances For

def Filter.limsSup {α : Type u_1} [ConditionallyCompleteLattice α] (f : Filter α) :

α

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} [ConditionallyCompleteLattice α] (f : Filter α) :

α

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} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) :

α

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

Filter.limsup u f = (Filter.map u f).limsSup

Instances For

def Filter.liminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) :

α

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

Filter.liminf u f = (Filter.map u f).limsInf

Instances For

def Filter.blimsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) (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

Filter.blimsup u f p = sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}

Instances For

def Filter.bliminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) (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

Filter.bliminf u f p = sSup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}

Instances For

theorem Filter.limsup_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} :

Filter.limsup u f = sInf {a : α | ∀ᶠ (n : β) in f, u n ≤ a}

theorem Filter.liminf_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} :

Filter.liminf u f = sSup {a : α | ∀ᶠ (n : β) in f, a ≤ u n}

theorem Filter.blimsup_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.blimsup u f p = sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}

theorem Filter.bliminf_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.bliminf u f p = sSup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}

theorem Filter.liminf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) :

Filter.liminf (u ∘ v) f = Filter.liminf u (Filter.map v f)

theorem Filter.limsup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) :

Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)

@[simp]

theorem Filter.blimsup_true {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) :

(Filter.blimsup u f fun (x : β) => True) = Filter.limsup u f

@[simp]

theorem Filter.bliminf_true {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) :

(Filter.bliminf u f fun (x : β) => True) = Filter.liminf u f

theorem Filter.blimsup_eq_limsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.blimsup u f p = Filter.limsup u (f ⊓ Filter.principal {x : β | p x})

theorem Filter.bliminf_eq_liminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.bliminf u f p = Filter.liminf u (f ⊓ Filter.principal {x : β | p x})

theorem Filter.blimsup_eq_limsup_subtype {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.blimsup u f p = Filter.limsup (u ∘ Subtype.val) (Filter.comap Subtype.val f)

theorem Filter.bliminf_eq_liminf_subtype {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} :

Filter.bliminf u f p = Filter.liminf (u ∘ Subtype.val) (Filter.comap Subtype.val f)

theorem Filter.limsSup_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : ∀ᶠ (n : α) in f, n ≤ a) :

f.limsSup ≤ a

theorem Filter.le_limsInf_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : ∀ᶠ (n : α) in f, a ≤ n) :

a ≤ f.limsInf

theorem Filter.limsup_le_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ᶠ (n : β) in f, u n ≤ a) :

Filter.limsup u f ≤ a

theorem Filter.le_liminf_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h : ∀ᶠ (n : β) in f, a ≤ u n) :

a ≤ Filter.liminf u f

theorem Filter.le_limsSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : α) in f, n ≤ b) → a ≤ b) :

a ≤ f.limsSup

theorem Filter.limsInf_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : α) in f, b ≤ n) → b ≤ a) :

f.limsInf ≤ a

theorem Filter.le_limsup_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b) :

a ≤ Filter.limsup u f

theorem Filter.liminf_le_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a) :

Filter.liminf u f ≤ a

theorem Filter.limsInf_le_limsSup {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} [f.NeBot] (h₁ : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h₂ : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) :

f.limsInf ≤ f.limsSup

theorem Filter.liminf_le_limsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} [f.NeBot] {u : β → α} (h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) :

Filter.liminf u f ≤ Filter.limsup u f

theorem Filter.limsSup_le_limsSup {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (hg : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g := by isBoundedDefault) (h : ∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a) :

f.limsSup ≤ g.limsSup

theorem Filter.limsInf_le_limsInf {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (hf : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (hg : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g := by isBoundedDefault) (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} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : u ≤ᶠ[f] v) (hu : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hv : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) :

Filter.limsup u f ≤ Filter.limsup v f

theorem Filter.liminf_le_liminf {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a ≤ v a) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hv : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v := by isBoundedDefault) :

Filter.liminf u f ≤ Filter.liminf v f

theorem Filter.limsSup_le_limsSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (h : f ≤ g) (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (hg : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g := by isBoundedDefault) :

f.limsSup ≤ g.limsSup

theorem Filter.limsInf_le_limsInf_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (h : g ≤ f) (hf : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (hg : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g := by isBoundedDefault) :

f.limsInf ≤ g.limsInf

theorem Filter.limsup_le_limsup_of_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : f ≤ g) {u : α → β} (hf : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hg : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) g u := by isBoundedDefault) :

Filter.limsup u f ≤ Filter.limsup u g

theorem Filter.liminf_le_liminf_of_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : g ≤ f) {u : α → β} (hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hg : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) g u := by isBoundedDefault) :

Filter.liminf u f ≤ Filter.liminf u g

theorem Filter.limsSup_principal_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) :

(Filter.principal s).limsSup = sSup s

theorem Filter.limsInf_principal_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) :

(Filter.principal s).limsInf = sInf s

theorem Filter.limsup_top_eq_ciSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddAbove (Set.range u)) :

Filter.limsup u ⊤ = ⨆ (i : β), u i

theorem Filter.liminf_top_eq_ciInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddBelow (Set.range u)) :

Filter.liminf u ⊤ = ⨅ (i : β), u i

theorem Filter.limsup_congr {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) :

Filter.limsup u f = Filter.limsup v f

theorem Filter.blimsup_congr {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ (a : β) in f, p a → u a = v a) :

Filter.blimsup u f p = Filter.blimsup v f p

theorem Filter.bliminf_congr {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ (a : β) in f, p a → u a = v a) :

Filter.bliminf u f p = Filter.bliminf v f p

theorem Filter.liminf_congr {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) :

Filter.liminf u f = Filter.liminf v f

@[simp]

theorem Filter.limsup_const {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) :

Filter.limsup (fun (x : α) => b) f = b

@[simp]

theorem Filter.liminf_const {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) :

Filter.liminf (fun (x : α) => b) f = b

theorem Filter.HasBasis.liminf_eq_sSup_iUnion_iInter {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :

Filter.liminf f v = sSup (⋃ (j : Subtype p), ⋂ (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} [ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :

Filter.liminf f v = sSup Set.univ

theorem Filter.HasBasis.limsup_eq_sInf_iUnion_iInter {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) :

Filter.limsup f v = sInf (⋃ (j : Subtype p), ⋂ (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} [ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) :

Filter.limsup f v = sInf Set.univ

@[simp]

theorem Filter.liminf_nat_add {α : Type u_1} [ConditionallyCompleteLattice α] (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} [ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ) :

Filter.limsup (fun (i : ℕ) => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop

@[simp]

theorem Filter.limsSup_bot {α : Type u_1} [CompleteLattice α] :

⊥.limsSup = ⊥

@[simp]

theorem Filter.limsup_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) :

Filter.limsup f ⊥ = ⊥

@[simp]

theorem Filter.limsInf_bot {α : Type u_1} [CompleteLattice α] :

⊥.limsInf = ⊤

@[simp]

theorem Filter.liminf_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) :

Filter.liminf f ⊥ = ⊤

@[simp]

theorem Filter.limsSup_top {α : Type u_1} [CompleteLattice α] :

⊤.limsSup = ⊤

@[simp]

theorem Filter.limsInf_top {α : Type u_1} [CompleteLattice α] :

⊤.limsInf = ⊥

@[simp]

theorem Filter.blimsup_false {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} :

(Filter.blimsup u f fun (x : β) => False) = ⊥

@[simp]

theorem Filter.bliminf_false {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} :

(Filter.bliminf u f fun (x : β) => False) = ⊤

@[simp]

theorem Filter.limsup_const_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} :

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} [CompleteLattice α] {f : Filter β} :

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} [CompleteLattice α] {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (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} [CompleteLattice α] {p : ι → Prop} {s : ι → Set α} {f : Filter α} (h : f.HasBasis p s) :

f.limsInf = ⨆ (i : ι), ⨆ (_ : p i), sInf (s i)

theorem Filter.limsSup_eq_iInf_sSup {α : Type u_1} [CompleteLattice α] {f : Filter α} :

f.limsSup = ⨅ s ∈ f, sSup s

theorem Filter.limsInf_eq_iSup_sInf {α : Type u_1} [CompleteLattice α] {f : Filter α} :

f.limsInf = ⨆ s ∈ f, sInf s

theorem Filter.limsup_le_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} :

Filter.limsup u f ≤ ⨆ (n : β), u n

theorem Filter.iInf_le_liminf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} :

⨅ (n : β), u n ≤ Filter.liminf u f

theorem Filter.limsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} :

Filter.limsup u f = ⨅ s ∈ f, ⨆ 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_iInf_iSup_of_nat {α : Type u_1} [CompleteLattice α] {u : ℕ → α} :

Filter.limsup u Filter.atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i

theorem Filter.limsup_eq_iInf_iSup_of_nat' {α : Type u_1} [CompleteLattice α] {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} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) :

Filter.limsup u f = ⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, u a

theorem Filter.limsSup_principal_eq_sSup {α : Type u_1} [CompleteLattice α] (s : Set α) :

(Filter.principal s).limsSup = sSup s

theorem Filter.limsInf_principal_eq_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) :

(Filter.principal s).limsInf = sInf s

@[simp]

theorem Filter.limsup_top_eq_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) :

Filter.limsup u ⊤ = ⨆ (i : β), u i

@[simp]

theorem Filter.liminf_top_eq_iInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) :

Filter.liminf u ⊤ = ⨅ (i : β), u i

@[deprecated Filter.limsSup_principal_eq_sSup]

theorem Filter.limsSup_principal {α : Type u_1} [CompleteLattice α] (s : Set α) :

(Filter.principal s).limsSup = sSup s

Alias of Filter.limsSup_principal_eq_sSup.

@[deprecated Filter.limsInf_principal_eq_sInf]

theorem Filter.limsInf_principal {α : Type u_1} [CompleteLattice α] (s : Set α) :

(Filter.principal s).limsInf = sInf s

Alias of Filter.limsInf_principal_eq_sInf.

@[deprecated Filter.limsup_top_eq_iSup]

theorem Filter.limsup_top {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) :

Filter.limsup u ⊤ = ⨆ (i : β), u i

Alias of Filter.limsup_top_eq_iSup.

@[deprecated Filter.liminf_top_eq_iInf]

theorem Filter.liminf_top {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) :

Filter.liminf u ⊤ = ⨅ (i : β), u i

Alias of Filter.liminf_top_eq_iInf.

theorem Filter.blimsup_congr' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)) :

Filter.blimsup u f p = Filter.blimsup u f q

theorem Filter.bliminf_congr' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x)) :

Filter.bliminf u f p = Filter.bliminf u f q

theorem Filter.HasBasis.blimsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (hf : f.HasBasis p s) {q : β → Prop} :

Filter.blimsup u f q = ⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

theorem Filter.blimsup_eq_iInf_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

Filter.blimsup u f p = ⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b

theorem Filter.blimsup_eq_iInf_biSup_of_nat {α : Type u_1} [CompleteLattice α] {p : ℕ → Prop} {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} [CompleteLattice α] {f : Filter β} {u : β → α} :

Filter.liminf u f = ⨆ s ∈ f, ⨅ 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_iSup_iInf_of_nat {α : Type u_1} [CompleteLattice α] {u : ℕ → α} :

Filter.liminf u Filter.atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i

theorem Filter.liminf_eq_iSup_iInf_of_nat' {α : Type u_1} [CompleteLattice α] {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} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) :

Filter.liminf u f = ⨆ (i : ι), ⨆ (_ : p i), ⨅ a ∈ s i, u a

theorem Filter.bliminf_eq_iSup_biInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

Filter.bliminf u f p = ⨆ s ∈ f, ⨅ (b : β), ⨅ (_ : p b ∧ b ∈ s), u b

theorem Filter.bliminf_eq_iSup_biInf_of_nat {α : Type u_1} [CompleteLattice α] {p : ℕ → Prop} {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 : Filter ι) [CompleteLattice R] (a : ι → R) :

Filter.limsup a F = sInf ((fun (I : Set ι) => sSup (a '' I)) '' F.sets)

theorem Filter.liminf_eq_sSup_sInf {ι : Type u_6} {R : Type u_7} (F : Filter ι) [CompleteLattice R] (a : ι → R) :

Filter.liminf a F = sSup ((fun (I : Set ι) => sInf (a '' I)) '' F.sets)

theorem Filter.liminf_le_of_frequently_le' {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, u a ≤ x) :

Filter.liminf u f ≤ x

theorem Filter.le_limsup_of_frequently_le' {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, x ≤ u a) :

x ≤ Filter.limsup u f

@[simp]

theorem CompleteLatticeHom.apply_limsup_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (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.

@[deprecated CompleteLatticeHom.apply_limsup_iterate]

theorem Filter.CompleteLatticeHom.apply_limsup_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) :

f (Filter.limsup (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop

Alias of CompleteLatticeHom.apply_limsup_iterate.

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

theorem CompleteLatticeHom.apply_liminf_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (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.

@[deprecated CompleteLatticeHom.apply_liminf_iterate]

theorem Filter.CompleteLatticeHom.apply_liminf_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) :

f (Filter.liminf (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop

Alias of CompleteLatticeHom.apply_liminf_iterate.

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} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ (x : β), p x → q x) :

Filter.blimsup u f p ≤ Filter.blimsup u f q

theorem Filter.bliminf_antitone {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ (x : β), p x → q x) :

Filter.bliminf u f q ≤ Filter.bliminf u f p

theorem Filter.mono_blimsup' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ᶠ (x : β) in f, p x → u x ≤ v x) :

Filter.blimsup u f p ≤ Filter.blimsup v f p

theorem Filter.mono_blimsup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ (x : β), p x → u x ≤ v x) :

Filter.blimsup u f p ≤ Filter.blimsup v f p

theorem Filter.mono_bliminf' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ᶠ (x : β) in f, p x → u x ≤ v x) :

Filter.bliminf u f p ≤ Filter.bliminf v f p

theorem Filter.mono_bliminf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ (x : β), p x → u x ≤ v x) :

Filter.bliminf u f p ≤ Filter.bliminf v f p

theorem Filter.bliminf_antitone_filter {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α} (h : f ≤ g) :

Filter.bliminf u g p ≤ Filter.bliminf u f p

theorem Filter.blimsup_monotone_filter {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α} (h : f ≤ g) :

Filter.blimsup u f p ≤ Filter.blimsup u g p

theorem Filter.blimsup_and_le_inf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

@[simp]

theorem Filter.bliminf_sup_le_inf_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

@[simp]

theorem Filter.bliminf_sup_le_inf_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

theorem Filter.bliminf_sup_le_and {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.bliminf u f p ⊔ Filter.bliminf u f q ≤ 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} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.bliminf u f p ≤ 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} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.bliminf u f q ≤ Filter.bliminf u f fun (x : β) => p x ∧ q x

theorem Filter.blimsup_sup_le_or {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.blimsup u f p ⊔ Filter.blimsup u f q ≤ 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} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.blimsup u f p ≤ 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} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

Filter.blimsup u f q ≤ Filter.blimsup u f fun (x : β) => p x ∨ q x

theorem Filter.bliminf_or_le_inf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

See also Filter.bliminf_or_eq_inf.

@[simp]

theorem Filter.bliminf_or_le_inf_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

@[simp]

theorem Filter.bliminf_or_le_inf_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

theorem OrderIso.apply_blimsup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) :

e (Filter.blimsup u f p) = Filter.blimsup (⇑e ∘ u) f p

@[deprecated OrderIso.apply_blimsup]

theorem Filter.OrderIso.apply_blimsup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) :

e (Filter.blimsup u f p) = Filter.blimsup (⇑e ∘ u) f p

Alias of OrderIso.apply_blimsup.

theorem OrderIso.apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) :

e (Filter.bliminf u f p) = Filter.bliminf (⇑e ∘ u) f p

@[deprecated OrderIso.apply_bliminf]

theorem Filter.OrderIso.apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) :

e (Filter.bliminf u f p) = Filter.bliminf (⇑e ∘ u) f p

Alias of OrderIso.apply_bliminf.

theorem sSupHom.apply_blimsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sSupHom α γ) :

g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p

@[deprecated sSupHom.apply_blimsup_le]

theorem Filter.SupHom.apply_blimsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sSupHom α γ) :

g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p

Alias of sSupHom.apply_blimsup_le.

theorem sInfHom.le_apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sInfHom α γ) :

Filter.bliminf (⇑g ∘ u) f p ≤ g (Filter.bliminf u f p)

@[deprecated sInfHom.le_apply_bliminf]

theorem Filter.InfHom.le_apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sInfHom α γ) :

Filter.bliminf (⇑g ∘ u) f p ≤ g (Filter.bliminf u f p)

Alias of sInfHom.le_apply_bliminf.

theorem Filter.limsup_sup_filter {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} :

Filter.limsup u (f ⊔ g) = Filter.limsup u f ⊔ Filter.limsup u g

theorem Filter.liminf_sup_filter {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} :

Filter.liminf u (f ⊔ g) = Filter.liminf u f ⊓ Filter.liminf u g

@[simp]

theorem Filter.blimsup_or_eq_sup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

@[simp]

theorem Filter.bliminf_or_eq_inf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} :

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

@[simp]

theorem Filter.blimsup_sup_not {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

(Filter.blimsup u f p ⊔ Filter.blimsup u f fun (x : β) => ¬p x) = Filter.limsup u f

@[simp]

theorem Filter.bliminf_inf_not {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

(Filter.bliminf u f p ⊓ Filter.bliminf u f fun (x : β) => ¬p x) = Filter.liminf u f

@[simp]

theorem Filter.blimsup_not_sup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

(Filter.blimsup u f fun (x : β) => ¬p x) ⊔ Filter.blimsup u f p = Filter.limsup u f

@[simp]

theorem Filter.bliminf_not_inf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} :

(Filter.bliminf u f fun (x : β) => ¬p x) ⊓ Filter.bliminf u f p = Filter.liminf u f

theorem Filter.limsup_piecewise {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {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 : β) => x ∉ s

theorem Filter.liminf_piecewise {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {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 : β) => x ∉ s

theorem Filter.sup_limsup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) :

a ⊔ Filter.limsup u f = Filter.limsup (fun (x : β) => a ⊔ u x) f

theorem Filter.inf_liminf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) :

a ⊓ Filter.liminf u f = Filter.liminf (fun (x : β) => a ⊓ u x) f

theorem Filter.sup_liminf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) :

a ⊔ Filter.liminf u f = Filter.liminf (fun (x : β) => a ⊔ u x) f

theorem Filter.inf_limsup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) :

a ⊓ Filter.limsup u f = Filter.limsup (fun (x : β) => a ⊓ u x) f

theorem Filter.limsup_compl {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) :

(Filter.limsup u f)ᶜ = Filter.liminf (compl ∘ u) f

theorem Filter.liminf_compl {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) :

(Filter.liminf u f)ᶜ = Filter.limsup (compl ∘ u) f

theorem Filter.limsup_sdiff {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) :

Filter.limsup u f \ a = Filter.limsup (fun (b : β) => u b \ a) f

theorem Filter.liminf_sdiff {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) :

Filter.liminf u f \ a = Filter.liminf (fun (b : β) => u b \ a) f

theorem Filter.sdiff_limsup {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) :

a \ Filter.limsup u f = Filter.liminf (fun (b : β) => a \ u b) f

theorem Filter.sdiff_liminf {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) :

a \ Filter.liminf u f = Filter.limsup (fun (b : β) => a \ u b) f

theorem Filter.mem_liminf_iff_eventually_mem {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} :

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

theorem Filter.mem_limsup_iff_frequently_mem {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} :

a ∈ Filter.limsup s 𝓕 ↔ ∃ᶠ (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 ∧ x ∉ s 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 : ι | x ∉ s 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 : Filter β} {b : ι → Set β} {q : ι → Prop} (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ Filter.blimsup u l p) :

∃ (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 : Filter β} {b : ι → Set β} (hl : l.HasBasis (fun (x : ι) => True) b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ Filter.blimsup u l p) :

∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

theorem Filter.frequently_lt_of_lt_limsSup {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : a < f.limsSup) :

∃ᶠ (n : α) in f, a < n

theorem Filter.frequently_lt_of_limsInf_lt {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : f.limsInf < a) :

∃ᶠ (n : α) in f, n < a

theorem Filter.eventually_lt_of_lt_liminf {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : b < Filter.liminf u f) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) :

∀ᶠ (a : α) in f, b < u a

theorem Filter.eventually_lt_of_limsup_lt {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : Filter.limsup u f < b) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) :

∀ᶠ (a : α) in f, u a < b

theorem Filter.le_limsup_of_frequently_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu_le : ∃ᶠ (x : α) in f, b ≤ u x) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) :

b ≤ Filter.limsup u f

theorem Filter.liminf_le_of_frequently_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu_le : ∃ᶠ (x : α) in f, u x ≤ b) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) :

Filter.liminf u f ≤ b

theorem Filter.frequently_lt_of_lt_limsup {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h : b < Filter.limsup u f) :

∃ᶠ (x : α) in f, b < u x

theorem Filter.frequently_lt_of_liminf_lt {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h : Filter.liminf u f < b) :

∃ᶠ (x : α) in f, u x < b

theorem Filter.limsup_le_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) :

Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y

theorem Filter.le_limsup_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) :

x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a

theorem Filter.le_liminf_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) :

x ≤ Filter.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a

theorem Filter.liminf_le_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) :

Filter.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y

theorem Filter.lt_mem_sets_of_limsSup_lt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α} (h : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) (l : f.limsSup < b) :

∀ᶠ (a : α) in f, a < b

theorem Filter.gt_mem_sets_of_limsInf_gt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α} :

Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f → b < f.limsInf → ∀ᶠ (a : α) in f, b < a

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

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

Filter.liminf_reparam f s p j = if j ∈ {j : Subtype p | BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i)} then j else ⋯.choose (Nat.find ⋯)

Instances For

theorem Filter.HasBasis.liminf_eq_ciSup_ciInf {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s ↑j).Nonempty) (H : ∃ (j : Subtype p), BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i)) :

Filter.liminf f v = ⨆ (j : Subtype p), ⨅ (i : ↑(s ↑(Filter.liminf_reparam f s p j))), 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} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) :

Filter.liminf f v = if ∃ (j : Subtype p), s ↑j = ∅ then sSup Set.univ else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i) then sSup ∅ else ⨆ (j : Subtype p), ⨅ (i : ↑(s ↑(Filter.liminf_reparam f s p j))), 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} [ConditionallyCompleteLinearOrder α] (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) :

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

Filter.limsup_reparam f s p j = Filter.liminf_reparam f s p j

Instances For

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

Filter.limsup f v = ⨅ (j : Subtype p), ⨆ (i : ↑(s ↑(Filter.limsup_reparam f s p j))), 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} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) :

Filter.limsup f v = if ∃ (j : Subtype p), s ↑j = ∅ then sInf Set.univ else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun (i : ↑(s ↑j)) => f ↑i) then sInf ∅ else ⨅ (j : Subtype p), ⨆ (i : ↑(s ↑(Filter.limsup_reparam f s p j))), 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} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Filter.Tendsto g Filter.atTop Filter.atTop) :

Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f

theorem Monotone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Filter.Tendsto g Filter.atBot Filter.atBot) :

Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f

theorem Antitone.isBoundedUnder_le_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Filter.Tendsto g Filter.atBot Filter.atTop) :

Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f

theorem Antitone.isBoundedUnder_ge_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Filter.Tendsto g Filter.atTop Filter.atBot) :

Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f

theorem GaloisConnection.l_limsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {v : α → β} {l : β → γ} {u : γ → β} (gc : GaloisConnection l u) (hlv : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => l (v x) := by isBoundedDefault) (hv_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) :

l (Filter.limsup v f) ≤ Filter.limsup (fun (x : α) => l (v x)) f

theorem OrderIso.limsup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hu_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hgu : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x) := by isBoundedDefault) (hgu_co : Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x) := by isBoundedDefault) :

g (Filter.limsup u f) = Filter.limsup (fun (x : α) => g (u x)) f

theorem OrderIso.liminf_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hu_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hgu : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x) := by isBoundedDefault) (hgu_co : Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x) := by isBoundedDefault) :

g (Filter.liminf u f) = Filter.liminf (fun (x : α) => g (u x)) f

theorem isCoboundedUnder_le_max {α : Type u_1} {β : Type u_2} [LinearOrder β] {f : Filter α} {u v : α → β} (h : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u ∨ Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) :

Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => u a ⊔ v a

theorem limsup_max {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) :

Filter.limsup (fun (a : α) => u a ⊔ v a) f = Filter.limsup u f ⊔ Filter.limsup v f

theorem liminf_min {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h₁ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v := by isBoundedDefault) :

Filter.liminf (fun (a : α) => u a ⊓ v a) f = Filter.liminf u f ⊓ Filter.liminf v f

theorem isBoundedUnder_le_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) 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} [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :

Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) 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} [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup fun (i : ι) => F i a

theorem isBoundedUnder_ge_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) 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} [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :

Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) 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} [LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) :

Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf fun (i : ι) => F i a

theorem limsup_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) :

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} [ConditionallyCompleteLinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) :

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} [ConditionallyCompleteLinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) :

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} [ConditionallyCompleteLinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) :

Filter.liminf (fun (a : α) => s.inf fun (i : ι) => F i a) f = s.inf fun (i : ι) => Filter.liminf (F i) f

theorem Monotone.frequently_ge_map_of_frequently_ge {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ (x : R) in F, l ≤ x) :

∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'

theorem Monotone.frequently_le_map_of_frequently_le {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {u : R} (freq_le : ∃ᶠ (x : R) in F, x ≤ u) :

∃ᶠ (y : S) in Filter.map f F, y ≤ f u

theorem Antitone.frequently_le_map_of_frequently_ge {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ (x : R) in F, l ≤ x) :

∃ᶠ (y : S) in Filter.map f F, y ≤ f l

theorem Antitone.frequently_ge_map_of_frequently_le {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {u : R} (frbdd : ∃ᶠ (x : R) in F, x ≤ u) :

∃ᶠ (y : S) in Filter.map f F, f u ≤ y

theorem Monotone.isCoboundedUnder_le_of_isCobounded {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F) :

Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f

theorem Monotone.isCoboundedUnder_ge_of_isCobounded {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F) :

Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f

theorem Antitone.isCoboundedUnder_le_of_isCobounded {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F) :

Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f

theorem Antitone.isCoboundedUnder_ge_of_isCobounded {R : Type u_6} {S : Type u_7} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) [F.NeBot] (cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F) :

Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f