EMetricSpace is broken

Stream: mathlib4

[Floris van Doorn]

I believe that our current definition of docs#EMetricSpace is broken (same with docs#PseudoEMetricSpace). We require that the topology (and uniformity) of the space is defined by the distance. In particular, points with distance ∞ from every other point must be isolated points.

I think this is highly undesirable in practice. For example, ℝ≥0∞ is not an EMetricSpace, since ∞ is not an isolated point. In fact, we have no instances of PseudoEMetricSpace besides instances that come from PseudoMetricSpace or instances that already assume (Pseudo)EMetricSpace on some other type.

I'm not sure how to best "fix" this. Presumably there's a bunch of lemmas that require EMetricSpace and talk about the topology of the space? (If not, we can simply remove the uniformity from the data of an EMetricSpace.)
I would like ℝ≥0∞ to be an EMetricSpace (if it isn't, then what is?), but I think it cannot be equipped with a nice uniformity? If so, then we should just remove the uniformity from EMetricSpace. However, we want it to work well with the topology (I think), so maybe we should redefine PseudoEMetricSpace to include an axiom that the topology plays well with edist something like this

def EMetric.ball [EDist α] (x : α) (ε : ℝ≥0∞) : Set α :=
  { y | edist y x < ε }

class PseudoEMetricSpace (α : Type u) [TopologicalSpace α] extends EDist α : Type u where
  edist_self : ∀ x : α, edist x x = 0
  edist_comm : ∀ x y : α, edist x y = edist y x
  edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z
  isOpen_ball : ∀ (x : α) (r : ℝ≥0∞), IsOpen (EMetric.ball x r)

Maybe we want a stronger condition on the topology, e.g. that on all balls (also of infinite radius) the topology coincides with the topology given by edist, so that only the topology between the balls of infinite radius is left unspecified.

Earlier somewhat related discussion here

[Floris van Doorn]

(I brought this up in the discussion of #21422)

[Yury G. Kudryashov]

I wouldn't call it "broken". There are 2 examples that work with our definition: Closeds and Lp emetric on the space of all measurable functions.

[Yury G. Kudryashov]

Is there a consensus in the literature on what should be called an extended metric space?

[Yury G. Kudryashov]

Definitely, we can have a typeclass between EDist and the current EMetricSpace. BTW, ENNReals won't be EMetricSpace in terms of your definition, because ball ∞ 1 isn't open.

[Yury G. Kudryashov]

+1 example: max edistance on functions that aren't assumed to be bounded.

[Yury G. Kudryashov]

+1: evariation on paths that aren't assumed to have bounded variation.

[Yury G. Kudryashov]

We can define EDist ENNReal, then see what properties are still true, then decide if we want to have a typeclass for this.

[Floris van Doorn]

Maybe I am a bit too harsh with my words, but I'm wondering if we can weaken the type-class assumptions to make this class more widely useful.

[Floris van Doorn]

Yury G. Kudryashov said:

Definitely, we can have a typeclass between EDist and the current EMetricSpace. BTW, ENNReals won't be EMetricSpace in terms of your definition, because ball ∞ 1 isn't open.

You are completely correct that ball ∞ 1 isn't open, so my suggestion doesn't work for the goal I intended. Thanks for spotting that.
Maybe ℝ≥0∞ really is ill-behaved enough to not be something like this...

[Floris van Doorn]

Yury G. Kudryashov said:

We can define EDist ENNReal, then see what properties are still true, then decide if we want to have a typeclass for this.

Somewhat related, in the Carleson project I'm defining a docs#ENorm on ENNReal, and I'm trying to figure out what precise class I want this enorm to satisfy. Probably this: carleson#ENormedSpace.

[Floris van Doorn]

Yury G. Kudryashov said:

I wouldn't call it "broken". There are 2 examples that work with our definition: Closeds and Lp emetric on the space of all measurable functions.

Both of these require that the space you start with is already an EMetricSpace, and in both cases (I think?) if you start with a metric space you get a metric space out. So that still doesn't provide any EMetric spaces used in Mathlib that are not Metric spaces.

[Floris van Doorn]

In your extra examples, are the topologies given by the emetric-space actually useful though?

[Yury G. Kudryashov]

Closeds on the real line aren't a MetricSpace. E.g., the Hausdorff distance between {4 ^ n | n : Nat} and {2 * 4 ^ n | n : Nat} is infinity.

[Sébastien Gouëzel]

I don't think our definition is broken: it does exactly what it is designed for. The standard example is indeed L^p (even when the base space is a nice metric space): the edistance between two functions is the integral of |f - g|, which can be infinite. Two functions which are at infinite distance are really not comparable in any way, so you really want them to be in different connected components of the L^p space.

[Floris van Doorn]

Thanks for your input! It's clear that I was wrong (sorry for the provocative title), and that EMetricSpace works fine. Maybe I'll investigate at some later point if there is a class between EDist and EMetricSpace where ENNReal fits nicely.

The reason I started this discussion is by PR #21422, where we add classes ENormedAddCommMonoid, which is supposed to be satisfied by both NormedAddCommGroup and ENNReal. NormedAddCommGroup is defined in terms of MetricSpace, so I was wondering to what extend we could have ENormedAddCommMonoid extend EMetricSpace.

[Kevin Buzzard]

Isn't what Floris is actually saying, that no amount of metric or emetric stuff with d(x,infty)=infty will ever give the right topology on ENNReal, which presumably is the topology making it homeomorphic to the closed interval.

[Kevin Buzzard]

So somehow maybe the conclusion is that ENNReal should not actually be an emetric space, because this doesn't even give the right notion of convergence, e.g. 1+1+1+1+1+1+... does not converge to infinity in the emetric, even though this is clearly desirable