Zulip Chat Archive

Stream: maths

Topic: Theory of the `tendsto` predicate


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

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

view this post on Zulip Johan Commelin (May 29 2020 at 17:56):

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

view this post on Zulip 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 fnff_n \to f ptwise a.e. iff g:fng\exists g : f_n \to g ptwise and g=fg = f a.e. But it would satisfying to have this be seen of as a form of convergence in a formal way.

view this post on Zulip Johan Commelin (May 29 2020 at 18:04):

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

view this post on Zulip Johan Commelin (May 29 2020 at 18:05):

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

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

view this post on Zulip Jeremy Avigad (May 29 2020 at 18:19):

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

view this post on Zulip Kevin Buzzard (May 29 2020 at 18:19):

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

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

view this post on Zulip 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 fn(x)a.e.g(x)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 μ{xdist(fx,gx)>ε}<ε\mu\{x | \operatorname{dist}(f x, g x) > \varepsilon \} < \varepsilon.

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

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

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

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

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

But I think that these two filters are equal.

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

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

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

view this post on Zulip Reid Barton (May 29 2020 at 18:32):

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

view this post on Zulip Jeremy Avigad (May 29 2020 at 18:33):

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

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

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

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