feat(measure_theory): the Vitali-Caratheodory theorem (#7766)
This PR proves the Vitali-Carathéodory theorem, asserting that a measurable function can be closely approximated from above by a lower semicontinuous function, and from below by an upper semicontinuous function.
This is the main ingredient in the proof of the general version of the fundamental theorem of calculus (when `f'` is just integrable, but not continuous).
