Intuition behind Filter notation

Stream: mathlib4

[Enrico Borba]

Can someone explain the decision behind:

∀ᶠ x in f, p x := f.Eventually p
∃ᶠ x in f, p x := f.Frequently p

Some specific points of confusion on my part:

• neither quantifier (∀ nor ∃) appears in the definition of either of the filter-specific symbols
• "eventually" to me sounds like there _exists_ some large enough x such that p holds, therefore implying an existential quantifier (but ∀ᶠ is used here)
• "frequently" to me sounds like there are points arbitrarily close to wherever this filter is going, which while not sounding like a "forall" it also doesn't sound quite like an "exists".

[Mario Carneiro]

"eventually" to me sounds like there _exists_ some large enough x such that p holds, therefore implying an existential quantifier (but ∀ᶠ is used here)

It's not that there exists some large enough x such that p holds, it's that there exists a large enough x such that p always holds thereafter. So it's an exists-forall statement, but the sentiment is of a forall statement where you ignore the early exceptions

[Mario Carneiro]

"frequently" to me sounds like there are points arbitrarily close to wherever this filter is going, which while not sounding like a "forall" it also doesn't sound quite like an "exists".

Frequently has the idea of a recurrence, there is a value where p holds and then another one after that and so on; no matter how far along you go there is always another point later where p holds. Besides being the formal dual of Eventually which justifies the use of exists, you can also read it as "an exists statement which is robust under ignoring early exceptions". Formally this is a forall-exists statement

[Ruben Van de Velde]

I wonder if we should put something like that explanation in the docstring

[Frédéric Dupuis]

Maybe it's a bit easier to translate into ordinary language when picking a specific filter (say f = atTop). Then, ∀ᶠ x in atTop, p x means "for all x large enough, p x holds", and ∃ᶠ x in atTop, p x means "there exists an arbitrarily large x such that p x holds".

[Patrick Massot]

There is a much more direct explanation. Filters are meant to be generalizes sets, and those notation directly extend the set versions. See docs#Filter.eventually_principal and docs#Filter.frequently_principal.

[Patrick Massot]

So for instance (atTop : Filter Nat) is meant to be “the set of very large natural numbers” and ∀ᶠ n in atTop, p nsimply reads “for every n in the set of very large natural numbers, p n”, aka “for every sufficiently large n, p n”.

[Patrick Massot]

All the messy stuff with nested quantifiers is implementation details. The intuition is definitely the one suggested by the notation.

[Enrico Borba]

Patrick Massot said:

There is a much more direct explanation. Filters are meant to be generalizes sets, and those notation directly extend the set versions. See docs#Filter.eventually_principal and docs#Filter.frequently_principal.

I saw this notion in MIL, and I'm still trying to wrap my head around it. It's very nice that the filter-specific quantifier notation matches up with the principle set. Hopefully that will help my understanding.

[Richard Osborn]

One way you can uniquely identify a subset $S$ of a set $X$ is by listing all the sets in $\mathcal P(X)$ that contain $S$. A filter is just an abstraction of this notion. When people say a filter is a "generalized set", they are referring to this correspondence. In fact, the principal filters are precisely the filters that correspond to an actual subset of $X$. All other filters aren't actually "describing" a subset of $X$, but something that acts very similarly. Another potential exercise is understanding how ultrafilters can be seen as corresponding to single element subsets.

[Enrico Borba]

Richard Osborn said:

One way you can uniquely identify a subset $S$ of a set $X$ is by listing all the sets in $\mathcal P(X)$ that contain $S$. A filter is just an abstraction of this notion. When people say a filter is a "generalized set", they are referring to this correspondence. In fact, the principal filters are precisely the filters that correspond to an actual subset of $X$. All other filters aren't actually "describing" a subset of $X$, but something that acts very similarly. Another potential exercise is understanding how ultrafilters can be seen as corresponding to single element subsets.

This is just the principal filter right?

[Enrico Borba]

Whoops I see that you indeed refer to them by name in the third sentence.

[Kevin Buzzard]

It really is worth stressing the "Filter is a generalisation of a set" side of things. When a student first sees a filter they focus on the set of subsets, not realising that what they should be focussing on is the "moral intersection" of all of these sets, for example with the neighbourhood filter on a topological space the moral intersection of all the neighbourhoods of x is "x and all the numbers infinitely close to it"

[Kevin Buzzard]

All this Cauchy sequence stuff was an attempt to make Newton's ideas rigorous; but that doesn't make the original pictorial ideas worthless. Similarly, encouraging an informal understanding of filter as "subset with magic" gives great geometric intuition.

[Enrico Borba]

they should be focusing on the "moral intersection" of all of these sets

Now I think I understand better. I wasn't sure which set to imagine for an arbitrary filter, this gives me some intuition, and it matches exactly with the principal filter as well.

[Kevin Buzzard]

The filter is implemented as the collection of all regular sets which contain our magic set

[Yaël Dillies]

Personally I still don't understand what people mean by that "generalised set" business and yet I believe I have good geometrical intuition about filters

[Yaël Dillies]

Maybe the "generalised set" idea only applies to filter bases?

