Metric spaces / real analysis

[malarbol]

This aims at centralizing conversations regarding metric spaces and real / functional analysis.

Concepts

• [x] distance functions
  • #1394
  • #1400
• [x] rework limits
  • #1378
• [ ] Lipschitz-continuous functions between metric spaces
  • #1417
• [ ] contracting functions between (pre|pseudo|)metric spaces
• [ ] total (pre|pseudo|)metric structures
  • #1403

Results

• [ ] continuity of algebraic functions
  • [x] negation is an isometry (#1398)
  • [x] addition is an isometry into the space of isometries (#1398)
  • [ ] multiplication is not uniformly continuous into the space of Lipschitz-continuous maps
  • [x] max is a short map into the metric space of short maps (#1398)
  • [ ] min is a short map
  • [x] the absolute value is a short map (#1398)
  • [ ] the distance functions are short maps into the space of short maps
• [ ] 1 + q + ... + qⁿ + ... = 1/(1-q)
• [ ] the squeeze theorem
• [ ] Banach fixed point theorem
• [ ] Extension of uniformly continuous functions from the rationals to the reals
• [ ] the exponential function

Related Issues

• [ ] #1354
• [ ] #1355
• [ ] #1360

Related Pull requests

• [x] #1371
• [x] #1402
• [x] #1398

References

• Real numbers at TypeTopology
• https://www.researchgate.net/publication/362446739_Point-free_Construction_of_Real_Exponentiation

[malarbol]

If I understood the logic

• sequence-Poset --> Poset of sequences in a poset
• type-sequence-Poset --> underlying type

I'm starting to think I got a few names wrong in the metric-spaces module. For example, function-Metric-Spaceshould be the metric space of functions between metric spaces, so what we called map-type-Metric-Space could (should?) be called type-function-Metric-Space. I remember @fredrik-bakke suggested this name at the time, but I didn't quite get why; I understand better now (hopefully).

Similarly, isometry-Metric-Space should be the metric space if isometries, and what I called isometry-Metric-Space now should be called type-isometry-Metric-Space; and the same goes for all spaces of functions between metric spaces. Maybe I could try to clean this up.

[malarbol]

Going further, I think we'd like cauchy-approximation-Metric-Space to be the metric space of Cauchy approximations in a metric space. With the current definition of "complete metric space", this will make cauchy-approximation-Complete-Metric-Space a bit problematic: we'd like it to be "the complete metric space of Cauchy approximations in a complete metric space" but I think this is only true if the underlying metric space is saturated. This suggests maybe we could modify the definition of completeness to include saturation: a complete metric space would be defined as "a saturated metric space where all Cauchy approximations are convergent".

[fredrik-bakke]

If I understood the logic

• sequence-Poset --> Poset of sequences in a poset
• type-sequence-Poset --> underlying type

I'm starting to think I got a few names wrong in the metric-spaces module. For example, function-Metric-Spaceshould be the metric space of functions between metric spaces, so what we called map-type-Metric-Space could (should?) be called type-function-Metric-Space. I remember @fredrik-bakke suggested this name at the time, but I didn't quite get why; I understand better now (hopefully).

Similarly, isometry-Metric-Space should be the metric space if isometries, and what I called isometry-Metric-Space now should be called type-isometry-Metric-Space; and the same goes for all spaces of functions between metric spaces. Maybe I could try to clean this up.

This is sort of it, yes, but the convention is not consistent across the library, so it is easy to confuse different readings, which I also do from time to time. To give you an example, the entry iso-Category is not the category of isomorphisms, that would be core-Category. Sorry I don't have clearer advice to give you on this right now, but I'll try to think up an explanation the next time I see some sort of confusion related to this.

[fredrik-bakke]

Usually, I try to think what a concept is most naturally understood to be. When it comes to cauchy approximations, I might not think of them first and foremost as elements of a new metric space. Rather, they are approximations in a given metric space. Therefore, cauchy-approximation-Metric-Space should be the type of cauchy approximations in a metric space.

[malarbol]

ok. I won't start any mass-renaming; I'm glad I asked. At some point soon I'll need the "metric space of isometries between metric spaces" and things like that, e.g. in #1398. Should it be called metric-space-isometry-Metric-Space then?

[lowasser]

I would be tempted to distinguish between these things by actually using the word of, e.g. metric-space-of-isometries-Metric-Space.

[malarbol]

Usually, I try to think what a concept is most naturally understood to be. When it comes to cauchy approximations, I might not think of them first and foremost as elements of a new metric space. Rather, they are approximations in a given metric space. Therefore, cauchy-approximation-Metric-Space should be the type of cauchy approximations in a metric space.

I understand it's a subtle distinction. For example when I think of a sequence in a partially ordered set, I don't immediately think of them as a partially ordered set, but as sequences in the underlying type. So, in this mindset, type-sequence-Poset would but sequence-Poset and sequence-Poset would be poset-sequence-Poset. Anyways, I'll just trust you on this and keep asking when I have doubts.

[malarbol]

I would be tempted to distinguish between these things by actually using the word of, e.g. metric-space-of-isometries-Metric-Space.

ok. I was thinking I should rename the module like this but I'm still not sure about the name. I have a few more PRs on the way before I really need to go there but I'll give it more thoughts.

[fredrik-bakke]

I would be tempted to distinguish between these things by actually using the word of, e.g. metric-space-of-isometries-Metric-Space.

This suggestion seems sound to me

[fredrik-bakke]

For sequences, though, I think the situation is a bit different. I wouldn't interpret sequence-Poset as the type of sequences in the carrier type of a poset, since there is already another common name for that, namely sequence ... — or sequence (type-Poset ....) which, if anything, would suggest the name sequence-type-Poset for the type of sequences in the underlying type of a poset.

[malarbol]

For sequences, though, I think the situation is a bit different. I wouldn't interpret sequence-Poset as the type of sequences in the carrier type of a poset, since there is already another common name for that, namely sequence ... — or sequence (type-Poset ....) which, if anything, would suggest the name sequence-type-Poset for the type of sequences in the underlying type of a poset.

mmh. we just merged #1388 with the names type-sequence-Preorder and type-sequence-Poset but maybe sequence-type-Preorder and sequence-type-Poset were better.

If I understand correctly, one key difference between sequence-type-Poset / sequence-Poset and isometry-Metric-Space is that the definition of sequence-type-Poset doesn't actually use the poset structure, it's just sequence (type-Poset ...) as you pointed out. On the other hand isometry-Metric-Space A B is not of the type Rel (type-Metric-Space A) (type-Metric-Space B) so it really depends on the Metric-Space structures and deserves the name isometry-Metric-Space. I still have some doubts, e.g. should anything be called function-Metric-Space? etc. But we'll just see along the way.