Packings, coverings, nets, uniform discretesness et. al.

Stream: mathlib4

[Wrenna Robson]

I have been playing around with something I have meant to define for some time now (for nearly two years - been busy!): a set of definitions to try and capture the contents of https://en.wikipedia.org/wiki/Delone_set. The direct motivation for this is to have an effective language to reason about (linear or otherwise) codes in, especially with the Hamming distance. (The notion of a uniformly discrete distance, for instance, defined at the head of here, is exactly that property of the Hamming distance that lets us say that non-equal elements have hamming distance at least 1, etc., etc.)

I don't think all these definitions are perfect, and perhaps I have missed something and I have some of them already. So the reason I am raising this topic here is that I want feedback on what I've lain down so far, and open thoughts.

(By the way, note that as currently defined the Hamming distance is also bounded! I suppose we could have an infinite version but I seem to recall we wanted to do it this way so we could stay in relatively easy to work with finite land.)

import Mathlib.Topology.MetricSpace.Infsep

universe u
variable {α β : Type*}

open scoped ENNReal

class DiscreteDist (α : Type u) [Dist α] : Type u where
  exists_pos_lt_dist : ∃ r > 0, ∀ x y : α, x ≠ y → r < dist x y

class BoundedDist (α : Type u) [Dist α] : Type u where
  exists_finite_dist_lt : ∃ R : ℝ, ∀ x y : α, dist x y < R

class DiscreteEDist (α : Type u) [EDist α] : Type u where
  exists_pos_lt_edist : ∃ r > 0, ∀ x y : α, x ≠ y → r < edist x y

class BoundedEDist (α : Type u) [EDist α] : Type u where
  exists_finite_edist_lt : ∃ R : ℝ≥0∞, R < ∞ ∧ ∀ x y : α, edist x y < R

instance [PseudoMetricSpace α] [DiscreteDist α] : DiscreteEDist α where
  exists_pos_lt_edist := by
    rcases DiscreteDist.exists_pos_lt_dist (α := α) with ⟨r, r_pos, hr⟩
    use ENNReal.ofReal r
    simp_rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg r_pos.le, ENNReal.ofReal_pos]
    exact ⟨r_pos, hr⟩

instance [PseudoMetricSpace α] [BoundedDist α] : BoundedEDist α where
  exists_finite_edist_lt := by
    rcases BoundedDist.exists_finite_dist_lt (α := α) with ⟨R, hr⟩
    use ENNReal.ofReal R
    simp_rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff', ENNReal.ofReal_lt_top, true_and, forall_and]
    exact ⟨hr, fun x y => (dist_nonneg).trans_lt (hr x y)⟩

namespace Set
variable [PseudoEMetricSpace α]

noncomputable def packingRadius (s : Set α) : ℝ≥0∞ :=
sSup fun r => s.PairwiseDisjoint (EMetric.ball · r)

lemma packingRadius_eq_half_einfsep (s : Set α) : s.packingRadius = s.einfsep / 2 := sorry

noncomputable def coveringRadius (s : Set α) : ℝ≥0∞ :=
    sInf fun r => (EMetric.closedBall . r) '' s = univ

-- lemma coveringRadius_eq_something (infEDist? something not defined which should be?)

def isPacking (s : Set α) (e : ℝ≥0∞) := e ≤ 2*(s.packingRadius)

def isCovering (s : Set α) (e : ℝ≥0∞) := s.coveringRadius ≤ e

def isNet (s : Set α) (e : ℝ≥0∞) := s.isPacking e ∧ s.isCovering e

def uniformlyDiscrete (s : Set α) := 0 < s.packingRadius

def relativelyDense (s : Set α) := s.coveringRadius < ∞

def delone (s : Set α) := s.uniformlyDiscrete ∧ s.relativelyDense