[Enrico Borba]

Yaël Dillies said:

Personally I still understand what people mean by that "generalised set" business and yet I believe I have good geometrical intuition about filters

Is there a "don't" missing there?

[Yaël Dillies]

Whoops, edited

[Mario Carneiro]

It kind of reminds me of nonstandard analysis, things like "function f is continuous iff for all points y infinitely close to x, f y is infinitely close to f x"

[Mario Carneiro]

nonstandard analysis is a different way of setting these things up such that being infinitely close to a point is an actual predicate so that you can read that as a real forall statement

[Mario Carneiro]

So I'm pretty sure this "generalized sets" thing actually has formal content in terms of the transfer principle

[Antoine Chambert-Loir]

Model theory provides a way to talk about this “generalized elements” (infinitesimals, ultrafilters) or “generalized sets” (filters) in a way that makes them look as a true element or a true set. The name for them is type, an unfortunate collision of words. Of course, interpretations of these objects in the initial universe makes them often empty (there is no real number $\varepsilon$ such that $0 < n\cdot \varepsilon < 1$ for all integers $n \geq 1$) but one can consider “non standard” (“saturated”…) models where these types are realized.

Constructions are possible by way of ultraproducts, and also by way of “spectra”. The set of 1-types in the language of rings (with parameters a given ring) corresponds to the prime spectrum of the base ring. The Stone-Cech compactification is another example of such a construction.

The compactness theorem says that provable statements of first order logic are those which are true in any model, but there are pairs of models (elementary equivalent extensions) which satisfy the same statements, and that is the content of the “transfer principles”.

[Jireh Loreaux]

15 years ago, I loved non-standard analysis and all these compactness arguments. However, the reason they lost their appeal for me is that they only preserve first order sentences.

Of course, you can make this behave pretty well by starting with a certain superstructure, but at some point you just want higher order things, and it's at that point that it gets very messy (e.g., distinguishing between internal and external sets, saturation principles, over/underflow, etc.).

So, while they are great for simplifying all kinds of very simple kinds of analysis arguments. It feels like the locus of complexity for more sophisticated arguments just gets shifted about, rather than actually simplified. In contrast, I don't feel the same way about filters. I honestly think they are uniformly (pun intended!) simpler.

[Antoine Chambert-Loir]

As mathlib's limit library indicates, filters mostly enter the game via the docs#Filter.Eventually and docs#Filter.Frequently quantifiers which shorten and clarify the formulas, without the need of enlarging the model to have new sets. Similarly, infinite/infinitesimals numbers in analysis appear via their corresponding filters, unless one wishes to play the game in full and, for example, study stability of ordinary differential equations using infinitesimals or even defining Riemann integrals using infinitesimals.

[Patrick Massot]

They also enter the game via direct image and inverse image. In order to express limits you don’t need eventually or frequently. You can say “the direct image under f of the set of points close to x is contained in the set of point close to y” completely as $f_*\mathcal{N}_x \le \mathcal{N}_y$. But indeed it is very much worth insisting of the fact that none of this involves non-standards models of anything or any fancy logic.

[Jireh Loreaux]

Indeed. I just had an undergraduate student who did a project developing the basic theory of filters and connecting the usual limit definitions to the filter counterparts. I carved a shortest path for this: and that really only involved principal filters, map, inf, and bases. There's no mention of eventually / frequently.

[Yury G. Kudryashov]

I added Eventually and Frequently to the library in 2020 !3#1845. Mathlib had a lot of stuff by then.
As a side effect, we have 3 ways to say that s belongs to a filter: s ∈ f, f ≤ principal s, and Filter.Eventually f fun x => x ∈ s. None of them is the simp-normal form, and different parts of the library prefer different spelling.

[Sam van G]

Just to add that the "generalized set" intuition for filters can be made rigorous with some order theory (Exercise 9.6 in Davey & Priestley 2002): Any partially ordered set $(P, \leq)$ admits a "free completion under directed infima", $F(P)$, which can be realized as the lattice of order-filters of $P$. The fact that this is the free completion under directed infima precisely tells you that an element of $F(P)$ should be thought of as a "generic way of calculating an infimum in $P$". Filters on a set $X$ are a special case: they are exactly order-filters of the poset $\mathcal{P}(X)$, and they thus represent "generic ways of calculating an intersection of subsets of $X$".

[Yaël Dillies]

I've read that book. I should have known better :face_palm:

[Anatole Dedecker]

Sam van G said:

Just to add that the "generalized set" intuition for filters can be made rigorous with some order theory (Exercise 9.6 in Davey & Priestley 2002): Any partially ordered set $(P, \leq)$ admits a "free completion under directed infima", $F(P)$, which can be realized as the lattice of order-filters of $P$. The fact that this is the free completion under directed infima precisely tells you that an element of $F(P)$ should be thought of as a "generic way of calculating an infimum in $P$". Filters on a set $X$ are a special case: they are exactly order-filters of the poset $\mathcal{P}(X)$, and they thus represent "generic ways of calculating an intersection of subsets of $X$".

Ah, I've been looking for such a result, nice to have a definitive source about it.