Zulip Chat Archive

Stream: Is there code for X?

Topic: How can one represent Calculus limits using filters?


view this post on Zulip Formally Verified Waffle Maker (Dec 15 2020 at 06:26):

I have been trying to learn about filters by looking at their usages in mathlib, but I still find them difficult. I was wondering how can one represent limx32x\displaystyle\lim_{x \to 3} 2x, for instance, using filters? Representing limits using filters would also serve as a great resource for beginners to Lean and mathlib.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 06:33):

Have you seen https://leanprover-community.github.io/theories/topology.html ?

view this post on Zulip Floris van Doorn (Dec 15 2020 at 06:34):

The default way to talk about filters in mathlib is the predicate that a limit is a certain value. This is called docs#filter.tendsto.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 06:35):

With that, you can represent your instance (over the reals) as

import analysis.specific_limits

open filter
example : tendsto (λ x : , 2 * x) (nhds 3) (nhds 6) :=
sorry

docs#nhds is the neighborhood filter.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 06:36):

Or if you want to be fancy

import analysis.specific_limits

open filter
open_locale topological_space
example : tendsto (λ x : , 2 * x) (𝓝 2) (𝓝 6) :=
sorry

view this post on Zulip Formally Verified Waffle Maker (Dec 15 2020 at 06:37):

Floris van Doorn said:

With that, you can represent your instance (over the reals) as

import analysis.specific_limits

open filter
example : tendsto (λ x : , 2 * x) (nhds 3) (nhds 6) :=
sorry

docs#nhds is the neighborhood filter.

Thank you so much. Since the limit example you gave really helped, I think beginners to Lean would find it very helpful if that was added to the official documentation.

view this post on Zulip Formally Verified Waffle Maker (Dec 15 2020 at 06:42):

And I am open to helping write documentation for beginners to Lean who know Calculus, if that is something that the Lean community is interested in.

view this post on Zulip Johan Commelin (Dec 15 2020 at 06:46):

@Formally Verified Waffle Maker sure! you could make a PR that adds

## Example

Filters can be used to represent limits as follows ... blabla
```
import analysis.specific_limits

open filter
example : tendsto (λ x : ℝ, 2 * x) (nhds 3) (nhds 6) :=
sorry
```

to the module docstring at the top of https://leanprover-community.github.io/mathlib_docs/topology/basic.html

view this post on Zulip Bryan Gin-ge Chen (Dec 15 2020 at 06:49):

P.S. the proof of the example is not too hard with a few tactics:

import analysis.specific_limits

open filter
example : tendsto (λ x : , 2 * x) (nhds 3) (nhds 6) :=
by convert continuous.tendsto _ _; [norm_num, continuity]

view this post on Zulip Bryan Gin-ge Chen (Dec 15 2020 at 06:50):

Though maybe this is overkill.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 06:58):

I made a PR here: leanprover-community/leanprover-community.github.io#151

view this post on Zulip Patrick Massot (Dec 15 2020 at 08:37):

You can also watch https://www.youtube.com/watch?v=hhOPRaR3tx0&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N&index=16

view this post on Zulip Patrick Massot (Dec 15 2020 at 08:37):

I still intend to write the corresponding chapter of MIL one day.

view this post on Zulip Patrick Massot (Dec 15 2020 at 08:45):

I've started an experiment about this. This year I'm officially teaching an algebra course to very good third year students (at ENS Paris-Saclay). These students are frustrated because their curriculum doesn't include a proper course in general topology (they have a detailed course about metric spaces spaces). Some of them repeatedly asked me to teach them general topology. Last week I accepted and gave a first underground topology course by night on our BigBlueButton server. It means I'm totally free to teach it my way and students are free to leave at any time. I couldn't resist running an experiment. So, after some introduction, I started with 20 minutes about lattices and Galois connections, then I moved to filters for about one hour and only after that I defined topological spaces. I'm pretty pleased about how it went and students seemed very happy. We'll see how many come back in Week 2. I'll tell you when I'll move to uniform spaces and Bourbaki real numbers. Note that I didn't use Lean, this is a much sneakier way to sell formalized maths than what I do with my first year undergrads.

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 09:08):

This is great. You can even tell them it's the traditional French style. You should set a problem sheet in Lean with some carefully-chosen questions which are nice to do and stick it up on a github site and then make a link to the community web editor and set it as a challenge. For example could one prove step through the Tychonoff proof using ultrafilters in a painless way in Lean?

Do we have in Lean that in a compact Hausdorff space there's a unique uniform structure compatible with the topology?

My memories of the undergraduate course I took was that continuous image of compact is compact, compact subspace of Hausdorff is closed, and closed subset of compact is compact were some pretty cool theorems. I still remember the open set proofs well. Are there slick filter proofs of these?

view this post on Zulip Patrick Massot (Dec 15 2020 at 09:39):

docs#compact_space_uniformity

view this post on Zulip Patrick Massot (Dec 15 2020 at 09:40):

https://github.com/leanprover-community/mathlib/blob/a959718e33ebb02ff61ca19220d2d33e0baae314/src/topology/subset_properties.lean#L447-L460

view this post on Zulip Patrick Massot (Dec 15 2020 at 09:41):

docs#is_closed.compact

view this post on Zulip Patrick Massot (Dec 15 2020 at 09:42):

docs#is_compact.is_closed

view this post on Zulip Patrick Massot (Dec 15 2020 at 09:42):

I will cover all this of course. At some point I will probably show some Lean as well, but I didn't want to reveal all weirdness at once.


Last updated: May 07 2021 at 21:10 UTC