Zulip Chat Archive

Stream: new members

Topic: Filters


view this post on Zulip Valery Isaev (May 12 2020 at 00:22):

I heard that analysis and topology in Lean is implemented using filters which are supposed to be more convenient from formalization point of view. I'd like to know what are advantages of this approach compared to the ordinary way of doing things.

view this post on Zulip Johan Commelin (May 12 2020 at 04:46):

@Valery Isaev Patrick wrote a nice short discussion in our perfectoid paper: https://math.commelin.net/files/poplws20cpp_perfectoid.pdf

view this post on Zulip Johan Commelin (May 12 2020 at 04:47):

You will want section 4

view this post on Zulip Kevin Buzzard (May 12 2020 at 06:08):

I think Johannes Hoelzl ported a lot of the basic results from Isabelle, following a book by I James. Hoelzl might well have written the Isabelle code as well

view this post on Zulip Patrick Massot (May 12 2020 at 09:39):

The first step is to read the module docstring at https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html. Then indeed there should be stuff in the perfectoid paper (I already started to forgot what's in there exactly). The book by James is "Topologies and uniformities". PM me if you have difficulties finding it

view this post on Zulip Rob Lewis (May 12 2020 at 09:40):

I see a badly formed doc string there!

view this post on Zulip Patrick Massot (May 12 2020 at 09:40):

Also note that the new book Mathematics in Lean will eventually contain explanations about you need to know here

view this post on Zulip Patrick Massot (May 12 2020 at 09:41):

Rob Lewis said:

I see a badly formed doc string there!

Probably a bad space again

view this post on Zulip Valery Isaev (May 12 2020 at 22:50):

Thanks for the references. If I understand correctly, the advantage is that various notions of limits are defined in terms of filters and hence the same lemmas and definitions can be used to establish the basic theory for them.

view this post on Zulip Kevin Buzzard (May 12 2020 at 23:26):

As a mathematician the advantages I see to filters are pretty much what you say: I can say "this sequence of reals tends to 7", "this sequence of reals diverges to +infinity", "this continuous function of x tends to 7 as x tends to 37", "this continuous function tends to 0 as x tends to -infinity" etc. But my impression is that there are other advantages too.

view this post on Zulip Kevin Buzzard (May 12 2020 at 23:26):

Note in particular this very general "tendsto" predicate; I think that this was one of the key insights.


Last updated: May 06 2021 at 22:13 UTC