Theory of filters on sets #
A filter on a type α
is a collection of sets of α
which contains the whole α
,
is upwards-closed, and is stable under intersection. They are mostly used to
abstract two related kinds of ideas:
- limits, including finite or infinite limits of sequences, finite or infinite limits of functions at a point or at infinity, etc...
- things happening eventually, including things happening for large enough
n : ℕ
, or near enough a pointx
, or for close enough pairs of points, or things happening almost everywhere in the sense of measure theory. Dually, filters can also express the idea of things happening often: for arbitrarily largen
, or at a point in any neighborhood of given a point etc...
Main definitions #
In this file, we endow Filter α
it with a complete lattice structure.
This structure is lifted from the lattice structure on Set (Set X)
using the Galois
insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to
the smallest filter containing it in the other direction.
We also prove Filter
is a monadic functor, with a push-forward operation
Filter.map
and a pull-back operation Filter.comap
that form a Galois connections for the
order on filters.
The examples of filters appearing in the description of the two motivating ideas are:
(Filter.atTop : Filter ℕ)
: made of sets ofℕ
containing{n | n ≥ N}
for someN
𝓝 x
: made of neighborhoods ofx
in a topological space (defined in topology.basic)𝓤 X
: made of entourages of a uniform space (those space are generalizations of metric spaces defined inMathlib/Topology/UniformSpace/Basic.lean
)MeasureTheory.ae
: made of sets whose complement has zero measure with respect toμ
(defined inMathlib/MeasureTheory/OuterMeasure/AE
)
The general notion of limit of a map with respect to filters on the source and target types
is Filter.Tendsto
. It is defined in terms of the order and the push-forward operation.
The predicate "happening eventually" is Filter.Eventually
, and "happening often" is
Filter.Frequently
, whose definitions are immediate after Filter
is defined (but they come
rather late in this file in order to immediately relate them to the lattice structure).
For instance, anticipating on Topology.Basic, the statement: "if a sequence u
converges to
some x
and u n
belongs to a set M
for n
large enough then x
is in the closure of
M
" is formalized as: Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M
,
which is a special case of mem_closure_of_tendsto
from Topology.Basic.
Notations #
∀ᶠ x in f, p x
:f.Eventually p
;∃ᶠ x in f, p x
:f.Frequently p
;f =ᶠ[l] g
:∀ᶠ x in l, f x = g x
;f ≤ᶠ[l] g
:∀ᶠ x in l, f x ≤ g x
;𝓟 s
:Filter.Principal s
, localized inFilter
.
References #
Important note: Bourbaki requires that a filter on X
cannot contain all sets of X
, which
we do not require. This gives Filter X
better formal properties, in particular a bottom element
⊥
for its lattice structure, at the cost of including the assumption
[NeBot f]
in a number of lemmas and definitions.
An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f
(e.g.,
Filter.comap
, Filter.coprod
, Filter.Coprod
, Filter.cofinite
).
GenerateSets g s
: s
is in the filter closure of g
.
- basic: ∀ {α : Type u} {g : Set (Set α)} {s : Set α}, s ∈ g → Filter.GenerateSets g s
- univ: ∀ {α : Type u} {g : Set (Set α)}, Filter.GenerateSets g Set.univ
- superset: ∀ {α : Type u} {g : Set (Set α)} {s t : Set α}, Filter.GenerateSets g s → s ⊆ t → Filter.GenerateSets g t
- inter: ∀ {α : Type u} {g : Set (Set α)} {s t : Set α}, Filter.GenerateSets g s → Filter.GenerateSets g t → Filter.GenerateSets g (s ∩ t)
Instances For
generate g
is the largest filter containing the sets g
.
Equations
- Filter.generate g = { sets := {s : Set α | Filter.GenerateSets g s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
mkOfClosure s hs
constructs a filter on α
whose elements set is exactly
s : Set (Set α)
, provided one gives the assumption hs : (generate s).sets = s
.
Equations
- Filter.mkOfClosure s hs = { sets := s, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
Galois insertion from sets of sets into filters.
Equations
- Filter.giGenerate α = { choice := fun (s : Set (Set α)) (hs : (Filter.generate s).sets ≤ s) => Filter.mkOfClosure s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Equations
- Filter.instCompleteLatticeFilter = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Either f = ⊥
or Filter.NeBot f
. This is a version of eq_or_ne
that uses Filter.NeBot
as the second alternative, to be used as an instance.
Alias of the reverse direction of Filter.principal_mono
.
Lattice equations #
There are only two filters on a Subsingleton
: ⊥
and ⊤
. If the type is empty, then they are
equal.
Equations
- ⋯ = ⋯
Equations
- Filter.instDistribLattice = DistribLattice.mk ⋯
The dual version does not hold! Filter α
is not a CompleteDistribLattice
.
Equations
- Filter.coframeMinimalAxioms = Order.Coframe.MinimalAxioms.mk ⋯
Instances For
Equations
- Filter.instCoframe = Order.Coframe.ofMinimalAxioms Filter.coframeMinimalAxioms
If f : ι → Filter α
is directed, ι
is not empty, and ∀ i, f i ≠ ⊥
, then iInf f ≠ ⊥
.
See also iInf_neBot_of_directed
for a version assuming Nonempty α
instead of Nonempty ι
.
If f : ι → Filter α
is directed, α
is not empty, and ∀ i, f i ≠ ⊥
, then iInf f ≠ ⊥
.
See also iInf_neBot_of_directed'
for a version assuming Nonempty ι
instead of Nonempty α
.
principal
equations #
Alias of the reverse direction of Filter.principal_neBot_iff
.
A special case of iInf_principal
that is safe to mark simp
.
Eventually #
Alias of Filter.Eventually.of_forall
.
Alias of Filter.eventually_all_finite
.
Alias of Filter.eventually_all_finset
.
Frequently #
Alias of Filter.Frequently.of_forall
.
Alias of the reverse direction of Filter.frequently_inf_principal
.
Alias of the forward direction of Filter.frequently_inf_principal
.
Relation “eventually equal” #
Alias of Filter.EventuallyEq.of_eq
.
Push-forwards, pull-backs, and the monad structure #
If functions m₁
and m₂
are eventually equal at a filter f
, then
they map this filter to the same filter.
The analog of kernImage
for filters. A set s
belongs to Filter.kernMap m f
if either of
the following equivalent conditions hold.
- There exists a set
t ∈ f
such thats = kernImage m t
. This is used as a definition. - There exists a set
t
such thattᶜ ∈ f
andsᶜ = m '' t
, seeFilter.mem_kernMap_iff_compl
andFilter.compl_mem_kernMap
.
This definition because it gives a right adjoint to Filter.comap
, and because it has a nice
interpretation when working with co-
filters (Filter.cocompact
, Filter.cofinite
, ...).
For example, kernMap m (cocompact α)
is the filter generated by the complements of the sets
m '' K
where K
is a compact subset of α
.
Equations
- Filter.kernMap m f = { sets := Set.kernImage m '' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
Filter
as a Monad
#
In this section we define Filter.monad
, a Monad
structure on Filter
s. This definition is not
an instance because its Seq
projection is not equal to the Filter.seq
function we use in the
Applicative
instance on Filter
.
The variables in the following lemmas are used as in this diagram:
φ
α → β
θ ↓ ↓ ψ
γ → δ
ρ
Temporary lemma that we can tag with gcongr
Temporary lemma that we can tag with gcongr
Equations
- ⋯ = ⋯