## Stream: maths

### Topic: filter at_infty

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

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

#### Kevin Buzzard (Nov 15 2019 at 15:54):

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

#### Mario Carneiro (Nov 15 2019 at 15:54):

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

#### Johan Commelin (Nov 15 2019 at 15:54):

Useful for disjoint unions

#### Mario Carneiro (Nov 15 2019 at 15:55):

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

#### Kevin Buzzard (Nov 15 2019 at 15:55):

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

#### Mario Carneiro (Nov 15 2019 at 15:55):

and the picture is like a disjoint union of metric spaces

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

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

#### Mario Carneiro (Nov 15 2019 at 15:56):

mathlib has emetric_space so it's not irrelevant

#### Kevin Buzzard (Nov 15 2019 at 15:56):

ha ha that does not surprise me :D

#### Mario Carneiro (Nov 15 2019 at 15:57):

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

#### Yury G. Kudryashov (Nov 15 2019 at 15:57):

@Mario Carneiro I wrote dist, not edist.

#### Kevin Buzzard (Nov 15 2019 at 15:58):

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

#### Mario Carneiro (Nov 15 2019 at 15:58):

you can't scale down infinitely...?

#### 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,\infty)$ and $[0,1)$ and then just let $N$ be 2.

#### Kevin Buzzard (Nov 15 2019 at 15:59):

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

#### Mario Carneiro (Nov 15 2019 at 15:59):

ah, yes that's true

#### 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!

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

#### Kevin Buzzard (Nov 15 2019 at 16:00):

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

#### Kevin Buzzard (Nov 15 2019 at 16:01):

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

#### 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?

#### Mario Carneiro (Nov 15 2019 at 16:02):

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

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

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

#### Mario Carneiro (Nov 15 2019 at 16:04):

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

#### Mario Carneiro (Nov 15 2019 at 16:04):

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

#### Kevin Buzzard (Nov 15 2019 at 16:04):

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

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

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

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

#### Mario Carneiro (Nov 15 2019 at 16:11):

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

#### Yury G. Kudryashov (Nov 15 2019 at 16:17):

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

#### Mario Carneiro (Nov 15 2019 at 16:18):

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

#### Mario Carneiro (Nov 15 2019 at 16:20):

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

#### Yury G. Kudryashov (Nov 15 2019 at 16:20):

Another reason: limits at infinity in complex numbers.

same deal

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

#### Reid Barton (Nov 15 2019 at 16:25):

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

#### Reid Barton (Nov 15 2019 at 16:25):

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

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

#### 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?

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