Opposite of diameter of an (e)metric space.

Stream: maths

[Wrenna Robson]

[Removed, incomplete.]

[Wrenna Robson]

Consider a metric space X, and a set S in X. The following is the definition of the diameter of the set S: $\operatorname{diameter} S = \operatorname{sup} \{d(x, y) \mid x, y \in S\}$. Note that we could also write this as $\operatorname{sup} \{d(x, y) \mid x, y \in S, x \ne y\}$, as long as we're taking the operation over the extended non-negative reals so that we can deal with the sup of the empty set acceptably.

Consider the quantity $\operatorname{inf} \{d(x, y) \mid x, y \in S, x \ne y\}$, which is in some sense "dual" or "opposite" to this. Referencing https://math.stackexchange.com/questions/2325394/what-to-call-the-opposite-of-the-diameter-of-a-metric-space, it doesn't appear there is a standard name for this quantity. But I would like to define it in mathlib (as I need the minimum distance of a set for coding theory stuff, and this is a natural step towards that). Can anyone suggest a good short name for this quantity?

The best one I've come up with so far is to call it the "grain" of the set - but I'm interested in better alternatives.

[Wrenna Robson]

(Sorry about the early posting - formatting now fixed.)

[Wrenna Robson]

I had a go at figuring out what this should be like. https://github.com/linesthatinterlace/verifying-cmce/blob/main/lean/src/shared/grain.lean

[Wrenna Robson]

It's a surprisingly robust definition! But one immediately wants to reach for equivalent notions to e.g. "bounded".

[Wrenna Robson]

Related to but not the same as some of these concepts: https://en.wikipedia.org/wiki/Delone_set

[Wrenna Robson]

It's possible that "packing radius of a set" is the right term (which is different from the packing radius of the set with respect to the whole space, off by about a factor of two).

[Kalle Kytölä]

Wrenna Robson said:

Can anyone suggest a good short name for this quantity?

How about inf_separation or more colloquially "minimum separation"?

I think I've heard the "minimum distance" in coding theory, as you mention. It is quite descriptive. Unfortunately docs#metric.inf_dist means a different thing, so I would avoid a naming clash --- therefore my proposal of "separation" rather than "distance".

[Kalle Kytölä]

Packing radius might be nice, too, though. (modulo the factor 2)

[Wrenna Robson]

inf_sep might be very nice! (I favour something short because it appears in theorem names: c.f. diam rather than diameter.)

[Wrenna Robson]

grain has the advantage of being five characters like diam <_<

[Eric Wieser]

I don't think that "advantage" is true

[Yaël Dillies]

The problem I have with inf_sep is that it could be read as inf + sep. So maybe infsep?

[Wrenna Robson]

Four is basically the same as five, Eric.

[Wrenna Robson]

I think you're right Yaël. But that might be an issue with any use of inf in the name.

[Yaël Dillies]

No, because the naming convention means that name atoms are separated by underscores.

[Eric Wieser]

I'm not sure that rule is universal

[Yaël Dillies]

Do you have a counterexample in mind?

[Yaël Dillies]

Note that here I'm considering bUnion as an atom, even though it is derived from Union. Here, b acts as a modifier, not as an atom itself.Similarly for forall vs forall₂.

[Eric Wieser]

exists_unique

[Wrenna Robson]

Am inclined btw to define fininfsep and infsep, the former being for finsets.

[Wrenna Robson]

Where they agree in the obvious case.

[Wrenna Robson]

This is because in the finset case, obviously, you have minimum rather than infimum, and various nice things therefore hold.

[Wrenna Robson]

and it's just nicer to work with really.

[Wrenna Robson]

I'm making some good progress on a file: might have a WIP PR to share soon for comment.

[Wrenna Robson]

if anyone can work out if diam_union has an analogous result for infsep and if so what that would be, that would be great.

[Sebastien Gouezel]

You can also use finset.inf_sep and set.inf_sep, so that dot notation becomes available and the names are coherent.

[Sebastien Gouezel]

There is no result for the inf_sep of a union: the sets {0, 1} and {epsilon, 1+epsilon} both have inf_sep equal to 1, but the inf_sep of their union is arbitrarily small. (Or you need to assume some bound on the minimal distance between elements of s and t).

[Wrenna Robson]

Hmm: we don't use dot notation for diam (perhaps we should). But that sounds useful.

[Wrenna Robson]

What about the inf_sep of an intersection?

[Sebastien Gouezel]

If s is included in t, then s.inf_sep \le t.inf_sep. So the inf_sep of an intersection is bounded by the min of the inf_seps.

[Wrenna Robson]

right, that's what I thought should be true

[Wrenna Robson]

Bounded... below?

[Wrenna Robson]

I'm not sure about s <= t -> s.inf_sep <= t.inf_sep. I think the order reverses.

[Sebastien Gouezel]

Yes, sorry!

[Wrenna Robson]

To complicate matters slightly further naming-wise, you really want both a dist and edist version. So we have set and finset, dist and edist. How should they be incorporated into a name?

[Wrenna Robson]

set.einfsep, set.infsep, finset.einfsep, finset.infsep is one option.

[Sebastien Gouezel]

I'd go with set.inf_esep and set.inf_sep, and similarly for finsets.

[Wrenna Robson]

Aha

[Wrenna Robson]

yes makes sense

[Yaël Dillies]

Eric Wieser said:

exists_unique

That's not a counterexample though. I'm saying that when there are two atoms, they are separated by an underscore. This name only has one atom.

[Yaël Dillies]

A counterexample would be something like set.emptysmul, but of course the real name is docs#set.empty_smul.

[Wrenna Robson]

Kinda the issue with the name infsep is that inf is really an atom that we are lumping together...

[Eric Wieser]

Yaël Dillies said:

No, because the naming convention means that name atoms are separated by underscores.

Oh sorry, I read this as "atoms cannot contain underscores"

[Eric Wieser]

Wrenna Robson said:

Kinda the issue with the name infsep is that inf is really an atom that we are lumping together...

Strictly for the not-necessarily-version the atom is Inf

[Yaël Dillies]

That's exactly my point, though. If you write inf_sep, then you can read it as inf + sep. But if you write infsep that's impossible by the naming convention. In contrast, there's no rule that an atom shouldn't contain another atom as a sublist/prefix/suffix/infix/whatever.

[Yaël Dillies]

(typically mul and smul)

[Wrenna Robson]

Well, I don't strongly care too much.

[Wrenna Robson]

It'll all come out in the wash.

[Wrenna Robson]

This now exists in draft form as #15689.

[Wrenna Robson]

I'm actively seeking comment on it - it's not finished - but it feels developed enough that I don't feel silly asking for comment on it. In particular I have a number of lemmas I need to fill in, and I want to make sure I get them all.

[Wrenna Robson]

There's some natural definitions about a space being uniformly discrete that could fit in with this. There's also the content of #12010. This is distinct from this but closely related to it, I think.

[Wrenna Robson]

In the ultimate case I'm most interested in (Hamming weights for (finite) linear codes), everything is as "nice" as possible, but I realised that what that meant was that I was mixing up/fusing separate concepts. (In such a space, things are finite, but also the metric is natural-valued, and necessarily bounded and uniformly discrete.)

[Wrenna Robson]

#15689 just updated today and is now much improved. I think it's approaching, if not a final form, at least a form where I am less inclined to make minor changes.

[Wrenna Robson]

There are some minor lemmas it depends on that should be their own PRs.

[Wrenna Robson]

I would like to actively request someone to give it a detailed review and give me their full thoughts - focusing less on style issues etc. (though that is fine) and more on whether it's conceptually "right" and what natural lemmas might be missing.