Stream: Is there code for X?

Topic: N epsilon convergence of sqnce in metric space

Keefer Rowan (May 28 2020 at 17:36):

Is there anything about N epsilon convergence of sequences in metric spaces?

Johan Commelin (May 28 2020 at 17:37):

Not so much, I guess. The preferred method is to use filters

Johan Commelin (May 28 2020 at 17:37):

About those, there is a lot

Keefer Rowan (May 28 2020 at 17:41):

Maybe it's just because I'm not familiar with filters, but it seems like it would be worth it to implement things the way an analyst would use sequences (I haven't even heard of filters until looking at Mathlib), so that proofs can be taken from analysis books and formalized. Are there advantages to using filters in metric spaces? (I could imagine advantages in the more general setting of topological spaces, as sequences aren't really that useful without things like 1st countable and whatnot).

Johan Commelin (May 28 2020 at 17:43):

You might want to hear about the experiences of other mathematicians like @Sebastien Gouezel, @Patrick Massot and @Yury G. Kudryashov

Johan Commelin (May 28 2020 at 17:43):

It's common that you haven't heard of filters.

Johan Commelin (May 28 2020 at 17:44):

Most of us hadn't

Johan Commelin (May 28 2020 at 17:45):

https://xenaproject.wordpress.com/2018/08/04/what-is-a-filter-how-some-computer-scientists-think-about-limits/ is an explanation by a mathematician of why filters are a good idea.

Keefer Rowan (May 28 2020 at 17:45):

Thanks, I'll have a look.

Johan Commelin (May 28 2020 at 17:46):

It gives a uniform way to deal with many different sorts of convergence that are usually swept under the rug

Reid Barton (May 28 2020 at 17:51):

We do have e.g. metric.tendsto_at_top to translate between filters and N-epsilon convergence

Gabriel Ebner (May 28 2020 at 17:54):

There is also is_countably_generated.tendsto_iff_seq_tendsto that translates tendsto of two general filters to limits of sequences.

Keefer Rowan (May 28 2020 at 17:57):

Those are both useful. Though I think it still seems like it would make sense to develop a self-contained body of theorems that allows the analyst to do sequences the way they're used to. It seems these theorems would be useful in proving those ones, but it still seems like such a self-contained body doesn't exist, correct?

Johan Commelin (May 28 2020 at 17:58):

No, it doesn't. You aren't the first to suggest it should. For every theorem about filters, you will probably need 5 different variants about sequences.

Keefer Rowan (May 28 2020 at 18:05):

Is that an argument against starting on such a file or is it just a pertinent observation? Is there a reason we shouldn't just prove the pertinent property of sequences every time we need it and slowly build up a topology/metric_spaces/sequences.lean file?

An observation

Sebastien Gouezel (May 28 2020 at 18:26):

Normally, all the relevant properties of sequences should already be there, although maybe in disguise. You can also have a look at the file topology/sequences.

Patrick Massot (May 28 2020 at 19:09):

@Keefer Rowan You think you don't like filters, but this is because you are lying to yourself. You're not interested in fancy topology, right? But you do care about limits of sequences with values in ℝ or ℝ². These limits can be a number, plus or minus infinity in ℝ, or simply infinity in ℝ². Sometimes you also want to says the limit is some number, but terms are (ultimately) to the left of this number. You also want to talk about limits of a function of one real variable at a point, or at plus or minus infinity. And again the limit can be a point, plus or minus infinity etc. Right? Say you care about five ways a variable can tend to something, and five ways the value can converge. That's already 25 definitions.

Of course limits compose. For instance if $\lim_{x \to x_0} f(x) = y_0$ and $\lim_{y \to y_0} g(y) = z_0$ then certainly $\lim_{x \to x_0} g(f(x)) = z_0$. And similarly, a continuous function is sequentially continuous function, etc. How many lemmas do you need then? Experts in combinatorics tell me the answer is $5 \times 5 \times 5 = 125$. Oh, oops, I suddenly remembered that you're probably also interested in limits when the variable is contrained to stay in a subset, maybe because you are extending some map defined on a dense subset. So we should double at least the first two 5s. That's now $10 \times 10 \times 5 = 500$ lemmas to state and prove. What did you say about not liking filters? It's time to choose the red pill.

Sebastien Gouezel (May 28 2020 at 19:45):

Can we have #filter for this message?

Patrick Massot (May 28 2020 at 19:51):

The plan is to have a chapter of Mathematics in Lean containing this message followed by stuff that actually help people navigating this theory in mathlib

Keefer Rowan (May 28 2020 at 19:53):

Is there a reference for filters that develops the theory. There is seemingly some nontrivial math in there that hard to follow from just reading the lean code. Any book/note recommendations?

Bourbaki?

Keefer Rowan (May 28 2020 at 19:54):

Bourbaki topology?

Yury G. Kudryashov (May 29 2020 at 00:13):

@Patrick Massot you have a typo in your "limits compose" example. Usually $\lim_{x\to a}f(x) = b$ means tendsto f (nhds_within a (-{a})) (nhds b), so these two limits don't compose.

Yury G. Kudryashov (May 29 2020 at 05:11):

BTW, then you want to formalize, e.g., integrals, so you need $\lim_{f(x)\to 0}g(x)$ where $x=(x_0, \dots, x_n)$.

Sebastien Gouezel (May 29 2020 at 07:33):

This is a bad definition of limit. I think for Patrick (and for anyone reasonable), $\lim_{x\to a}f(x) = b$ means tendsto f (nhds a) (nhds b).

Kevin Buzzard (May 29 2020 at 07:35):

I definitely remember seeing Yury's definition in my very first analysis course, and then never again. I think there was some long discussion about this, long ago

Patrick Massot (May 29 2020 at 07:50):

Note also that using filters greatly clarify this question, since you explicitly say which source filter you are using.

Kenny Lau (May 29 2020 at 07:53):

maybe that -{a} definition is reserved for functions \R \to \R

Mario Carneiro (May 29 2020 at 07:54):

Indeed, in intro analysis class they make a big deal about the fact that the limit exists and is not equal to the function at a removable singularity

Mario Carneiro (May 29 2020 at 07:54):

with the tendsto f (nhds a) (nhds b) definition you basically can never have removable singularities

Mario Carneiro (May 29 2020 at 07:55):

(that said this is obviously the better definition)

Kenny Lau (May 29 2020 at 07:55):

afaik the reason for this is that the function may not be defined at the point of limit, such as sin(x)/x

Kenny Lau (May 29 2020 at 07:56):

so in order for the statement $\lim_{x \to 0} \frac{\sin x}x = 1$ to make sense, we must employ the "worse" definition of limit

Kenny Lau (May 29 2020 at 07:56):

(even worse, we must allow functions not defined everywhere)

Sebastien Gouezel (May 29 2020 at 07:58):

Otherwise, you just write $\lim_{\substack{x \to 0\\ x \ne 0}} \frac{\sin x}x = 1$ and you avoid all ambiguities.

Yury G. Kudryashov (May 29 2020 at 10:09):

I think that I wrote $\lim_{x\to a} f(x)$ for a function undefined at a in more than one paper. Anyway, it's definitely more clear with filters.

Last updated: May 07 2021 at 22:14 UTC