Subtraction in extended reals/integers

Stream: mathlib4

[Brendan Seamas Murphy]

Has anyone had a reason to write down an expression like sup S - inf S, eg for measure theory? If so, was it a pain to work with? Did you have to do a lot of casesplitting or find it frustrating that none of the usual typeclass apply to subtraction except (basically) the data of it? I'm thinking of adding a function Set α → WithBot (WithTop α) which forms this difference when α is a complete commutative monoid with an ordered subtraction (this would include the naturals) and some API for it. But I don't want to reinvent the wheel if this is a problem that's been dealt with before

[Floris van Doorn]

For subtraction in ENNReal you want to look for lemmas with tsub in the name, see docs#OrderedSub and the lemmas below it. That is the notion of truncated subtraction.

[Brendan Seamas Murphy]

Yes, this is not about ENNReal

[Floris van Doorn]

Oh, that's what the topic name suggests. Using WithBot (WithTop α) is annoying when your type already has a top and/or bot. I recommend working using typeclasses that you expect WithBot (WithTop α) to have, and do it for an arbitrary type using those typeclasses.

[Brendan Seamas Murphy]

But I can't ask for typeclasses that say WithBot (WithTop α) has a well behaved subtraction because it doesn't. However if α does then the formal expression sup S - inf S is well behaved. And subtraction in the "extended reals" is not in the "extended nonnegative reals"

[Brendan Seamas Murphy]

Please ignore the remark about the natural numbers, the main cases of interest are the integers and the reals (which do not have top or bottom elements)

[Brendan Seamas Murphy]

(though we do sometimes want to talk about the natural numbers union ±infinity, see the defintion of krull dimension)

[Sébastien Gouëzel]

Why not just work with EReal, which already has a subtraction (defined by hand)? It is probably missing a lot of API because it hasn't been used a lot, but this API would definitely be worth adding.

[Brendan Seamas Murphy]

Because I'm actually more interested in integers

[Brendan Seamas Murphy]

I just figured it was more likely to have come up for reals in some corner of measure theory

[Sébastien Gouëzel]

In measure theory, we use extended nonegative reals and everything is much better behaved.

[Brendan Seamas Murphy]

Surely we have statements about integrals involving EReal?

[Yaël Dillies]

I don't actually think we do

[Sébastien Gouëzel]

Essentially none, no. Interesting functions are most often integrable or nonnegative, in the former case the (Bochner) integral takes values in a Banach space, in the latter case the (Lebesgue) integral takes values in the extended nonnegative reals.

[Brendan Seamas Murphy]

Huh, well that shows you how little I've interacted with that part of the library