Commit 2021-01-03 23:18 96948e45

feat(measure_theory): almost everywhere measurable functions (#5568) This PR introduces a notion of almost everywhere measurable function, i.e., a function which coincides almost everywhere with a measurable function, and builds a basic API around the notion. It will then be used in #5510 to extend the Bochner integral. The main new definition in the PR is h : ae_measurable f μ. It comes with h.mk f building a measurable function that coincides almost everywhere with f (these assertions are respectively h.measurable_mk and h.ae_eq_mk).