N epsilon convergence of sqnce in metric space

Stream: Is there code for X?

[Keefer Rowan]

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

[Johan Commelin]

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

[Johan Commelin]

About those, there is a lot

[Keefer Rowan]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Most of us hadn't

[Johan Commelin]

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]

Thanks, I'll have a look.

[Johan Commelin]

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

[Reid Barton]

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

[Gabriel Ebner]

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

[Keefer Rowan]

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]

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]

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?

[Johan Commelin]

An observation

[Sebastien Gouezel]

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]

@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]

Can we have #filter for this message?

[Patrick Massot]

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]

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?

[Johan Commelin]

Bourbaki?

[Keefer Rowan]

Bourbaki topology?

[Yury G. Kudryashov]

@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]

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]

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]

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]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

(that said this is obviously the better definition)

[Kenny Lau]

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]

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]

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

[Sebastien Gouezel]

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]

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.