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?

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

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

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

Indeed 2 looks like the whole space is bounded.

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