How can one represent Calculus limits using filters?

Stream: Is there code for X?

[Formally Verified Waffle Maker]

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 $\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.

[Floris van Doorn]

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

[Floris van Doorn]

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.

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Formally Verified Waffle Maker]

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.

[Formally Verified Waffle Maker]

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.

[Johan Commelin]

@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

[Bryan Gin-ge Chen]

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]

[Bryan Gin-ge Chen]

Though maybe this is overkill.

[Floris van Doorn]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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?

[Patrick Massot]

docs#compact_space_uniformity

[Patrick Massot]

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

[Patrick Massot]

docs#is_closed.compact

[Patrick Massot]

docs#is_compact.is_closed

[Patrick Massot]

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.