[Merged by Bors] - chore(data/real/ereal): fix addition and multiplication on ereal

[sgouezel]

The current version of multiplication on ereal is completely broken (it satisfies (-1) * (+∞) = +∞). The addition is not really broken, but it satisfies (-∞) + (+∞) = +∞, while the analogy with ennreal through the exponential and the logarithm suggest that a better convention would be (-∞) + (+∞) = -∞. We fix the multiplication (by defining one directly by hand) and tweak the addition to obey the better convention (by changing the definition from with_top (with_bot ℝ) to with_bot (with_top ℝ)).

---

[fpvandoorn]

LGTM

The proofs are quite long though.
I'm wondering if you can simplify a lot of the proofs like this:
define a function ereal.signed_ennreal : sign_type ->ennreal -> ereal (defined by "multiplication"), and then define (x : ereal) * (y : ereal) := ereal.signed_ennreal (x.sign * y.sign) (x.abs * y.abs). Since ereal.signed_ennreal x.sign x.abs = x you should get many properties about multiplication for free.

Do you want to try this? If not, I'm also fine with merging this as-is.

[sgouezel]

I thought about this approach, but I used the current definition to make sure that defeqs are good for multiplication (especially for bot and for top) (in fact maybe they would also work with the other definition, but that's less obvious). The proofs look long because I've squeezed the simps, but in fact they are completely automatic case disjunctions, so I'd rather keep the current definition.

[fpvandoorn]

Ok, then let's keep it as this for now.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests