Zulip Chat Archive

Stream: Is there code for X?

Topic: N epsilon convergence of sqnce in metric space


view this post on Zulip Keefer Rowan (May 28 2020 at 17:36):

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

view this post on Zulip Johan Commelin (May 28 2020 at 17:37):

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

view this post on Zulip Johan Commelin (May 28 2020 at 17:37):

About those, there is a lot

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 28 2020 at 17:43):

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

view this post on Zulip Johan Commelin (May 28 2020 at 17:44):

Most of us hadn't

view this post on Zulip 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.

view this post on Zulip Keefer Rowan (May 28 2020 at 17:45):

Thanks, I'll have a look.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 28 2020 at 18:06):

An observation

view this post on Zulip 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.

view this post on Zulip 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 limxx0f(x)=y0\lim_{x \to x_0} f(x) = y_0 and limyy0g(y)=z0\lim_{y \to y_0} g(y) = z_0 then certainly limxx0g(f(x))=z0\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×5×5=1255 \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×10×5=50010 \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.

view this post on Zulip Sebastien Gouezel (May 28 2020 at 19:45):

Can we have #filter for this message?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 28 2020 at 19:54):

Bourbaki?

view this post on Zulip Keefer Rowan (May 28 2020 at 19:54):

Bourbaki topology?

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 00:13):

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

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 05:11):

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

view this post on Zulip Sebastien Gouezel (May 29 2020 at 07:33):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 29 2020 at 07:53):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 29 2020 at 07:54):

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

view this post on Zulip Mario Carneiro (May 29 2020 at 07:55):

(that said this is obviously the better definition)

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 29 2020 at 07:56):

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

view this post on Zulip Kenny Lau (May 29 2020 at 07:56):

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

view this post on Zulip Sebastien Gouezel (May 29 2020 at 07:58):

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

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 10:09):

I think that I wrote limxaf(x)\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