liminfs and limsups of functions and filters #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Defines the Liminf/Limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.
We define Limsup f (Liminf f) where f is a filter taking values in a conditionally complete
lattice. Limsup f is the smallest element a such that, eventually, u ≤ a (and vice versa for
Liminf f). To work with the Limsup along a function u use Limsup (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 (λ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.
f.is_bounded (≺): the filter f is eventually bounded w.r.t. the relation ≺, i.e.
eventually, it is bounded by some uniform bound.
r will be usually instantiated with ≤ or ≥.
def
filter.is_bounded_under
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(f : filter β)
(u : β → α) :
Prop
f.is_bounded_under (≺) u: the image of the filter f under u is eventually bounded w.r.t.
the relation ≺, i.e. eventually, it is bounded by some uniform bound.
Equations
- filter.is_bounded_under r f u = filter.is_bounded r (filter.map u f)
theorem
filter.is_bounded_bot
{α : Type u_1}
{r : α → α → Prop} :
filter.is_bounded r ⊥ ↔ nonempty α
theorem
filter.is_bounded_principal
{α : Type u_1}
{r : α → α → Prop}
(s : set α) :
filter.is_bounded r (filter.principal s) ↔ ∃ (t : α), ∀ (x : α), x ∈ s → r x t
theorem
filter.is_bounded_sup
{α : Type u_1}
{r : α → α → Prop}
{f g : filter α}
[is_trans α r]
(hr : ∀ (b₁ b₂ : α), ∃ (b : α), r b₁ b ∧ r b₂ b) :
filter.is_bounded r f → filter.is_bounded r g → filter.is_bounded r (f ⊔ g)
theorem
filter.is_bounded.mono
{α : Type u_1}
{r : α → α → Prop}
{f g : filter α}
(h : f ≤ g) :
filter.is_bounded r g → filter.is_bounded r f
theorem
filter.is_bounded_under.mono
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{f g : filter β}
{u : β → α}
(h : f ≤ g) :
filter.is_bounded_under r g u → filter.is_bounded_under r f u
theorem
filter.is_bounded_under.mono_le
{α : Type u_1}
{β : Type u_2}
[preorder β]
{l : filter α}
{u v : α → β}
(hu : filter.is_bounded_under has_le.le l u)
(hv : v ≤ᶠ[l] u) :
theorem
filter.is_bounded_under.mono_ge
{α : Type u_1}
{β : Type u_2}
[preorder β]
{l : filter α}
{u v : α → β}
(hu : filter.is_bounded_under ge l u)
(hv : u ≤ᶠ[l] v) :
theorem
filter.is_bounded_under_const
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
[is_refl α r]
{l : filter β}
{a : α} :
filter.is_bounded_under r l (λ (_x : β), a)
theorem
filter.is_bounded.is_bounded_under
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{f : filter α}
{q : β → β → Prop}
{u : α → β}
(hf : ∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁)) :
filter.is_bounded r f → filter.is_bounded_under q f u
theorem
filter.not_is_bounded_under_of_tendsto_at_top
{α : Type u_1}
{β : Type u_2}
[preorder β]
[no_max_order β]
{f : α → β}
{l : filter α}
[l.ne_bot]
(hf : filter.tendsto f l filter.at_top) :
theorem
filter.not_is_bounded_under_of_tendsto_at_bot
{α : Type u_1}
{β : Type u_2}
[preorder β]
[no_min_order β]
{f : α → β}
{l : filter α}
[l.ne_bot]
(hf : filter.tendsto f l filter.at_bot) :
theorem
filter.is_bounded_under.bdd_above_range_of_cofinite
{α : Type u_1}
{β : Type u_2}
[semilattice_sup β]
{f : α → β}
(hf : filter.is_bounded_under has_le.le filter.cofinite f) :
theorem
filter.is_bounded_under.bdd_below_range_of_cofinite
{α : Type u_1}
{β : Type u_2}
[semilattice_inf β]
{f : α → β}
(hf : filter.is_bounded_under ge filter.cofinite f) :
theorem
filter.is_bounded_under.bdd_above_range
{β : Type u_2}
[semilattice_sup β]
{f : ℕ → β}
(hf : filter.is_bounded_under has_le.le filter.at_top f) :
theorem
filter.is_bounded_under.bdd_below_range
{β : Type u_2}
[semilattice_inf β]
{f : ℕ → β}
(hf : filter.is_bounded_under ge filter.at_top f) :
is_cobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is
also called frequently bounded. Will be usually instantiated with ≤ or ≥.
There is a subtlety in this definition: we want f.is_cobounded to hold for any f in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
¬ ∀ a, ∀ᶠ n in f, a ≤ n
would not work as well in this case.
def
filter.is_cobounded_under
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(f : filter β)
(u : β → α) :
Prop
is_cobounded_under (≺) f u states that the image of the filter f under the map u does not
tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated
with ≤ or ≥.
Equations
- filter.is_cobounded_under r f u = filter.is_cobounded r (filter.map u f)
theorem
filter.is_cobounded.mk
{α : Type u_1}
{r : α → α → Prop}
{f : filter α}
[is_trans α r]
(a : α)
(h : ∀ (s : set α), s ∈ f → (∃ (x : α) (H : x ∈ s), r a x)) :
To check that a filter is frequently bounded, it suffices to have a witness
which bounds f at some point for every admissible set.
This is only an implication, as the other direction is wrong for the trivial filter.
theorem
filter.is_bounded.is_cobounded_flip
{α : Type u_1}
{r : α → α → Prop}
{f : filter α}
[is_trans α r]
[f.ne_bot] :
filter.is_bounded r f → filter.is_cobounded (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.is_bounded.is_cobounded_ge
{α : Type u_1}
{f : filter α}
[preorder α]
[f.ne_bot]
(h : filter.is_bounded has_le.le f) :
theorem
filter.is_bounded.is_cobounded_le
{α : Type u_1}
{f : filter α}
[preorder α]
[f.ne_bot]
(h : filter.is_bounded ge f) :
theorem
filter.is_cobounded.mono
{α : Type u_1}
{r : α → α → Prop}
{f g : filter α}
(h : f ≤ g) :
filter.is_cobounded r f → filter.is_cobounded r g
@[simp]
theorem
filter.is_bounded_under_le_neg
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_group α]
{l : filter β}
{u : β → α} :
filter.is_bounded_under has_le.le l (λ (x : β), -u x) ↔ filter.is_bounded_under ge l u
@[simp]
theorem
filter.is_bounded_under_le_inv
{α : Type u_1}
{β : Type u_2}
[ordered_comm_group α]
{l : filter β}
{u : β → α} :
filter.is_bounded_under has_le.le l (λ (x : β), (u x)⁻¹) ↔ filter.is_bounded_under ge l u
@[simp]
theorem
filter.is_bounded_under_ge_inv
{α : Type u_1}
{β : Type u_2}
[ordered_comm_group α]
{l : filter β}
{u : β → α} :
filter.is_bounded_under ge l (λ (x : β), (u x)⁻¹) ↔ filter.is_bounded_under has_le.le l u
@[simp]
theorem
filter.is_bounded_under_ge_neg
{α : Type u_1}
{β : Type u_2}
[ordered_add_comm_group α]
{l : filter β}
{u : β → α} :
filter.is_bounded_under ge l (λ (x : β), -u x) ↔ filter.is_bounded_under has_le.le l u
theorem
filter.is_bounded_under.sup
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{f : filter β}
{u v : β → α} :
filter.is_bounded_under has_le.le f u → filter.is_bounded_under has_le.le f v → filter.is_bounded_under has_le.le f (λ (a : β), u a ⊔ v a)
@[simp]
theorem
filter.is_bounded_under_le_sup
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
{f : filter β}
{u v : β → α} :
filter.is_bounded_under has_le.le f (λ (a : β), u a ⊔ v a) ↔ filter.is_bounded_under has_le.le f u ∧ filter.is_bounded_under has_le.le f v
theorem
filter.is_bounded_under.inf
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{f : filter β}
{u v : β → α} :
filter.is_bounded_under ge f u → filter.is_bounded_under ge f v → filter.is_bounded_under ge f (λ (a : β), u a ⊓ v a)
@[simp]
theorem
filter.is_bounded_under_ge_inf
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
{f : filter β}
{u v : β → α} :
filter.is_bounded_under ge f (λ (a : β), u a ⊓ v a) ↔ filter.is_bounded_under ge f u ∧ filter.is_bounded_under ge f v
theorem
filter.is_bounded_under_le_abs
{α : Type u_1}
{β : Type u_2}
[linear_ordered_add_comm_group α]
{f : filter β}
{u : β → α} :
filter.is_bounded_under has_le.le f (λ (a : β), |u a|) ↔ filter.is_bounded_under has_le.le f u ∧ filter.is_bounded_under ge f u
The Limsup of a filter f is the infimum of the a such that, eventually for f,
holds x ≤ a.
The Liminf of a filter f is the supremum of the a such that, eventually for f,
holds x ≥ a.
def
filter.limsup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(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).Limsup
def
filter.liminf
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(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).Liminf
def
filter.blimsup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(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 = has_Inf.Inf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}
def
filter.bliminf
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(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 = has_Sup.Sup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}
theorem
filter.limsup_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α} :
filter.limsup u f = has_Inf.Inf {a : α | ∀ᶠ (n : β) in f, u n ≤ a}
theorem
filter.liminf_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α} :
filter.liminf u f = has_Sup.Sup {a : α | ∀ᶠ (n : β) in f, a ≤ u n}
theorem
filter.blimsup_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{p : β → Prop} :
filter.blimsup u f p = has_Inf.Inf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}
theorem
filter.bliminf_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{p : β → Prop} :
filter.bliminf u f p = has_Sup.Sup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}
@[simp]
theorem
filter.blimsup_true
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(f : filter β)
(u : β → α) :
filter.blimsup u f (λ (x : β), true) = filter.limsup u f
@[simp]
theorem
filter.bliminf_true
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
(f : filter β)
(u : β → α) :
filter.bliminf u f (λ (x : β), true) = filter.liminf u f
theorem
filter.blimsup_eq_limsup_subtype
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{p : β → Prop} :
filter.blimsup u f p = filter.limsup (u ∘ coe) (filter.comap coe f)
theorem
filter.bliminf_eq_liminf_subtype
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{p : β → Prop} :
filter.bliminf u f p = filter.liminf (u ∘ coe) (filter.comap coe f)
theorem
filter.Limsup_le_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{f : filter α}
{a : α}
(hf : filter.is_cobounded has_le.le f . "is_bounded_default")
(h : ∀ᶠ (n : α) in f, n ≤ a) :
theorem
filter.le_Liminf_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{f : filter α}
{a : α}
(hf : filter.is_cobounded ge f . "is_bounded_default")
(h : ∀ᶠ (n : α) in f, a ≤ n) :
theorem
filter.limsup_le_of_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{a : α}
(hf : filter.is_cobounded_under has_le.le f u . "is_bounded_default")
(h : ∀ᶠ (n : β) in f, u n ≤ a) :
filter.limsup u f ≤ a
theorem
filter.le_liminf_of_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{a : α}
(hf : filter.is_cobounded_under ge f u . "is_bounded_default")
(h : ∀ᶠ (n : β) in f, a ≤ u n) :
a ≤ filter.liminf u f
theorem
filter.le_limsup_of_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{a : α}
(hf : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(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}
[conditionally_complete_lattice α]
{f : filter β}
{u : β → α}
{a : α}
(hf : filter.is_bounded_under ge f u . "is_bounded_default")
(h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a) :
filter.liminf u f ≤ a
theorem
filter.Liminf_le_Limsup
{α : Type u_1}
[conditionally_complete_lattice α]
{f : filter α}
[f.ne_bot]
(h₁ : filter.is_bounded has_le.le f . "is_bounded_default")
(h₂ : filter.is_bounded ge f . "is_bounded_default") :
theorem
filter.liminf_le_limsup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice α]
{f : filter β}
[f.ne_bot]
{u : β → α}
(h : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(h' : filter.is_bounded_under ge f u . "is_bounded_default") :
filter.liminf u f ≤ filter.limsup u f
theorem
filter.Limsup_le_Limsup
{α : Type u_1}
[conditionally_complete_lattice α]
{f g : filter α}
(hf : filter.is_cobounded has_le.le f . "is_bounded_default")
(hg : filter.is_bounded has_le.le g . "is_bounded_default")
(h : ∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → (∀ᶠ (n : α) in f, n ≤ a)) :
theorem
filter.limsup_le_limsup
{β : Type u_2}
{α : Type u_1}
[conditionally_complete_lattice β]
{f : filter α}
{u v : α → β}
(h : u ≤ᶠ[f] v)
(hu : filter.is_cobounded_under has_le.le f u . "is_bounded_default")
(hv : filter.is_bounded_under has_le.le f v . "is_bounded_default") :
filter.limsup u f ≤ filter.limsup v f
theorem
filter.liminf_le_liminf
{β : Type u_2}
{α : Type u_1}
[conditionally_complete_lattice β]
{f : filter α}
{u v : α → β}
(h : ∀ᶠ (a : α) in f, u a ≤ v a)
(hu : filter.is_bounded_under ge f u . "is_bounded_default")
(hv : filter.is_cobounded_under ge f v . "is_bounded_default") :
filter.liminf u f ≤ filter.liminf v f
theorem
filter.Limsup_le_Limsup_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{f g : filter α}
(h : f ≤ g)
(hf : filter.is_cobounded has_le.le f . "is_bounded_default")
(hg : filter.is_bounded has_le.le g . "is_bounded_default") :
theorem
filter.Liminf_le_Liminf_of_le
{α : Type u_1}
[conditionally_complete_lattice α]
{f g : filter α}
(h : g ≤ f)
(hf : filter.is_bounded ge f . "is_bounded_default")
(hg : filter.is_cobounded ge g . "is_bounded_default") :
theorem
filter.limsup_le_limsup_of_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice β]
{f g : filter α}
(h : f ≤ g)
{u : α → β}
(hf : filter.is_cobounded_under has_le.le f u . "is_bounded_default")
(hg : filter.is_bounded_under has_le.le g u . "is_bounded_default") :
filter.limsup u f ≤ filter.limsup u g
theorem
filter.liminf_le_liminf_of_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_lattice β]
{f g : filter α}
(h : g ≤ f)
{u : α → β}
(hf : filter.is_bounded_under ge f u . "is_bounded_default")
(hg : filter.is_cobounded_under ge g u . "is_bounded_default") :
filter.liminf u f ≤ filter.liminf u g
theorem
filter.Limsup_principal
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(h : bdd_above s)
(hs : s.nonempty) :
(filter.principal s).Limsup = has_Sup.Sup s
theorem
filter.Liminf_principal
{α : Type u_1}
[conditionally_complete_lattice α]
{s : set α}
(h : bdd_below s)
(hs : s.nonempty) :
(filter.principal s).Liminf = has_Inf.Inf s
theorem
filter.limsup_congr
{β : Type u_2}
{α : Type u_1}
[conditionally_complete_lattice β]
{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}
[conditionally_complete_lattice α]
{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}
[conditionally_complete_lattice α]
{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_1}
[conditionally_complete_lattice β]
{f : filter α}
{u v : α → β}
(h : ∀ᶠ (a : α) in f, u a = v a) :
filter.liminf u f = filter.liminf v f
theorem
filter.limsup_const
{β : Type u_2}
{α : Type u_1}
[conditionally_complete_lattice β]
{f : filter α}
[f.ne_bot]
(b : β) :
filter.limsup (λ (x : α), b) f = b
theorem
filter.liminf_const
{β : Type u_2}
{α : Type u_1}
[conditionally_complete_lattice β]
{f : filter α}
[f.ne_bot]
(b : β) :
filter.liminf (λ (x : α), b) f = b
@[simp]
theorem
filter.blimsup_false
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
filter.blimsup u f (λ (x : β), false) = ⊥
@[simp]
theorem
filter.bliminf_false
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
filter.bliminf u f (λ (x : β), false) = ⊤
theorem
filter.limsup_const_bot
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β} :
filter.limsup (λ (x : β), ⊥) f = ⊥
Same as limsup_const applied to ⊥ but without the ne_bot f assumption
theorem
filter.liminf_const_top
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β} :
filter.liminf (λ (x : β), ⊤) f = ⊤
Same as limsup_const applied to ⊤ but without the ne_bot f assumption
theorem
filter.has_basis.Limsup_eq_infi_Sup
{α : Type u_1}
[complete_lattice α]
{ι : Sort u_2}
{p : ι → Prop}
{s : ι → set α}
{f : filter α}
(h : f.has_basis p s) :
f.Limsup = ⨅ (i : ι) (hi : p i), has_Sup.Sup (s i)
theorem
filter.has_basis.Liminf_eq_supr_Inf
{α : Type u_1}
{ι : Type u_4}
[complete_lattice α]
{p : ι → Prop}
{s : ι → set α}
{f : filter α}
(h : f.has_basis p s) :
f.Liminf = ⨆ (i : ι) (hi : p i), has_Inf.Inf (s i)
theorem
filter.limsup_le_supr
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
filter.limsup u f ≤ ⨆ (n : β), u n
theorem
filter.infi_le_liminf
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
(⨅ (n : β), u n) ≤ filter.liminf u f
theorem
filter.limsup_eq_infi_supr
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
In a complete lattice, the limsup of a function is the infimum over sets s in the filter
of the supremum of the function over s
theorem
filter.limsup_eq_infi_supr_of_nat
{α : Type u_1}
[complete_lattice α]
{u : ℕ → α} :
filter.limsup u filter.at_top = ⨅ (n : ℕ), ⨆ (i : ℕ) (H : i ≥ n), u i
theorem
filter.limsup_eq_infi_supr_of_nat'
{α : Type u_1}
[complete_lattice α]
{u : ℕ → α} :
filter.limsup u filter.at_top = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)
theorem
filter.blimsup_congr'
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{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}
[complete_lattice α]
{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.blimsup_eq_infi_bsupr_of_nat
{α : Type u_1}
[complete_lattice α]
{p : ℕ → Prop}
{u : ℕ → α} :
theorem
filter.liminf_eq_supr_infi
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{u : β → α} :
In a complete lattice, the liminf of a function is the infimum over sets s in the filter
of the supremum of the function over s
theorem
filter.liminf_eq_supr_infi_of_nat
{α : Type u_1}
[complete_lattice α]
{u : ℕ → α} :
filter.liminf u filter.at_top = ⨆ (n : ℕ), ⨅ (i : ℕ) (H : i ≥ n), u i
theorem
filter.liminf_eq_supr_infi_of_nat'
{α : Type u_1}
[complete_lattice α]
{u : ℕ → α} :
filter.liminf u filter.at_top = ⨆ (n : ℕ), ⨅ (i : ℕ), u (i + n)
theorem
filter.bliminf_eq_supr_binfi_of_nat
{α : Type u_1}
[complete_lattice α]
{p : ℕ → Prop}
{u : ℕ → α} :
theorem
filter.limsup_eq_Inf_Sup
{ι : Type u_1}
{R : Type u_2}
(F : filter ι)
[complete_lattice R]
(a : ι → R) :
filter.limsup a F = has_Inf.Inf ((λ (I : set ι), has_Sup.Sup (a '' I)) '' F.sets)
theorem
filter.liminf_eq_Sup_Inf
{ι : Type u_1}
{R : Type u_2}
(F : filter ι)
[complete_lattice R]
(a : ι → R) :
filter.liminf a F = has_Sup.Sup ((λ (I : set ι), has_Inf.Inf (a '' I)) '' F.sets)
@[simp]
theorem
filter.liminf_nat_add
{α : Type u_1}
[complete_lattice α]
(f : ℕ → α)
(k : ℕ) :
filter.liminf (λ (i : ℕ), f (i + k)) filter.at_top = filter.liminf f filter.at_top
@[simp]
theorem
filter.limsup_nat_add
{α : Type u_1}
[complete_lattice α]
(f : ℕ → α)
(k : ℕ) :
filter.limsup (λ (i : ℕ), f (i + k)) filter.at_top = filter.limsup f filter.at_top
theorem
filter.liminf_le_of_frequently_le'
{α : Type u_1}
{β : Type u_2}
[complete_lattice β]
{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_1}
{β : Type u_2}
[complete_lattice β]
{f : filter α}
{u : α → β}
{x : β}
(h : ∃ᶠ (a : α) in f, x ≤ u a) :
x ≤ filter.limsup u f
@[simp]
theorem
filter.complete_lattice_hom.apply_limsup_iterate
{α : Type u_1}
[complete_lattice α]
(f : complete_lattice_hom α α)
(a : α) :
⇑f (filter.limsup (λ (n : ℕ), ⇑f^[n] a) filter.at_top) = filter.limsup (λ (n : ℕ), ⇑f^[n] a) filter.at_top
If f : α → α is a morphism of complete lattices, then the limsup of its iterates of any
a : α is a fixed point.
theorem
filter.complete_lattice_hom.apply_liminf_iterate
{α : Type u_1}
[complete_lattice α]
(f : complete_lattice_hom α α)
(a : α) :
⇑f (filter.liminf (λ (n : ℕ), ⇑f^[n] a) filter.at_top) = filter.liminf (λ (n : ℕ), ⇑f^[n] a) filter.at_top
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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{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}
[complete_lattice α]
{f g : filter β}
{p : β → Prop}
{u : β → α}
(h : f ≤ g) :
filter.blimsup u f p ≤ filter.blimsup u g p
@[simp]
theorem
filter.blimsup_and_le_inf
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.blimsup u f (λ (x : β), p x ∧ q x) ≤ filter.blimsup u f p ⊓ filter.blimsup u f q
@[simp]
theorem
filter.bliminf_sup_le_and
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.bliminf u f p ⊔ filter.bliminf u f q ≤ filter.bliminf u f (λ (x : β), p x ∧ q x)
@[simp]
theorem
filter.blimsup_sup_le_or
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.blimsup u f p ⊔ filter.blimsup u f q ≤ filter.blimsup u f (λ (x : β), p x ∨ q x)
See also filter.blimsup_or_eq_sup.
@[simp]
theorem
filter.bliminf_or_le_inf
{α : Type u_1}
{β : Type u_2}
[complete_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.bliminf u f (λ (x : β), p x ∨ q x) ≤ filter.bliminf u f p ⊓ filter.bliminf u f q
See also filter.bliminf_or_eq_inf.
theorem
filter.order_iso.apply_blimsup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice α]
{f : filter β}
{p : β → Prop}
{u : β → α}
[complete_lattice γ]
(e : α ≃o γ) :
⇑e (filter.blimsup u f p) = filter.blimsup (⇑e ∘ u) f p
theorem
filter.order_iso.apply_bliminf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice α]
{f : filter β}
{p : β → Prop}
{u : β → α}
[complete_lattice γ]
(e : α ≃o γ) :
⇑e (filter.bliminf u f p) = filter.bliminf (⇑e ∘ u) f p
theorem
filter.Sup_hom.apply_blimsup_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice α]
{f : filter β}
{p : β → Prop}
{u : β → α}
[complete_lattice γ]
(g : Sup_hom α γ) :
⇑g (filter.blimsup u f p) ≤ filter.blimsup (⇑g ∘ u) f p
theorem
filter.Inf_hom.le_apply_bliminf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[complete_lattice α]
{f : filter β}
{p : β → Prop}
{u : β → α}
[complete_lattice γ]
(g : Inf_hom α γ) :
filter.bliminf (⇑g ∘ u) f p ≤ ⇑g (filter.bliminf u f p)
@[simp]
theorem
filter.blimsup_or_eq_sup
{α : Type u_1}
{β : Type u_2}
[complete_distrib_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.blimsup u f (λ (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}
[complete_distrib_lattice α]
{f : filter β}
{p q : β → Prop}
{u : β → α} :
filter.bliminf u f (λ (x : β), p x ∨ q x) = filter.bliminf u f p ⊓ filter.bliminf u f q
theorem
filter.sup_limsup
{α : Type u_1}
{β : Type u_2}
[complete_distrib_lattice α]
{f : filter β}
{u : β → α}
[f.ne_bot]
(a : α) :
a ⊔ filter.limsup u f = filter.limsup (λ (x : β), a ⊔ u x) f
theorem
filter.inf_liminf
{α : Type u_1}
{β : Type u_2}
[complete_distrib_lattice α]
{f : filter β}
{u : β → α}
[f.ne_bot]
(a : α) :
a ⊓ filter.liminf u f = filter.liminf (λ (x : β), a ⊓ u x) f
theorem
filter.sup_liminf
{α : Type u_1}
{β : Type u_2}
[complete_distrib_lattice α]
{f : filter β}
{u : β → α}
(a : α) :
a ⊔ filter.liminf u f = filter.liminf (λ (x : β), a ⊔ u x) f
theorem
filter.inf_limsup
{α : Type u_1}
{β : Type u_2}
[complete_distrib_lattice α]
{f : filter β}
{u : β → α}
(a : α) :
a ⊓ filter.limsup u f = filter.limsup (λ (x : β), a ⊓ u x) f
theorem
filter.limsup_compl
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α) :
(filter.limsup u f)ᶜ = filter.liminf (has_compl.compl ∘ u) f
theorem
filter.liminf_compl
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α) :
(filter.liminf u f)ᶜ = filter.limsup (has_compl.compl ∘ u) f
theorem
filter.limsup_sdiff
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α)
(a : α) :
filter.limsup u f \ a = filter.limsup (λ (b : β), u b \ a) f
theorem
filter.liminf_sdiff
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α)
[f.ne_bot]
(a : α) :
filter.liminf u f \ a = filter.liminf (λ (b : β), u b \ a) f
theorem
filter.sdiff_limsup
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α)
[f.ne_bot]
(a : α) :
a \ filter.limsup u f = filter.liminf (λ (b : β), a \ u b) f
theorem
filter.sdiff_liminf
{α : Type u_1}
{β : Type u_2}
[complete_boolean_algebra α]
(f : filter β)
(u : β → α)
(a : α) :
a \ filter.liminf u f = filter.limsup (λ (b : β), a \ u b) f
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.frequently_lt_of_lt_Limsup
{α : Type u_1}
{f : filter α}
[conditionally_complete_linear_order α]
{a : α}
(hf : filter.is_cobounded has_le.le f . "is_bounded_default")
(h : a < f.Limsup) :
theorem
filter.frequently_lt_of_Liminf_lt
{α : Type u_1}
{f : filter α}
[conditionally_complete_linear_order α]
{a : α}
(hf : filter.is_cobounded ge f . "is_bounded_default")
(h : f.Liminf < a) :
theorem
filter.eventually_lt_of_lt_liminf
{α : Type u_1}
{β : Type u_2}
{f : filter α}
[conditionally_complete_linear_order β]
{u : α → β}
{b : β}
(h : b < filter.liminf u f)
(hu : filter.is_bounded_under ge f u . "is_bounded_default") :
theorem
filter.eventually_lt_of_limsup_lt
{α : Type u_1}
{β : Type u_2}
{f : filter α}
[conditionally_complete_linear_order β]
{u : α → β}
{b : β}
(h : filter.limsup u f < b)
(hu : filter.is_bounded_under has_le.le f u . "is_bounded_default") :
theorem
filter.le_limsup_of_frequently_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{f : filter α}
{u : α → β}
{b : β}
(hu_le : ∃ᶠ (x : α) in f, b ≤ u x)
(hu : filter.is_bounded_under has_le.le f u . "is_bounded_default") :
b ≤ filter.limsup u f
theorem
filter.liminf_le_of_frequently_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{f : filter α}
{u : α → β}
{b : β}
(hu_le : ∃ᶠ (x : α) in f, u x ≤ b)
(hu : filter.is_bounded_under ge f u . "is_bounded_default") :
filter.liminf u f ≤ b
theorem
filter.frequently_lt_of_lt_limsup
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{f : filter α}
{u : α → β}
{b : β}
(hu : filter.is_cobounded_under has_le.le f u . "is_bounded_default")
(h : b < filter.limsup u f) :
theorem
filter.frequently_lt_of_liminf_lt
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order β]
{f : filter α}
{u : α → β}
{b : β}
(hu : filter.is_cobounded_under ge f u . "is_bounded_default")
(h : filter.liminf u f < b) :
theorem
monotone.is_bounded_under_le_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[nonempty β]
[linear_order β]
[preorder γ]
[no_max_order γ]
{g : β → γ}
{f : α → β}
{l : filter α}
(hg : monotone g)
(hg' : filter.tendsto g filter.at_top filter.at_top) :
filter.is_bounded_under has_le.le l (g ∘ f) ↔ filter.is_bounded_under has_le.le l f
theorem
monotone.is_bounded_under_ge_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[nonempty β]
[linear_order β]
[preorder γ]
[no_min_order γ]
{g : β → γ}
{f : α → β}
{l : filter α}
(hg : monotone g)
(hg' : filter.tendsto g filter.at_bot filter.at_bot) :
filter.is_bounded_under ge l (g ∘ f) ↔ filter.is_bounded_under ge l f
theorem
antitone.is_bounded_under_le_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[nonempty β]
[linear_order β]
[preorder γ]
[no_max_order γ]
{g : β → γ}
{f : α → β}
{l : filter α}
(hg : antitone g)
(hg' : filter.tendsto g filter.at_bot filter.at_top) :
filter.is_bounded_under has_le.le l (g ∘ f) ↔ filter.is_bounded_under ge l f
theorem
antitone.is_bounded_under_ge_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[nonempty β]
[linear_order β]
[preorder γ]
[no_min_order γ]
{g : β → γ}
{f : α → β}
{l : filter α}
(hg : antitone g)
(hg' : filter.tendsto g filter.at_top filter.at_bot) :
filter.is_bounded_under ge l (g ∘ f) ↔ filter.is_bounded_under has_le.le l f
theorem
galois_connection.l_limsup_le
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[conditionally_complete_lattice β]
[conditionally_complete_lattice γ]
{f : filter α}
{v : α → β}
{l : β → γ}
{u : γ → β}
(gc : galois_connection l u)
(hlv : filter.is_bounded_under has_le.le f (λ (x : α), l (v x)) . "is_bounded_default")
(hv_co : filter.is_cobounded_under has_le.le f v . "is_bounded_default") :
l (filter.limsup v f) ≤ filter.limsup (λ (x : α), l (v x)) f
theorem
order_iso.limsup_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[conditionally_complete_lattice β]
[conditionally_complete_lattice γ]
{f : filter α}
{u : α → β}
(g : β ≃o γ)
(hu : filter.is_bounded_under has_le.le f u . "is_bounded_default")
(hu_co : filter.is_cobounded_under has_le.le f u . "is_bounded_default")
(hgu : filter.is_bounded_under has_le.le f (λ (x : α), ⇑g (u x)) . "is_bounded_default")
(hgu_co : filter.is_cobounded_under has_le.le f (λ (x : α), ⇑g (u x)) . "is_bounded_default") :
⇑g (filter.limsup u f) = filter.limsup (λ (x : α), ⇑g (u x)) f
theorem
order_iso.liminf_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[conditionally_complete_lattice β]
[conditionally_complete_lattice γ]
{f : filter α}
{u : α → β}
(g : β ≃o γ)
(hu : filter.is_bounded_under ge f u . "is_bounded_default")
(hu_co : filter.is_cobounded_under ge f u . "is_bounded_default")
(hgu : filter.is_bounded_under ge f (λ (x : α), ⇑g (u x)) . "is_bounded_default")
(hgu_co : filter.is_cobounded_under ge f (λ (x : α), ⇑g (u x)) . "is_bounded_default") :
⇑g (filter.liminf u f) = filter.liminf (λ (x : α), ⇑g (u x)) f