lemma uniformlyDiscrete_of_isPacking_pos (s : Set α) (e : ℝ≥0∞) (e_pos : 0 < e)
    (h : s.isPacking e) : s.uniformlyDiscrete := (ENNReal.mul_pos_iff.mp (h.trans_lt' e_pos)).2

lemma relativelyDense_of_isCovering_finite (s : Set α) (e : ℝ≥0∞) (e_finite : e < ∞)
    (h : s.isCovering e) : s.relativelyDense := h.trans_lt e_finite

lemma delone_of_isNet_pos_finite (s : Set α) (e : ℝ≥0∞) (e_pos : 0 < e) (e_finite : e < ∞)
    (h : s.isNet e) : s.delone :=
  ⟨s.uniformlyDiscrete_of_isPacking_pos _ e_pos h.1,
  s.relativelyDense_of_isCovering_finite _ e_finite h.2⟩

end Set

[Newell Jensen]

The definitions you have from packingRadius on wards seem to line up with what is mentioned in Delone set nicely. I am still trying to wrap my mind around how you would connect this with the class definitions you have above? I would imagine that if you have had instances of DiscreteDist and BoundedDist on \alpha that you would then hope to be able to derive s.delone (or something of that sort)?

[Wrenna Robson]

Yes, I think that then follows.

[Newell Jensen]

I would like to see this in mathlib so if you need any help, let me know.

[Wrenna Robson]

Thanks. I don't have any time right now but - oh, I can't remember his name, but if you search "Delone" I've been talking about this recently with another community member.

[Wrenna Robson]

(I'm moving house in two weeks.)

[Newell Jensen]

Yes, I read that chat. Do you have a branch you have already started working on?

[Wrenna Robson]

Me personally? No I don't think I pushed it.

[Wrenna Robson]

I'm really interested in this being in MathLib too, especially as I made the original infsep definition that I think is flawed but a decent start. It's purely been a finding time thing.

[Wrenna Robson]

Very interested in collaborating on this though.

[Newell Jensen]

Okay, I can put up a draft branch if you would like to collaborate on this if that is okay with you.

[Wrenna Robson]

Sounds great.

[Wrenna Robson]

Incidentally it's possible that we shouldn't define packingRadius as above (if you read that discussion, you'll have seen the issues that creep in in the discrete case) but it feels like one those things we're just going to need to get right by experimentation

[Wrenna Robson]

(I think I may have had a local branch where I was playing around with some other definitions but I can't access it right now, so press ahead and we'll throw some stuff together and see where we get to.)

[Newell Jensen]

At first I was thinking of naming the file Delone and putting in the same directory as your infsep but I can easily see this file can expand on to Meyer sets etc. That is, things like ε-nets, ε-packings, ε-coverings, uniformly discrete sets, relatively dense sets, Delone sets, Meyer sets etc. Maybe call the file epsilon.lean?

[Newell Jensen]

Wrenna Robson said:

Incidentally it's possible that we shouldn't define packingRadius as above (if you read that discussion, you'll have seen the issues that creep in in the discrete case) but it feels like one those things we're just going to need to get right by experimentation

I have seen another definition of packing radius

$$r_p = \sup\{ r > 0\ |\ \Lambda \in \bigcup_{R > 0} D_{(r, R)}\}$$

where $D_{(r, R)}$ is the set of all Delone sets with two choosen radii $r$ and $R$ so that $$U = $B_{r(0)}$$ and $K = B_{R(0)}$ are appropriate "confining" neighborhoods (of uniform discreteness and relative denseness) for $$\Lambda$$.

But this requires defining and using the Minkowski sum and difference to define uniform discreteness and relative denseness beforehand.

[Wrenna Robson]

What's the Minkowski sum and difference?

[Wrenna Robson]

This does look like it's maybe workable. In a sense the key thing is that you can link it back to things like the concept of "minimum distance" when that is possible.

[Wrenna Robson]

Hmm, looking up the Minkowski sum and difference, that does seem as if it needs an underlying addition operation...

[Newell Jensen]

Wrenna Robson said:

Hmm, looking up the Minkowski sum and difference, that does seem as if it needs an underlying addition operation...

Yes, the definitions I have seen assume an Euclidean space.

[Wrenna Robson]

Right, whereas we're thinking - well, the prototypical example in coding theory is the hamming distance but other metrics exist

[Wrenna Robson]

And it feels as if there should be a unifying description

[Newell Jensen]

However, there are pointwise operations on sets.

[Newell Jensen]

So I am not sure that this is an issue.

[Wrenna Robson]

Right

[Wrenna Robson]

I mean as I say for a space with the hamming distance there's not necessarily any kind of operation at all.

[Newell Jensen]

From what I have seen in the literature, the packing and covering radius in coding theory are derived from a lattice subset of an Euclidean space. Hamming distance is also defined as the difference between two strings, which are modeled as vectors in a vector space and so on. I am not an expert in this area but I have a feeling that although the majority of mathlib builds from the general to the concrete, maybe this time the hamming distance will need to be modeled from the concrete as to get to the general. (I am just going off Wikipedia and Lattice and Codes - Ebeling).

That is, we define things using more concrete definitions of Metric/Euclidean space and work backwards for the coding theory bits that are needed. This would be following the route of the literature at least from what I can tell.

[Newell Jensen]

Will re-read over that chat you had to see what the main issues you were having with the packing radius were.

[Yaël Dillies]

@Newell Jensen, are you thinking of docs#Metric.thickening ?

[Wrenna Robson]

@Newell Jensen well, by definition it isn't a Euclidean space, because then it would have the Euclidean distance. And technically a Hamming space just needs, well, equality of elements. Linear codes are a vector space but they could, for instance, be over a finite field, where there's no notion of being embedded inside a Euclidean space at all.

[Newell Jensen]

The Euclidean or metric space assumption was for the packing and covering radii, since those are needed for Delone sets. I was assuming that for the Hamming distance/space etc. that would be handled in another branch. What I was trying to get at was the concern over using balls for the packing radius definition. I have still yet to read up on that discussion to understand the issue and was getting ahead of myself some.

[Wrenna Robson]

Well the Hamming space is also a metric space, that's fine.

[Wrenna Robson]

(we already have that)

[Wrenna Robson]

The concern basically boils down to - when your metric is integer valued, or I guess really discrete such that you don't have "continuous" values but it's especially clear in the integer case, one can end up with - well, for instance, open balls of radius 1 around distinct points won't intersect, so you always have the packing radius at least 1, but that's true even if the minimum distance is 1... basically the difference between open and closed balls matters more.

[Newell Jensen]

Yaël Dillies said:

Newell Jensen, are you thinking of docs#Metric.thickening ?

No (although this is first time I am seeing this).

[Newell Jensen]

@Wrenna Robson just to get something on the board: #10641

[Wrenna Robson]

I like the name

[Wrenna Robson]

I think it would not be unreasonable to remove InfSep.lean and put its contents here

[Wrenna Robson]

It certainly seems intimately bound up in this

[Wrenna Robson]

I'm not sure it's in my definitions above but I did define the equivalent definition to infsep but for covering radius... somewhere...

[Wrenna Robson]

I'm trying to remember if I posted it. Sorry, I'm just a bit out of it with stress as I say.

[Newell Jensen]

Wrenna Robson said:

I'm trying to remember if I posted it. Sorry, I'm just a bit out of it with stress as I say.

No worries, I will remove infsep and add it to the file.

[Wrenna Robson]

Thanks.

[Newell Jensen]

I wonder if we can remove all the #aligns?

[Wrenna Robson]

Morally I feel like it should be fine but I don't know what the policy on them is

[Ruben Van de Velde]

Why do you want to remove aligns?

[Wrenna Robson]

It might be good to state some goals: I think broadly what we are looking for here is, aside from the specific context of coding theory, to get concepts such as Delone sets, packing radii, minimum distance and so forth to a) lie flat together, b) be defined in Mathlib to an appropriate degree of generality i.e. for as arbitrary a metric space as possible.

[Wrenna Robson]

The wrinkles come in because in the literature, different definitions are sometimes used, and in general settings they might not be equivalent.

[Newell Jensen]

Ruben Van de Velde said:

Why do you want to remove aligns?

It was only a thought since I am moving a previous file into a new one.

[Wrenna Robson]

@Edward van de Meent feel free to use your thread for discussing coding theory in specific, but the general discussion should I think go here

[Patrick Massot]

Please do not remove any #align from Mathlib until we officially deprecate mathport.

[Wrenna Robson]

Patrick Massot said:

Please do not remove any #align from Mathlib until we officially deprecate mathport.

Thanks, good to understand the policy.

[Patrick Massot]

I now it seems crazy that people could start porting a Lean 3 project now. But it could happen and the vague goal was to make it possible to do so for one year after the port.

[Wrenna Robson]

For sure

[Edward van de Meent]

@Newell Jensen i took a look at the current definitions in #10641 ... i noticed that your definitions uses the sSup and sInf from ENNReal... i don't think this is quite what we want... in particular i think we'd like this to depend on the codomain we're looking at... i got around this problem by defining my own kind of general metric spaces... is this something that you think might be a viable option?
for example, i defined stuff like this:

@[ext]
class GDist (α : Type*) (β :Type*) [LinearOrderedAddCommMonoid β] where
  protected gdist : α → α → β

def gdist (β :Type*) [LinearOrderedAddCommMonoid β]{α :Type*} [GDist α β] (x y: α) : β := GDist.gdist x y

class GPseudoMetricSpace (α : Type u) (β:Type v) [LinearOrderedAddCommMonoid β] extends GDist α β where
  gdist_self : ∀ x : α, gdist x x = 0
  gdist_comm : ∀ x y : α, gdist x y = gdist y x
  gdist_triangle : ∀ x y z : α, gdist x z ≤ gdist x y + gdist y z
  toBornology : Bornology α := Bornology.ofGDist gdist gdist_comm gdist_triangle
  cobounded_sets : (Bornology.cobounded α).sets =
    { s | ∃ C : β, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, gdist x y ≤ C } := by intros; rfl

for most of the DeloneSet stuff i used a mixin to be able to combine CompleteLinearOrder and LinearOrderedAddCommMonoid:

class IsOrderedAddCommMonoid (α : Type*) [PartialOrder α] [AddCommMonoid α] where
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c, c + a ≤ c + b
instance (α : Type*) [h1: LinearOrder α] [h2: AddCommMonoid α] [h3:IsOrderedAddCommMonoid α]:
  LinearOrderedAddCommMonoid α := {
  h1,h2,h3 with
}

this way you avoid diamonds while assuming both of them

[Edward van de Meent]

(not mwe but it should give a sense of how i went about some of these things)

[Wrenna Robson]

I think defining a general metric is an idea with metric but it's possibly beyond scope of this, I'm not sure.

[Edward van de Meent]

it does fix how you might expect the covering radius and packing radius to work...

[Edward van de Meent]

i.e. have them be discrete when the distance is

[Wrenna Robson]

Yeah, I'm just wondering if there's another way

[Edward van de Meent]

i suppose there might be some construction where you always cast between ENNRealand the 'actual' codomain of your metric but i think that might get tedious

[Wrenna Robson]

Well we already have that to a degree when you need to work with real metrics...

[Edward van de Meent]

the fact that it's currently like that doesn't mean there can't be a better solution...

[Wrenna Robson]

Ultimately as you say you want it to be true that if the range of your metric is discrete - to put it another way, if the distance between objects decreases in "chunks" - then this is also true of the covering and packing radii in the way that we would expect.

[Wrenna Robson]

And it feels like this is a property of the metric, to be sure, but not one that necessarily needs the codomain to be different.

[Wrenna Robson]

In the particular case where the range is nonnegative Integers, it's easy to work with, but what if it were nonnegative half integers, or some other type on which a bunch of stuff isn't already defined?

[Wrenna Robson]

Better I think to work with sets than types

[Edward van de Meent]

what if the metric can't be embedded in ENNReal though? then you also get problems...

[Wrenna Robson]

For sure. I can't think of any examples where that might happen

[Edward van de Meent]

you might define a metric to nonneg hyperreals or to nonneg surreals? i don't think you can embed those...

[Wrenna Robson]

I suppose. But I'm not even sure we currently have those in Mathlib in any form - this might be the limit of what we should generalise

[Edward van de Meent]

i believe that hyperreals are a thing?

[Edward van de Meent]

yup.

[Edward van de Meent]

it's at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Hyperreal.html#Hyperreal

[Wrenna Robson]

Yeah I guess in the most most general case, you would embed a metric in the surreals

[Wrenna Robson]

But essentially I think I think we should stick to the extended nnreals for now.

[Edward van de Meent]

but i already have the definitions, and porting the necessary lemmas from PseudoMetricSpace and MetricSpace is very easy, just a case of adding G's, beta's, and sometimes adding some assumption about cancelling . this should work for most things you might need. it would be a shame if i were not to use them :smiling_face_with_tear:

[Wrenna Robson]

We have the surreals but their basic theory is not complete.

[Edward van de Meent]

yes, so just generalise the codomain and it's fixed?

[Wrenna Robson]

No for sure. I'm very much in favour of generalized metrics in general. There was someone else talking about them fairly recently...

[Edward van de Meent]

(that might have been me?)

[Wrenna Robson]

Maybe?

[Wrenna Robson]

My memory is poor, especially without avatars.

[Wrenna Robson]

I didn't think so though. Anyway! It seems a shame to throw away your work on that. But they could be added without this Delone/radius stuff, couldn't they?

[Edward van de Meent]

they could... but the fact that we want these definitions to work is a great reason to include them

[Wrenna Robson]

I agree. But what I'm suggesting is another PR to base #10641 on.

[Edward van de Meent]

i'm not sure i quite understand what that entices precisely, could you please elaborate?

[Wrenna Robson]

As in, prepare a branch with generalised metrics on, push and submit it for review, and then #10641 could build on it while it was still in review.

[Wrenna Robson]

If you haven't done a PR before, perhaps ambitious for a first PR. Still, everyone needs to start somewhere.

[Kevin Buzzard]

Patrick Massot said:

I now it seems crazy that people could start porting a Lean 3 project now. But it could happen and the vague goal was to make it possible to do so for one year after the port.

I totally agree with this, and had no plans on porting anything, but then Eric pointed out to me a couple of days ago that I'd never ported the solutions to my 1st year undergrad course to Lean 4 and the thought did occur to me that I might want to just try mathport one last time...

[Edward van de Meent]

Wrenna Robson said:

As in, prepare a branch with generalised metrics on, push and submit it for review, and then #10641 could build on it while it was still in review.

a first PR is at #10680 , defining pseudo metric spaces with generic codomain.

[Edward van de Meent]

i now have #10749 , defining metric spaces with a generic codomain.

[Wrenna Robson]

Oh cool, does it build off #10680?

[Edward van de Meent]

yes, it does. (it is also listed as a dependency)

[Wrenna Robson]

Great. Well done!

[Edward van de Meent]

i haven't ported lemmas yet, but i think most lemmas we would need are easily ported.

[Edward van de Meent]

how do we add these definitions to #10641?

[Wrenna Robson]

Merge in these branches and add them as dependencies would be the normal way.

[Edward van de Meent]

i merged the branch into it, can you check i did it correctly?

[Wrenna Robson]

I'm afraid I'm off sick today.

[Wrenna Robson]

So not easily. Sorry.

[Edward van de Meent]

oh... get better soon then :heart:

[Newell Jensen]

I assume you have looked at how other "blocked-by-other-PR" branches in mathlib are handling it. If so, you should be good. I am not sure if there is any documentation that mentions exactly what to do here.

[Edward van de Meent]

well... i didn't quite look at that...
looking at it afterward, i'm not really finding an example where it gets added afterward? so i'm not sure... it might be the case that you, as creator of the PR, need to add the dependencies to the first comment... i'm not sure tho

[Newell Jensen]

From your merge I see your changes have been added to the branch. I assume that once your branches get merged this diff would change back to the changes of my branch (if I didn't add any further changes that is).

[Edward van de Meent]

yes, i'm pretty sure that's how that works, yes

[Newell Jensen]

Whether or not this tracks the changes you push to your other branches though, I am unsure.

[Edward van de Meent]

i think it doesn't

[Edward van de Meent]

anyhow, i hope you don't mind if i change some of your work to include these generalised definitions...

[Newell Jensen]

I don't mind. This is all for fun anyways right? :wink:

[Edward van de Meent]

do we need #align statements if this wasn't in lean3?

[Newell Jensen]

I think it would be wise though to get your previous branches dialed in first, or you could be wasting time so to speak

[Newell Jensen]

Edward van de Meent said:

do we need #align statements if this wasn't in lean3?

Yes, we need to keep those as Patrick mentions above.

[Wrenna Robson]

It doesn't track changes you make to other branches

[Wrenna Robson]

I would probably counsel spending time on them and getting feedback as it will have cascading effects

[Newell Jensen]

Yes, the PR review process for mathlib can also take longer than one would expect sometimes (depending).

[Wrenna Robson]

My goodness yes

[Newell Jensen]

I think getting somebody to review who has done a bunch on Metric spaces work (not I) would be best.

[Edward van de Meent]

that's true... although if there are many dependencies, i believe it can give quite a bit of motivation for getting it approved...

[Newell Jensen]

Well, usually small changes get merged faster, all things being considered.

[Newell Jensen]

At any rate, maybe @Yury G. Kudryashov or someone else with more experience than I can take a look at your branches if they get some time.

[Edward van de Meent]

is there any sense in splitting up a PR post hoc?

[Edward van de Meent]

because i could probably split the first pr into maybe 3 parts? one defining the mixins for combining orders and (additive) commutative monoids, one for defining GDist and GPseudoMetricSpace, and one for copying some relevant lemmas from PseudoMetricSpace

[Newell Jensen]

Well sometimes the reviewers need to see the other parts to see where you are "going with it all" so I would just leave it until you get some feedback. My $0.02 at least.

[Edward van de Meent]

right... anyhow, i've done some thinking and i've been considering if we want Delone to be a definition or rather a Prop-typed Mixin class or something like that... or maybe even data-carrying?
for example, these are some possiblilities

def isDelone {a} (s:Set a) : Prop := uniformlyDiscrete s ∧ relativelyDense s

structure Delone a :Type _ where
  carrier : Set a
  uniformly_discrete: uniformlyDiscrete carrier
  relatively_dense: relativelyDense carrier

class isDelone {a} (s:Set a): Prop where
  uniformly_discrete: uniformlyDiscrete carrier
  relatively_dense: relativelyDense carrier

[Edward van de Meent]

i think in general the class is preferable to the def, as that can be inferred automatically when you define instances...

[Edward van de Meent]

but i'm not sure how i should decide between the structure and class...

[Ruben Van de Velde]

Re: #align: you shouldn't add new ones when there's nothing in mathlib3 that can be aligned, but you should preserve the existing ones while there's still something sensible to align to

[Newell Jensen]

Edward van de Meent said:

right... anyhow, i've done some thinking and i've been considering if we want Delone to be a definition or rather a Prop-typed Mixin class or something like that... or maybe even data-carrying?
for example, these are some possiblilities

def isDelone {a} (s:Set a) : Prop := uniformlyDiscrete s ∧ relativelyDense s

This is what is already in the branch, its just the Prop type is not explicitly written.

[Edward van de Meent]

right... so what do you think about my other suggestions?

[Sébastien Gouëzel]

I would probably go with

structure IsDeloneWith (s : Set X) (r R : ℝ) : Prop :=
  UnifDiscrete : UniformlyDiscreteWith s r
  UnifDense : UniformlyDenseWith s R
  rPos : 0 < r
  RPos : 0 < R

def IsDelone (s : Set X) : Prop :=
  ∃ r R, IsDeloneWith s r R

because the values of r and R can be relevant, so most API should be developed with IsDeloneWith (just like we do for LipschitzWith or IsBigOWith). And definitely a structure, not a class, because it's not something you can expect the system to fill in for you in useful ways.

[Edward van de Meent]

ah... i hadn't considered that...

[Sébastien Gouëzel]

By the way, I am still not really convinced that the general GDist class you have just PRed is the way to go, because it would lead to a lot of code duplication, and create a bunch of unsolvable diamonds if you want to register useful instances for products for instance. Do you have examples of issues that can't be solved with the mixin or extension approaches that have been sketched to you earlier in the discussion?

[Edward van de Meent]

you can't make a metric with a codomain that cannot be injectively embedded into ENNReal, for example hyperreals or surreals.

[Wrenna Robson]

While this is true, it is still unclear to me there's any practical application for this.

[Edward van de Meent]

i also think that making extensions will bring the same diamond issues that you would get anyway...

[Sébastien Gouëzel]

Yes, I'm not asking for theoretical issues, rather practical ones that you have encountered when trying to prove a concrete theorem and that have led you to introduce the more general class.

[Sébastien Gouëzel]

Prop-valued mixins will not lead you to diamonds. Extensions wouldn't lead you to diamonds either if one extends metric spaces in the correct way.

[Edward van de Meent]

the problem i'm trying to solve is the fact that you cannot take the infimum or supremum of distances with certain properties when using hamming distance, without having to specify and prove each time that you keep within the (extended) natural numbers.

[Edward van de Meent]

with regards to the code duplication, i'm not sure i quite see what you mean

[Edward van de Meent]

any duplication will be temporary as soon as we make sure MetricSpace a gets a GMetricSpace a Real instance

[Edward van de Meent]

and yes, that might bring with it some diamonds, but nothing we can't fix by implementing forgetful inheritance

[Sébastien Gouëzel]

You can for instance use edist, and have a lemma saying that the supremum of a subset of ENNReal made of extended natural numbers is still an extended natural number.

As for code duplication, you were saying yourself that you had started to copy a bunch of metric space lemmas to GMetricSpace. Note that we can not hope to replace metric spaces and emetric spaces by GMetricSpace, because of the subtle inheritance pattern that a metric space should also contain an edist to avoid diamonds.

[Edward van de Meent]

those diamonds don't give problems though? because EDist a gets an instance GDist a ENNReal, while Dist a gets an instance GDist a Real. these don't have the same type signature, so there is no problem

[Yury G. Kudryashov]

But we can't just replace EMetricSpace and MetricSpace with a single GMetricSpace.

[Sébastien Gouëzel]

I am trying to say that the implementation of MetricSpace and EMetricSpacehave to be genuinely different. So you can't do both with one single class.

[Edward van de Meent]

that's true... but we can make instances to convert them

[Wrenna Robson]

It might be useful indeed to have special handling for an integer-valued metric, as I've expressed before, but I don't know exactly the best way of doing so.

[Yury G. Kudryashov]

This will lead to code duplication between 3 classes.

[Wrenna Robson]

Yeah I mean I don't know that it needs a class

[Edward van de Meent]

how so? what code will be duplicated?

[Wrenna Robson]

For that reason

[Yury G. Kudryashov]

About diamonds: you can't have a generic instance for GMetricSpace (∀ i, X i) K without introducing a diamond.

[Edward van de Meent]

you mean the one for getting to GDist, right?

[Yury G. Kudryashov]

Yes

[Yury G. Kudryashov]

Because formulas for Dist and EDist on ∀ i, X i are different.

[Johan Commelin]

How about

• No instances for products of GMetricSpaces (Because diamonds, and it's not clear we need such products)
• Instances from (E)MetricSpace to GMetricSpace _ (E)Real
• All lemmas that are copied to GMetricSpace can be deprecated for (E)MetricSpace.

[Wrenna Robson]

Yury G. Kudryashov said:

Because formulas for Dist and EDist on ∀ i, X i are different.

Oh, are they?

[Yury G. Kudryashov]

And the only way I see to unify them is to use ⨆ i, dist (x i) (y i) which is not what you probably want for Nat-value distance (you want it to be computable, right?)

[Yury G. Kudryashov]

Wrenna Robson said:

Yury G. Kudryashov said:

Because formulas for Dist and EDist on ∀ i, X i are different.

Oh, are they?

Yes, the Real one takes Finset.sup of nndists.

[Edward van de Meent]

Yury G. Kudryashov said:

Because formulas for Dist and EDist on ∀ i, X i are different.

i don't think this can lead to two of the same GDist class though? unless that was a diamond to begin with? because Dist (∀ i, X i) leads to GDist (∀ i, X i) Real, while EDist (∀ i, X i) leads to GDist (∀ i, X i) ENNReal

[Edward van de Meent]

and if Dist (∀ i, X i) leads to EDist (∀ i, X i), that's a diamond to begin with, and i wouldn't be introducing one

[Yury G. Kudryashov]

I claim that you can't have

instance [∀ i, GDist (X i) K] : GDist (∀ i, X i) K where
  gdist x y := _

without introducing a diamond.

[Yury G. Kudryashov]

Dist X doesn't lead to EDist X; PseudoMetricSpace X has a edist field to avoid a diamond.

[Edward van de Meent]

Yury G. Kudryashov said:

I claim that you can't have

instance [∀ i, GDist (X i) K] : GDist (∀ i, X i) K where
  gdist x y := _

without introducing a diamond.

ok... but how would you define this? because there are many ways to combine elements of K? if you know i is finite, you can add them... if you know K has a complete ordering, then both iSup and iInf give valid ways to combine them. so it doesn't make sense to begin with.

[Edward van de Meent]

if you mean that i might run into trouble when trying to define the hamming distance, i believe that's the whole reason why Hamming exists as a definition hiding previously defined metrics

[Wrenna Robson]

Yes, Hamming exists so that you don't have to worry about any kind of "default" product metric.

[Yury G. Kudryashov]

If you aren't going to have this instance, then I see no diamonds.

[Wrenna Robson]

(as an aside, it's easy to imagine an extension to hamming which defines an edist, which would then be defined on arbitrary products - I think we didn't do that because I was somewhat trying to preserve computability)

[Yury G. Kudryashov]

You can have a noncomputable ENat-valued function and a computable Nat-valued function that requires Fintype.

[Wrenna Robson]

Yes I think that's what you'd probably want to do and it would be better to do that!

[Wrenna Robson]

But it's another one of those "when I have time" things

[Yury G. Kudryashov]

BTW, another way to deal with this is to use a bundled operator instead of a typeclass.

[Wrenna Robson]

Hmm?

[Edward van de Meent]

in the sense of class PseudoMetric (dist: A -> A -> B)?

[Yury G. Kudryashov]

Something like

structure GDistHom (X R : Type*) [TypeclassAssumptions R] where
  toFun : X → X → R
  nonneg' : ∀ x, 0 ≤ toFun x
  symmetric' : ∀ x y, toFun x y = toFun y x
  triangle' : ∀ x y z, toFun x z ≤ toFun x y + toFun y z

[Wrenna Robson]

Oh for the GDist thing

[Yury G. Kudryashov]

Like we have docs#AddGroupSeminorm

[Edward van de Meent]

i think that in general would be a prettier solution, honestly... because there are lots of kind of distance you might define on a space, also real-valued ones.

[Edward van de Meent]

and making it a class will only invite diamond conflicts

[Edward van de Meent]

Yury G. Kudryashov said:

Something like

structure GDistHom (X R : Type*) [TypeclassAssumptions R] where
  toFun : X → X → R
  nonneg' : ∀ x, 0 ≤ toFun x
  symmetric' : ∀ x y, toFun x y = toFun y x
  triangle' : ∀ x y z, toFun x z ≤ toFun x y + toFun y z

i'll give it a try

[Edward van de Meent]

is there a reason this should have hom in the name though?

[Yury G. Kudryashov]

No reason, it can be called something like GMetric instead, or even Metric.

[Edward van de Meent]

and to be clear, should there be two versions, like Metric and PseudoMetric?

[Yury G. Kudryashov]

I guess, yes.

[Edward van de Meent]

is it necessary to make an operator class (like morphism classes) for GPseudoMetric and GMetric? i'm reading Anne Baanen's dissertation where they say one of the reasons to use such classes for MonoidHom was that the bundled nature would lead to duplicating lemmas for RingHom, i'm guessing this is possibly also the case for GPseudoMetric and GMetric?

[Kevin Buzzard]

What is a morphism of metric spaces? Is it distance-preserving? Distance-non-increasing? A continuous map of the underlying topological spaces?

[Edward van de Meent]

i don't think that works in this case, there isn't necessarily an underlying topological space i think...

[Edward van de Meent]

should there be some definition, it should at the very least include all isometries

[Edward van de Meent]

Kevin Buzzard said:

What is a morphism of metric spaces? Is it distance-preserving? Distance-non-increasing? A continuous map of the underlying topological spaces?

what i meant by "operator class" is a class GMetricClass T a b stating that T is a type where elements are a GMetric from a to b, i.e. a class for the distance operator

[Wrenna Robson]

Kevin Buzzard said:

What is a morphism of metric spaces? Is it distance-preserving? Distance-non-increasing? A continuous map of the underlying topological spaces?

In this context I think we'd want to use isometries but you make an important point.

[Yury G. Kudryashov]

If you don't want to duplicate between PseudoMetric and Metric, then you need a typeclass, at least for PseudoMetric.

[Edward van de Meent]

i thought so. as for the morphisms, i think in general a morphism of generic metrics GMetric a1 b1 and GMetric a2 b2 is some map f : a1 -> a2 and g:b1 -> b2 where g preserves ordering, and dist (f x) (f y))= g( dist x y)

[Edward van de Meent]

akin to how linear morphisms can take a ringhom as parameter

[Yury G. Kudryashov]

Let's not add morphisms between different metrics to the mix (yet).

[Yury G. Kudryashov]

As Kevin said, there are many natural types of morphisms here (isometries, dilations, continuous maps, Lipschitz continuous maps, Hölder continuous maps etc)

[Edward van de Meent]

right. in that case we probably take b1=b2 and g=id?

[Edward van de Meent]

which gives isometries i think...

[Joseph Myers]

We should definitely define IsometryClass and IsometryEquivClass, for the existing (pseudo)(e)metric spaces, as has been discussed before, since we have multiple types of bundled isometries and consequent duplication of lemmas. That doesn't say how useful such classes would be for metrics with other codomain, however.

[Edward van de Meent]

i've made the suggested changes, can someone take a look at #10680 and #10749?

[Newell Jensen]

Looks like you need to update the main github comment for the first PR as you are doing the mapping now correct?

[Newell Jensen]

This comment will be what ends up in the log when the branch is merged.

[Edward van de Meent]

i think i did do that already? could you point to a specific part that you think should be changed?

[Newell Jensen]

Ah, sorry, browser had stale tab from yesterday. I see changes on refresh.

[Edward van de Meent]

i'd like to create an instance GPseudoMetricClass (PseudoEMetric a) a b, but i can't figure out how to declare FunLike (PseudoEMetric a) a (a -> ENNReal)... i got this far:

import Mathlib.Topology.EMetricSpace.Basic
import Mathlib.Data.ENNReal.Basic
open ENNReal
instance: FunLike (PseudoEMetricSpace α) α (α → ℝ≥0∞) where
  coe := fun x => x.edist
  coe_injective' := fun X Y => by
    cases X; cases Y; congr
    simp only
    intro h
    sorry

i'd probably like to use some kind of extensibility, but apparently there are no applicable lemmas...

PseudoEMetricSpace.mk edist_self✝¹ edist_comm✝¹ edist_triangle✝¹ toUniformSpace✝¹ =
  PseudoEMetricSpace.mk edist_self✝ edist_comm✝ edist_triangle✝ toUniformSpace✝

should i make ext lemmas until this works? or is there no proof for this?

[Edward van de Meent]

curiously, there does exist an ext lemma for MetricSpace... not too sure what that's about

[Emilie (Shad Amethyst)]

Isn't PseudoEMetricSpace.mk.injEq enough?

[Emilie (Shad Amethyst)]

ext lemmas base themselves on that auto-generated theorem

[Edward van de Meent]

regardless, i've made a PR to add them at #10813

[Edward van de Meent]

i'm currently porting lemmas about einfsep... currently those lemmas assume EDist a, but i want them available for any GPseudoMetric a b with CompleteLinearOrder b, AddCommMonoid b, and CovariantClass b b (.+.) (.<=.)... but i realise that for most of these, that isn't the most general case...

should i prove these for general functions gdist:a -> a -> b, with an assumption along the lines of gdist >= 0 where necessary? could someone tell me if in that case, these lemmas will be available for all instances gdist:T with instances FunLike T a (a -> b)?

[Edward van de Meent]

i have defined an instance FunLike (GPseudoMetric a b) a (a -> b), so that is not the limiting factor here...

[Edward van de Meent]

or do i rather add gidst:T and FunLike T a (a -> b) assumptions?

[Edward van de Meent]

Edward van de Meent said:

or do i rather add gidst:T and FunLike T a (a -> b) assumptions?

this is what i've done for now...

[Edward van de Meent]

i'm guessing i can't port le_einfsep_pi_of_le, (or at least not directly) because i'd need to specify how i want to combine the metrics to get one on (b : β) → π b?

[Edward van de Meent]

ok, so i got this error...

failed to synthesize instance
  FunLike (((b' : β) → π b') → ((b' : β) → π b') → γ) ((i : β) → π i) (((i : β) → π i) → γ)

this happens at a point where i assume a parameter has an instance FunLike, which i pass some partially applied definition... i guess this means you typically shouldn't assume some funlike instance

[Edward van de Meent]

is it just me, or is it in general beneficial to only use einfsep over infsep?

[Wrenna Robson]

einfsep is more natural in some ways. infsep is useful because it's kind of like. it's useful to have the "real only" version defined. But it essentially has values it isn't meaningful on yeah

[Edward van de Meent]

i seem to be at a bit of a fork in the road... there are multiple possible definitions of covering_radius that i can think of. i've already proven some weak inequalities between them, so these are in ascending order:

• ⨆ (y:α), closest_distance s y with def closest_distance (y:α): ℝ≥0∞ := ⨅ (x ∈ s), (edist x y) the infimum of distances to elements of s. my intuition suggests this might be equivalent to the third definition... but i'm having a hard time proving it...
• ⨅ (R:ℝ≥0∞) (_:IsCoveringWith s R), R is the current definition
• ⨅ (x∈ s) (y:α) (_:IsCoveringWith s (edist x y)), edist x y is a variation on the current definition where you only consider relevant distances
  i've tried to prove the first and second equivalent, but i haven't succeeded yet...

[Edward van de Meent]

for reference: a MWE with my proofs

import Mathlib.Topology.EMetricSpace.Basic
open ENNReal Set

variable {α:Type*} [PseudoEMetricSpace α] (s:Set α)

def IsCoveringWith (R:ℝ≥0∞):Prop := ⋃ (x∈ s), (EMetric.ball x R) = univ

noncomputable def closest_distance (y:α): ℝ≥0∞ := ⨅ (x ∈ s), (edist x y)

noncomputable def covering_radius : ℝ≥0∞ := ⨆ (y:α), closest_distance s y
noncomputable def covering_radius' : ℝ≥0∞ := ⨅ (R:ℝ≥0∞) (_:IsCoveringWith s R), R
noncomputable def covering_radius'' : ℝ≥0∞ :=
  ⨅ (x∈ s) (y:α) (_:IsCoveringWith s (edist x y)), edist x y

example : covering_radius s ≤ covering_radius' s := by
  simp_rw [covering_radius,covering_radius',le_iInf_iff]
  simp_rw [IsCoveringWith,closest_distance,iSup_le_iff,iInf_le_iff]
  intro b hcov y c hc
  simp at hc
  have hy: y∈ univ := trivial
  rw [← hcov] at hy
  simp at hy
  obtain ⟨x,⟨hx,hx'⟩⟩ := hy
  obtain hz := hc x hx
  rw [edist_comm] at hx'
  exact hz.trans hx'.le

example: covering_radius' s ≤ covering_radius'' s:= by
  simp_rw [covering_radius'',covering_radius',IsCoveringWith]
  simp_rw [le_iInf_iff,iInf_le_iff,le_iInf_iff]
  intro x _ y hy _ hb
  exact hb (edist x y) hy

[Edward van de Meent]

ok. i've found a counterexample to the second and third definition being equal. use s={0} and α = {1 - (1 / n) | n ∈ ℕ} ∪ s as subsets of ℝ, then the second definition gives 1 while the third gives ∞...