Zulip Chat Archive

Stream: Is there code for X?

Topic: Does mathlib have infinity and a type of extended reals?


view this post on Zulip Lars Ericson (Dec 02 2020 at 18:37):

In mathlib I see "native float infinity". I don't immediately see the "conceptual" infinity. Two questions:

Q1. Where is abstract infinity oo in mathlib?
Q2. Is there a definition of "extended reals" that is something like Rbar = R + {-oo, oo}?

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 18:37):

docs#ereal

view this post on Zulip Yury G. Kudryashov (Dec 10 2020 at 21:11):

We have docs#real, docs#nnreal, docs#ennreal, and docs#ereal

view this post on Zulip Rémy Degenne (Dec 11 2020 at 08:43):

note that ereal is rather incomplete : it looks like it does not have has_mul for example. ereal is defined as with_bot(with_top(R)) and the with_top construction comes with a mul, but it looks like the with_bot does not (unless I am missing an order_dual statement somewhere). And even if you wrote a has_mul for with_bot, the resulting mul would be strange : you would have (-1)*(+oo) = +oo (and not -oo like you would maybe expect).

view this post on Zulip Damiano Testa (Dec 11 2020 at 08:46):

Also, what would -∞ * +∞ equal?

view this post on Zulip Ruben Van de Velde (Dec 11 2020 at 08:46):

37

view this post on Zulip Damiano Testa (Dec 11 2020 at 08:46):

You are completely right!!

view this post on Zulip Rémy Degenne (Dec 11 2020 at 08:47):

from the order of the with_bot(with_top(R)) construction, assuming that you define the mul of bot as done with top, it would be -oo

view this post on Zulip Eric Wieser (Dec 11 2020 at 08:47):

I assume you meant to ask what -∞ + +∞ is? Coming from floating point, -∞ * +∞ = -∞ seems like the obvious choice.

view this post on Zulip Damiano Testa (Dec 11 2020 at 08:49):

I thought that it was the multiplication that people were talking about, but you are right, addition also has its problems. However, I now realize that the problems might simply be in my head, since it may in practice not matter much how you define the non-sensical operations. I still need to interiorize the division-by-zero conundrum...

view this post on Zulip Rémy Degenne (Dec 11 2020 at 08:52):

I just tested the additive version : for ereal, bot + top = top

view this post on Zulip Rémy Degenne (Dec 11 2020 at 08:54):

because I was wrong about the definition : it is ereal = with_top (with_bot ℝ)

view this post on Zulip Rémy Degenne (Dec 11 2020 at 08:55):

hence the rule is that for all x in with_bot ℝ, x + top = top

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 11:57):

I wrote ereal and because I'm a mathematician and I did not have good answers for things like -infty+infty and 0 * infty I simply did not define them. In the analogous Isabelle code (written by a computer scientist) they're all defined and take on some random values for these weird cases. I'm sure the maintainers would happily accept a PR which adds all these functions and then proves all the lemmas in the Isabelle file (which I think I left a link to in the docstring?). The proofs are all easy by cases of course.


Last updated: May 16 2021 at 05:21 UTC