[Merged by Bors] - feat(measure_theory): links between an integral and its improper version

[ADedecker]

This PR introduces ways of studying and computing ∫ x, f x ∂μ by studying the limit of the sequence ∫ x in φ n, f x ∂μ for an appropriate sequence φ of subsets of the domain of f.

---

There are a few things I'm not 100% happy with in this PR, so I'm open to suggestions. These are :

• the name of the new file (currently integral_eq_improper.lean)
• the name mono_ae_cover which isn't really clear
• the definition of mono_ae_cover involves some assumptions which may be a bit too strong, but I had some troubles when trying to loosen them
• in the part about Ixxs, I found myself duplicating a few things between the "prove f is integrable" and "integral of f is ..." versions of the lemmas, but factoring things out involves stating a lot of lemmas which won't be useful to anything else, so I'm not sure if I should do it

[benjamindavidson]

Just some suggestions for improving the syntax in the docstrings (most of these are just things that I think read better, not actual corrections).

[benjamindavidson]

Something strange: The name of this branch is mathlib-integral_limits (not mathlib_integral_limits). I think this prevented me from being able to clone the branch using leanproject get.

[ADedecker]

Thanks for the review @benjamindavidson, I should definitely try to improve my English. I'm tagging this as WIP again because I just found a way to make everything easier to use by extending growing_family to any sequence indexed by an archimedean ordered semiring, which avoids having to deal with coe in concrete applications. I should be able to finish this small refactor soon.

[benjamindavidson]

@ADedecker Your English is fine!!! Like I said, most of these are not corrections as much as they are preferences.

[sgouezel]

in this lemma, you are assuming that f is measurable. However, I think you can easily deduce from this one a version assuming only that f is almost everywhere measurable. From there, you can weaken all the assumptions in the subsequent lemmas, from measurability to almost everywhere measurability.

[ADedecker]

Instead of just using the measurable version to prove the ae_measurable one, I added a few lemmas to integrable_on.lean about ae-measurability of an indicator, which allows me to use ae_measurable all the way. Should I move these to a separate PR ?

[bors]

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

This looks great, thanks!
bors d+

[ADedecker]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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