Stream: math-comp analysis

Topic: Metrics and Distance Functions

view this post on Zulip 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:

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

generates the same uniformity as ball).

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.

view this post on Zulip Pierre Roux (Feb 27 2023 at 08:01):

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

view this post on Zulip Julien Puydt (Feb 27 2023 at 08:50):

Indeed 2 looks like the whole space is bounded.

view this post on Zulip 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