Stream: math-comp analysis

Topic: Metrics and Distance Functions

Zachary Stone (Feb 27 2023 at 00:41):

There is a tricky detail about our current definition of pseudometric in terms of ball : M -> R -> M -> Prop.
There isn't always a distance function. You'd like a distance function dist : M -> M -> R with the property that

ball x eps y <-> dist x y < eps

and you'd really like

dist x y = inf_(eps | 0 < eps) ball x eps y)

However, this is not always possible. In particular, if there is a pair of x,y : M with ball x eps y for no values of eps, you can't construct a distance that'll satisfy triangle inequality and be compatible with ball. Let me include here some context I think is relevant:

• Every metrizable uniform space has a metric which has a distance function anway. So we can always add this assumption with a wlog so long as you're only talking about [uniform] topological properties. (Turns out

limit_ball x eps y :=  if eps <= 1 then ball eps y else true

generates the same uniformity as ball).

• I'm pretty sure every pseudometric we actually define does have a corresponding metric. I'm double checking now, though.
• While it's certainly possible to construct pathological examples, I'm also fairly sure that path-connected spaces work correctly anyway. So it's rare to see the bad thing in practice.
• Having an actual distance function is sometimes essential. It comes up in the Banach Fixed Point theorem, in the proof that uniform <-> completely regular, and many other.

Ok, so what are our options?

1. One low-impact approach is to add a new axiom to pseudometric that says

ball_total x y : exists (eps : {posnum R}), ball x eps y

this is good enough to build the distance function we need.

2. A more "principled approach" is to also consider the stronger

ball_bounded : exists B, forall x y, ball x B y

Then we can add two new structures: totalPseudoMetricType and boundedPseudometricType, and prove that every "metrizable uniform structure" has all three extensions. And build some machinery to wlog add in whatever extra assumptions we need.

Any thoughts on the matter? I quite like option 2, but it dramatically benefit from waiting for HB to avoid all the awful boilerplate it would incur.

Pierre Roux (Feb 27 2023 at 08:01):

I don't grasp everything but 2. seems like a very strong hypothesis?

Julien Puydt (Feb 27 2023 at 08:50):

Indeed 2 looks like the whole space is bounded.

Zachary Stone (Feb 27 2023 at 14:08):

Yes. The result is a bit surprising. Given an unbounded metric, there is a bounded metric that generates the same topology. The limit_ball above is a simple way to achieve this. Another way to see this, recall f(x) = x/(x+1) is a continuous order isomorphism from [0,\oo) to [0,1). Given a metric d, it's straightforward to show f \o d is also a metric that generates the same topology as d

Last updated: Apr 19 2024 at 20:01 UTC