fixes #1313 and moves Egorov

[affeldt-aist]

Motivation for this change

fixes #1313

This PR also shuffles the contents of the file lebesgue_measure.v
so that lemmas that do not depend on Lebesgue's measure appear
before it (the Egorov theorem in particular).

Checklist

- [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

Docs changes are good. Putting the code in a less-dependent order certainly can't hurt. Although given the shape of the diff it's hard to tell if it helps. I'll make my usual plea for splitting these big files.

[affeldt-aist]

I also think that lebesgue_measure.v should be split, it not well named anyway, its first part is about real-valued measurable functions, I didn't go as far as appending its first part to measure.v because the latter is already very long, a new file like measurable_realfun.v might be better, what about recording the splitting idea as a issue for later (unless you think it is a better idea to do it now)?

[zstone1]

I think a measurable_realfun.v would be great. But it doesn't have to happen now. An issue is sufficient.