Lebesgue differentiation theorem and applications

[affeldt-aist]

Motivation for this change

This is track D of issue #965

~~This is based of PR #995~~ (merged)

~~Based on PR #1121~~ (merged)

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

• [x] added corresponding documentation in the headers

Compatibility with MathComp 2.0

• [ ] I added the label TODO: HB port to make sure someone ports this PR to the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

i have not yet done the changelog and I have not yet moved the lemmas to the right files but this might wait a first round of review I think there is also still some room for improvement in the last bit (FTC0 and density) and I plan to go on revising it but I do not want to delay the review more than that