Generalizing the Hyperreal API

Stream: mathlib4

[Violeta Hernández]

Currently Mathlib does not have much of a development for the hyperreals, just a single 700 line file over at docs#Hyperreal. My proposal is to cut it down in half.

Most of the file is spent introducing such notions such as docs#Hyperreal.Infinite, docs#Hyperreal.Infinitesimal, and docs#Hyperreal.st. All of these can be generalized (and are useful! e.g. surreals) to the setting of a general (non-)Archimedean field. Specifically:

• Hyperreal.Infinite x: ArchimedeanClass.mk x < 0
• Hyperreal.Infinitesimal x: 0 < ArchimedeanClass.mk x
• Hyperreal.st x: ArchimedeanClass.stdPart x (I added this just a few days ago)
• Hyperreal.IsSt x r: 0 < ArchimedeanClass.mk (x - ↑r)
• Hyperreal.InfinitePos x: 0 < x ∧ ArchimedeanClass.mk x < 0
• Hyperreal.InfiniteNeg x: x < 0 ∧ ArchimedeanClass.mk x < 0

My idea is then to deprecate all of these predicates, and generalize whatever useful theorems exist about them to this broader setting of non-Archimedean fields. This would leave us with basically nothing about hyperreals proper, save for the definition and some very basic theorems about how these functions relate to the ultrafilters in their definition. Is this an ok thing to do?

[Violeta Hernández]

(Truthfully I'm skeptical on whether we even want hyperreals specifically in Mathlib, rather than more generally proving Łoś's theorem, but that's a separate discussion)

[Ruben Van de Velde]

That sounds sensible. It doesn't seem too bad to keep the definition and presumably the instance of ArchimedeanClass if it's not that much code

[Violeta Hernández]

Would the correct move be to just deprecate everything about these six predicates? Or do I also have to show that the API that exists on ArchimedeanClass is sufficient to prove all of the API that exists on Hyperreal?

[Violeta Hernández]

(after #33007, it basically should be)

[Ruben Van de Velde]

Well, picking a random example like docs#Hyperreal.isSt_iff_abs_sub_lt_delta - if you deprecate it in favour of a lemma about ArchimedeanClass.stdPart, ideally you'd replace the proof to be sure the replacement works as well as you expect