Commit 2021-01-03 23:18 96948e45
View on Github →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
).