Commit 2022-03-28 11:38 f0c15be6

feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions (#12985) A function is almost everywhere strongly measurable if it is almost everywhere the pointwise limit of a sequence of simple functions. These are the functions that can be integrated in the most general version of the Bochner integral. As a prerequisite for the refactor of the Bochner integral, we define almost strongly measurable functions and build a comprehensive API for them, gathering in the file strongly_measurable.lean all facts that will be needed for the refactor. The API does not claim to be complete, but it is already pretty big.