# Zulip Chat Archive

## Stream: maths

### Topic: Theory of the `tendsto` predicate

#### Keefer Rowan (May 29 2020 at 17:53):

Bourbaki only introduces limits where the "codomain filter" is the neighborhood filter of some point. Mathlib goes with a much more general `tendsto`

predicate where the codomain filter can be any filter on the codomain type of `f`

. Is there a reference where this theory is developed more fully; in particular I'm trying to think if a.e. pointwise convergence can be formulated in terms of `tendsto`

. More generally, can convergence spaces be construed as maps from `point_to_filter : \beta \to filter \beta`

so that $F \longrightarrow b$ iff `tendsto id F (point_to_filter b)`

where `F : filter \beta`

? I would be interested in thinking about these problems if the answer is unknown, but I thought I'd first check if this has been worked out already. I'm pretty sure a.e. convergence isn't done in Mathlib, but I could be wrong.

Note: It is "well-known" that a.e. pointwise convergence is non-topological, meaning it is not induced by a topology on the space of measurable functions (or more-or-less equivalently, the space of functions up to a.e. equivalence).

#### Johan Commelin (May 29 2020 at 17:55):

I think `tendsto`

was first developped by Johannes Hölzl et al for the Isabelle library. Johannes later ported it to lean.

#### Johan Commelin (May 29 2020 at 17:56):

As far as I know there is no "informal" maths text that explains it.

#### Keefer Rowan (May 29 2020 at 18:01):

I'm more or less fine with the idea, so an informal reference isn't really necessary. I was more interested to see if anyone had any thoughts on the a.e. pointwise convergence issue. Convergence spaces can be used to formalize a.e. pointwise convergence as a "sort of convergence", but can these by "tendsto"-ized? I'll think about it, but I was wondering if this has already been covered by someone. I would imagine that a.e. pointwise convergence would be something that people would want to formalize. You of course don't need to do all this as you can just stick to $f_n \to f$ ptwise a.e. iff $\exists g : f_n \to g$ ptwise and $g = f$ a.e. But it would satisfying to have this be seen of as a form of convergence in a formal way.

#### Johan Commelin (May 29 2020 at 18:04):

We have stuff about `frequently`

and `eventually`

. I think those are close to what you want.

#### Johan Commelin (May 29 2020 at 18:05):

But as you've noticed, I'm not an analyst...

#### Keefer Rowan (May 29 2020 at 18:11):

Thanks for the pointer. Those definitely would be useful for formalizing a.e. convergence but still isn't exactly what I'm thinking about. So I guess the question is still open for anyone more "analytically-inclined".

#### Jeremy Avigad (May 29 2020 at 18:19):

This paper provides a nice explanation: https://cs.vu.nl/~jhl890/pub/hoelzl2013typeclasses.pdf

#### Kevin Buzzard (May 29 2020 at 18:19):

@Patrick Massot @Sebastien Gouezel @Yury G. Kudryashov ?

#### Reid Barton (May 29 2020 at 18:25):

I think from this perspective what's going on for topological spaces is that each point has a largest (in the filter order, reverse inclusion) filter which converges to it, namely its neighborhood filter. So to check continuity of a function at a point you only have to look at what happens to these neighborhood filters, and this is what the `tendsto`

formulation encodes.

For a general convergence space you could phrase continuity as an inequality involving the "filters of convergent filters" at each point, but this isn't exactly `tendsto`

because you would need to apply `filter.map`

twice, or something.

#### Yury G. Kudryashov (May 29 2020 at 18:26):

As far as I understand,

- you can write
`∀ₘ x, tendsto (λ n, f n x) at_top (nhds (g x))`

for $f_n(x)\to_{a.e.} g(x)$; - I don't think that you can do it with one
`tendsto`

(though I have no proof at the moment, so I may be wrong); - you can use
`tendsto`

for convergence in measure because you can define "neighborhoods" of a function`f`

to be all functions`g`

such that $\mu\{x | \operatorname{dist}(f x, g x) > \varepsilon \} < \varepsilon$.

#### Keefer Rowan (May 29 2020 at 18:28):

@Reid Barton how do you mean that the nbhd filter is the largest filter that converges to the point. Isn’t the meaning of convergence tendsto relative to the nbhd filter?

#### Jeremy Avigad (May 29 2020 at 18:28):

Items one and two sound right to me, but in the third I don't think you can use the same epsilon in both places.

#### Yury G. Kudryashov (May 29 2020 at 18:29):

Why not? (if not, you can parametrize nhds with two parameters)

#### Yury G. Kudryashov (May 29 2020 at 18:29):

But I think that these two filters are equal.

#### Reid Barton (May 29 2020 at 18:31):

I mean: Given a topological space, you can turn it into a convergence space by saying that a filter "converges to" a point if it's $\le$ the neighborhood filter of that point. Then (basically by definition) the neighborhood filter of a point is the biggest filter that converges to that point.

The point of this construction is that you end up with the right notion of continuous maps: the continuous maps between the convergence spaces built from topological spaces are the continuous maps in the ordinary sense between the topological spaces.

#### Reid Barton (May 29 2020 at 18:32):

I think the answer to your question "More generally, can convergence spaces be construed..." is no: you only get what the nlab calls pretopological spaces that way.

#### Keefer Rowan (May 29 2020 at 18:32):

Note that convergence in measure can be made into a uniform space, so you can always use that

#### Reid Barton (May 29 2020 at 18:32):

In a convergence space, the "filter of convergent filters" might not be principal.

#### Jeremy Avigad (May 29 2020 at 18:33):

Oh, you are right. I take it back. I got the definition confused.

#### Reid Barton (May 29 2020 at 18:33):

and in your example I assume it's not--I'm guessing you have a generator for each measure 0 "bad" set, and you can only intersect countably many of those filters or the "bad" set will no longer be measure 0.

#### Keefer Rowan (May 29 2020 at 18:37):

I’ll have to look at it more later, but it seems that a pretopological space is exactly the most general structure under which convergence is given by tendsto and a certain generalized “nbhd filter” of each point. And the claim is that ae convergence is not pretopological, hence cant be implemented with tendsto.

#### Reid Barton (May 29 2020 at 18:37):

I'm pretty sure I got the direction of the order on filters wrong at least once above.

Last updated: May 10 2021 at 06:13 UTC