identifier for completed lebesgue measure

[affeldt-aist]

Motivation for this change

This PR introduces an identifier for the completed lebesgue measure and
a proof that the completed sigma-algebra is the same as the Caratheodory one.

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]

Structure looks good. There may be a way to compress those long proofs, but I can't see anything obvious. We'll need to generalize these results beyond R anyway. Maybe we can make progress then.

[affeldt-aist]

FTR, I compressed the proofs and gained about 40 lines before merging.