ereal multiplication

Stream: maths

[Kevin Buzzard]

Sebastien Gouezel said:

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!

My conclusion from looking at the conventions which had been chosen last week was that probably a lot of these questions were regarded as junk questions even by the analysts (for example -infty * +infty = +infty was true for a long time and nobody complained until today.) I had just assumed that because nobody had flagged these issues before that they must be questions which don't come up. As an algebraist I do not agree that the only meaningful answer to (-1) * (+∞) is -∞, I want to argue that infinity itself is a junk concept in algebra; no ring can ever contain infinity, for example. I think arguing that "$(-1)\times x$ must be $-x$" doesn't work; there are plenty of statements that also "must" be true like $x+1>x$ and $x/x=1$, and the moment you add infinity they cannot all be true at the same time because algebra breaks with infinity, so something has to give somewhere. I think the only thing that matters is when you have some application which is sensible and which needs a different convention for infinity, so if you've found one then go ahead and make the change! You argued coherently that $0\times\infty=0$ should be true recently because it was a useful convention for analysis, but I think it's risky to start arguing that conventions should be changed just because something which "must" be true isn't true.

[Damiano Testa]

I agree with Kevin considering ∞ a junk value.

However, thinking of ereal as the "2-point compactification of real", I would be happy to know that multiplication by negative reals is a homeomorphism and would therefore be happier if (-1) * (+∞) were equal to -∞! :smile:

Also, should the topic by "ereal multiplication"? I think that Reid's comment arose from this.

[Sebastien Gouezel]

Yes, wrong topic title, sorry. Corrected!

[Vincent Beffara]

Do you have any idea of a change of definition for ereal? It seems to appear only in 7 files in mathlib so the changes involved would be minimal in any case.

[Sebastien Gouezel]

I'm switching to with_bot (with_top R) to make sure that (-∞) + (+∞) = -∞ (which is the right convention by analogy with the probability theory one). And I'm giving a definition from scratch for the multiplication, since you can't do it in two steps as we do for the other operations (what would be (-1) * (+∞) on with_top R). It's not as painful as I was fearing!

[Pedro Sánchez Terraf]

Sebastien Gouezel said:

I'm switching to with_bot (with_top R) to make sure that (-∞) + (+∞) = -∞ (which is the right convention by analogy with the probability theory one).

Is that * in place of +? Perhaps there is another analogy I'm missing!

[Yuyang Zhao]

Pedro Sánchez Terraf said:

Sebastien Gouezel said:

I'm switching to with_bot (with_top R) to make sure that (-∞) + (+∞) = -∞ (which is the right convention by analogy with the probability theory one).

Is that * in place of +? Perhaps there is another analogy I'm missing!

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/bot_eq_zero_class/near/309165196

[Sebastien Gouezel]

It's +. There are two things which are wrong currently on ereal, one about * (which is just plain wrong) and one about + (which is not really plain wrong because there is no canonical choice for (-∞) + (+∞), but arguably this one should better be -∞ so that the exponential becomes an isomorphism with ennreal). I am fixing both.

[Sebastien Gouezel]

#17770

[Kevin Buzzard]

I should apologise for defining ereal as with_top (with_bot ℝ) instead of with_bot (with_top ℝ) -- at the time I could see no clear difference! I do like your explanation that addition in ereal should be compatible with multiplication on ennreal via exp/log, and you'd already convinced me that 0 * \infty = 0 was a good idea in ennreal.

[Vincent Beffara]

Do we actually use multiplication in ereal a lot ?

[Kevin Buzzard]

I don't think we use ereal a lot. IIRC I only made the definition because I wanted to get some practice using with_bot and trying to understand the concept of a type synonym (at the time with_bot X was defined to be option X and this might still be the case).

[Vincent Beffara]

Yes I counted 7 files in which it is used. It might be more natural to equip it with just the addition and smul from the reals or something. Unless it makes integrals against signed measures weird or something?

[Sebastien Gouezel]

Vincent Beffara said:

Do we actually use multiplication in ereal a lot ?

No, we don't (otherwise, someone would have already noticed it and fixed it). But it's not a reason to have it wrong :-)

[Vincent Beffara]

I mean, one way to not have it wrong is to not have it at all

[Sebastien Gouezel]

Sure. But with the PR we have it, and we have it right.