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

1. 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: Jun 22 2024 at 14:01 UTC