[Merged by Bors] - feat(order/limsup_liminf, order/filter/ennreal): add properties of limsup for ennreal-valued functions

[RemyDegenne]

---

[sgouezel]

I wonder if we could use a slightly more abstract definition to deduce many properties from things we already have on limsups: the essential supremum of a function is the limsup of this function along the almost-everywhere filter, I think.

[RemyDegenne]

I just looked at filter.limsup, and indeed it is very very close to what I defined. The lemma filter.limsup_eq even states f.limsup u = Inf {a : α | ∀ᶠ (n : β) in f, u n ≤ a}

I spent some time looking at existing definitions before writing the new code but I missed that one.

[RemyDegenne]

I am thinking about removing the ess_sup/ess_inf definitions entirely, as well as the ess_sup file. It looks like all the ess_sup lemmas do at the moment is translate an hypothesis µ \ne 0 into µ.ae.ne_bot when necessary, then call a limsup lemma.

I don't know where I should put the ennreal results. data/real/ennreal does not import filters and topology/instances/ennreal does not seem to be the right place either. Should I create an order/instances/ennreal file?

I tried generalizing the results beyond ennreal for a bit, but it looks like I would need new and very specific classes (something like a (conditionally?)_complete_canonically_linear_ordered_cancel_add_comm_monoid), so I'll keep ennreal.

[RemyDegenne]

TODO:

• rewrite the order_iso lemmas for galois connections instead of order_iso
• change the order_iso hypotheses from complete_lattice to conditionally_complete_lattice? (under enough boundedness assumptions on the filter)

[sgouezel]

a new file order/filter/ennreal.lean would be a good place, I think.

[sgouezel]

I am not sure I would have dropped completely the esssup file: even if it just boils down to restating limsup lemmas, it will certainly be useful for people that don't think of the essential supremum as the limsup along the ae filter (i.e., everyone :-)

[sgouezel]

bors r+
Thanks!

[bors]

Build failed:

• Build mathlib

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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