[Merged by Bors] - feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions#12985
[Merged by Bors] - feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions#12985
Conversation
RemyDegenne
left a comment
There was a problem hiding this comment.
That was long, but since it's only simple API which is very similar to the measurable one that was not too bad.
We (or rather I) should extend the measurability tactic to (ae_)strongly_measurable.
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
|
Thanks! |
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
… 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.
|
Pull request successfully merged into master. Build succeeded: |
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.leanall facts that will be needed for the refactor. The API does not claim to be complete, but it is already pretty big.If reviewers find this more convenient, I could split the PR into two, a first bit on additional API for strongly measurable functions, and then what is really about ae strongly measurable functions.