filter at_infty

Stream: maths

[Yury G. Kudryashov]

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]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Useful for disjoint unions

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

and the picture is like a disjoint union of metric spaces

[Mario Carneiro]

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

[Kevin Buzzard]

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]

mathlib has emetric_space so it's not irrelevant

[Kevin Buzzard]

ha ha that does not surprise me :D

[Mario Carneiro]

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

[Yury G. Kudryashov]

@Mario Carneiro I wrote dist, not edist.

[Kevin Buzzard]

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

[Mario Carneiro]

you can't scale down infinitely...?

[Kevin Buzzard]

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]

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

[Mario Carneiro]

ah, yes that's true

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Another reason: limits at infinity in complex numbers.

[Mario Carneiro]

same deal

[Yury G. Kudryashov]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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