Zulip Chat Archive

Stream: maths

Topic: ennreal multiplication


Sebastien Gouezel (Nov 29 2022 at 10:07):

With the multiplication we have currently on ennreal (a.k.a. the extended reals), the following lemma is proved in the library:

lemma mul_top (x : ereal) (h : x  0) : x *  =  := with_top.mul_top h

Does everyone agree our definition is nonsense for, say, x = -1?

Kevin Buzzard (Nov 29 2022 at 10:12):

ha ha we were laughing at this very lemma at Xena last Thursday! I'm an algebraist, I don't multiply by infinity, I consider infinity a junk value. If you analysts actually find situations where you want to multiply infinity by -1 then surely go ahead and change it to whatever junk value you want the answer to be :-) Currently the graph of the function is spectacularly discontinuous at x=0, it's like infinity minus the Dirac delta "function".

Sebastien Gouezel (Nov 29 2022 at 10:18):

When you have +∞ and -∞, even algebraists should agree that the only meaningful answer for (-1) * (+∞) is -∞. Otherwise, negation does not even coincide with multiplication with -1!

Reid Barton (Nov 29 2022 at 10:36):

You are talking about just ereal and not ennreal, right?

Sebastien Gouezel (Nov 29 2022 at 10:56):

Yes, it's just for ereal that what we have is nonsense.


Last updated: Dec 20 2023 at 11:08 UTC