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 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).

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 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.

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 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.

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: Dec 20 2023 at 11:08 UTC