EMetric instance on ENNReal

Stream: Is there code for X?

[Oliver Nash]

Am I being silly or do we really not have:

import Mathlib.Data.Real.ENNReal

instance : EMetricSpace ℝ≥0∞ := inferInstance -- fails

[Kevin Buzzard]

Activating silly defences:

import Mathlib
set_option autoImplicit false

open ENNReal

instance : EMetricSpace ℝ≥0∞ := inferInstance

Yeah it looks like you're not being silly. I really like this "am I missing an import -- no because I imported everything" fallback.

[Yaël Dillies]

We don't have it because it doesn't give you the right topology on ℝ≥0∞.

[Oliver Nash]

Oh!

[Yaël Dillies]

With that instance, ∞ is infinitely far away from any other point, so it's an isolated point.

[Kevin Buzzard]

wait, what is the "right topology"? Somehow it's been decided that it's homeo to $[0,1]$ despite Yael having just convincingly argued that it's actually homeomorphic to $[0,1)$ disjoint union a point? :-)

[Oliver Nash]

I wonder if this might be a useful def to be able to enable locally. I reached for this because I want to construct a small argument about measures of sets being similar. Since measures are ℝ≥0∞-valued this edistance would be very convenient.

[Oliver Nash]

I'll continue what I was doing and see how useful or not this distance would actually be in my application. If it looks very useful, I'll think about this some more. Thanks!

[Yaël Dillies]

Kevin, it depends on whether you want diverging series of non-negative reals to converge to $∞$.

[Kevin Buzzard]

Aah so they don't for the emetric! But they do for the topology.

[Kevin Buzzard]

And I know from LTE that it's very convenient for diverging series to converge to infty because it meant that I could do a lot of e.g. sum rearrangement without ever having to prove that anything converged.

[Yury G. Kudryashov]

@Oliver Nash In what statement do you want a EMetric on ENNReals?

[Oliver Nash]

It's WIP so I don't have something as precise as I'd like but the general idea was that I had a small analysis-style argument I wanted to make about measures of sets being similar so it would contain expressions like edist (μ x) (μ y) ≤ ε if we actually had such an edist.

[Oliver Nash]

Of course all my sets actually have finite measure so it's really just a question of how early I take advantage of this and pass to the reals. But it looked like it might be convenient to be able to defer this. As I say, it's WIP so I'm not sure yet and haven't decided.

[Oliver Nash]

If the little project works out I'll post the PR here.

[Oliver Nash]

(It's mostly work I'm doing to avoid finishing preparation for Leiden. Don't tell Rob.)

[Yury G. Kudryashov]

You can introduce a global EDist instance for ENNReal (e.g., given by edist x y = max (y - x) (x - y)). Or even generalize docs#Nat.dist to any canonically ordered additive comm monoid.