Zulip Chat Archive

Stream: maths

Topic: filter at_infty


view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 15:27):

Hi, do we have a filter with base "complements to balls"? If not, what would be a correct name for this filter? More precisely, I'd like to have the following:

  1. for each point, the filter "far away from here" (def away_from x := filter.comap (dist x) at_top?)
  2. the filter "away from everywhere" (def at_infty := infi away_from?)
  3. lemma away_from_eq_at_infty (x) : away_from x = at_infty
  4. For an ordered field, at_infty = sup at_top at_bot

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:50):

I think lemma (3) fails in extended metric spaces (even if you use only finite balls), because there can be points that are infinitely far away from each other, and the corresponding away_from x filters will differ from each other and at_infty

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:54):

whatever is an "extended metric space"? I don't think we have them in maths departments.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:54):

metric space with +inf as a possible value for the metric

view this post on Zulip Johan Commelin (Nov 15 2019 at 15:54):

Useful for disjoint unions

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:55):

There are plenty of examples, e.g. l^2 metric but on all sequences

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:55):

For the disjoint union you can just scale your real numbers down I guess.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:55):

and the picture is like a disjoint union of metric spaces

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:56):

the relation "distance less than infinity" is an equivalence relation that partitions the space into metric spaces

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:56):

I have no doubt that examples can be made, all I'm saying is that probably Yury is thinking about metric spaces because they are by far the more common notion.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:56):

mathlib has emetric_space so it's not irrelevant

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:56):

ha ha that does not surprise me :D

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:57):

it wasn't even my doing; thank Sebastien for that one

view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 15:57):

@Mario Carneiro I wrote dist, not edist.

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:58):

Are they ever needed? Can one get away with doing the scaling trick?

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:58):

you can't scale down infinitely...?

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:59):

I mean, if you're worried about saying "let the distance between them be N where N is larger than anything else around" then one fix is to let N be infinity, but another fix is to choose some appropriate homeo between [0,)[0,\infty) and [0,1)[0,1) and then just let NN be 2.

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 15:59):

I guess formally I'm asking whether every emetric space is homeomorphic to a metric space.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 15:59):

ah, yes that's true

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:00):

However I do now see that it might be a useful concept. I'd never heard of it until 5 minutes ago!

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:00):

the topology is generated by small balls, so you can always just put a max on the distance and get a homeo

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:00):

For the scaling thing you need to check that you preserve the triangle inequality.

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:01):

Aah, you're suggesting that we scale by sending everything >= 1 to 1.

view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 16:02):

Do I guess correctly that we don't have these filters yet? What would be good names? I mean, do they have standard names in some textbooks?

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:02):

for bounded metric spaces, the at_infty filter is trivial, as well as away_from x

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:03):

In some ways it's odd because it's looking at large distance behavior of metrics, while the topology looks at small distance behavior

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:03):

I guess @Patrick Massot is someone you could check with, but if Mario hasn't seen them then that's already evidence that they're not there.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:04):

I've never heard of the idea, but it seems reasonable enough

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:04):

You need more than an ordered field for (4) I think

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:04):

(1)nn(-1)^nn would converge for this filter :D

view this post on Zulip Kevin Buzzard (Nov 15 2019 at 16:05):

If the ordered field has a metric you might be OK. I guess a general ordered field might not.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:06):

Not sure what the best typeclasses to select from are here, but you want an ordered metric space (the field structure is not necessary), probably an orderable_space so that you know what the open sets are

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:10):

If you have a general orderable metric space, you don't know that it's not bounded (which would falsify (4) because at_top and at_bot are not trivial). If the order has no endpoints, and the metric space is also not bounded, then I think (4) is true

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:11):

I wonder if you can craft some more interesting filters using topological "ends"

view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 16:17):

@Kevin Buzzard Yes, my reason was to formalize rn±r^n→±∞ for r>1|r|>1.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:18):

Why not simply write rn|r^n|\to\infty?

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:20):

I mean, this filter is basically the preimage of the infinity filter by abs

view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 16:20):

Another reason: limits at infinity in complex numbers.

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:20):

same deal

view this post on Zulip Yury G. Kudryashov (Nov 15 2019 at 16:22):

I'd like to have lemma (3) from the list above: the preimage of at_top by dist x is the same for all x.

view this post on Zulip Reid Barton (Nov 15 2019 at 16:25):

Isn't there another version of this that's something like "away from compact sets"

view this post on Zulip Reid Barton (Nov 15 2019 at 16:25):

Basically, the neighborhood filter of the point at infinity of the one-point compactification

view this post on Zulip Reid Barton (Nov 15 2019 at 16:26):

I tend to think that this is the principled thing even when in practice it's easier to express it as "far away from the origin" or similar

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:29):

that gives the same answer as long as closed balls are compact. Hmm, how much do the other examples matter and what is the "right" answer for them?

view this post on Zulip Mario Carneiro (Nov 15 2019 at 16:32):

I think I have seen situations similar to the one you are talking about, and I would usually deal with them using a theorem such as "any bounded set is contained in a ball centered at the origin" which gets more to the heart of the matter


Last updated: May 10 2021 at 08:14 UTC