Theory of the `tendsto` predicate

Stream: maths

[Keefer Rowan]

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]

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

[Johan Commelin]

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

[Keefer Rowan]

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]

We have stuff about frequently and eventually. I think those are close to what you want.

[Johan Commelin]

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

[Keefer Rowan]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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

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]

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

[Yury G. Kudryashov]

But I think that these two filters are equal.

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Jeremy Avigad]

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

[Reid Barton]

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]

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]

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