liminfs and limsups of functions and filters
Defines the Liminf/Limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.
We define f.Limsup (f.Liminf) where f is a filter taking values in a conditionally complete
lattice. f.Limsup is the smallest element a such that, eventually, u ≤ a (and vice versa for
f.Liminf). To work with the Limsup along a function u use (f.map u).Limsup.
Usually, one defines the Limsup as Inf (Sup s) where the Inf is taken over all sets in the filter.
For instance, in ℕ along a function u, this is Inf_n (Sup_{k ≥ n} u k) (and the latter quantity
decreases with n, so this is in fact a limit.). There is however a difficulty: it is well possible
that u is not bounded on the whole space, only eventually (think of Limsup (λx, 1/x) on ℝ. Then
there is no guarantee that the quantity above really decreases (the value of the Sup beforehand is
not really well defined, as one can not use ∞), so that the Inf could be anything. So one can not
use this Inf Sup ... definition in conditionally complete lattices, and one has to use a less
tractable definition.
In conditionally complete lattices, the definition is only useful for filters which are eventually bounded above (otherwise, the Limsup would morally be +∞, which does not belong to the space) and which are frequently bounded below (otherwise, the Limsup would morally be -∞, which is not in the space either). We start with definitions of these concepts for arbitrary filters, before turning to the definitions of Limsup and Liminf.
In complete lattices, however, it coincides with the Inf Sup definition.
f.is_bounded (≺): the filter f is eventually bounded w.r.t. the relation ≺, i.e.
eventually, it is bounded by some uniform bound.
r will be usually instantiated with ≤ or ≥.
Equations
- filter.is_bounded r f = ∃ (b : α), ∀ᶠ (x : α) in f, r x b
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)
f is eventually bounded if and only if, there exists an admissible set on which it is
bounded.
A bounded function u is in particular eventually bounded.
is_cobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is
also called frequently bounded. Will be usually instantiated with ≤ or ≥.
There is a subtlety in this definition: we want f.is_cobounded to hold for any f in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
¬ ∀ a, ∀ᶠ n in f, a ≤ n
would not work as well in this case.
Equations
- filter.is_cobounded r f = ∃ (b : α), ∀ (a : α), (∀ᶠ (x : α) in f, r x a) → r b a
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)
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.
A filter which is eventually bounded is in particular frequently bounded (in the opposite direction). At least if the filter is not trivial.
Filters are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic is_bounded_default in the statements,
in the form (hf : f.is_bounded (≥) . is_bounded_default).
The Limsup of a filter f is the infimum of the a such that, eventually for f,
holds x ≤ a.
Equations
- f.Limsup = has_Inf.Inf {a : α | ∀ᶠ (n : α) in f, n ≤ a}
The Liminf of a filter f is the supremum of the a such that, eventually for f,
holds x ≥ a.
Equations
- f.Liminf = has_Sup.Sup {a : α | ∀ᶠ (n : α) in f, a ≤ n}
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
- f.limsup u = (filter.map u f).Limsup
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
- f.liminf u = (filter.map u f).Liminf
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
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