-
Notifications
You must be signed in to change notification settings - Fork 47
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Refactoring lemmas about composition in Lebesgue Measure #925
Refactoring lemmas about composition in Lebesgue Measure #925
Conversation
in this commit the new formulation of the lemmas have an apostrophe ('), to distinguish them from the old ones. This is done in order to don't break already proved theorems while i'm experimenting.
new name is the old name concatenated with _comp
Simplified lemma measurable_funM
I would name the non compositional lemmas |
Sorry, I failed to see you message before my nitpicking commit where I was essentially doing this renaming. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for your contribution Marco. You are surely right: the lemmas you pointed out ought better be provided in smaller lemmas to be composed with measurable_fun_comp
. I just added a commit with a changelog and nitpicking. See CONTRIBUTING.md for a few clues about style.
Naming is not yet perfect but we'll have the occasion to come back to it when addressing #916.
- a few more hints for closing measurable_fun lemmas - favoring composition leading to one lemma removal - add deprecation for removed lemmas
theories/lebesgue_measure.v
Outdated
@@ -1823,6 +1896,7 @@ move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr. | |||
by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv. | |||
Qed. | |||
|
|||
(*can this be changed?*) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This can indeed be changed advantageously by using measurable_fun_if
provided lemmas about the measurability of boolean comparison operators (_ < _, etc.). This approach should trigger a bit of cleaning also and might better be done as a different PR.
favor use of `measurable_fun_comp` Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]> Co-authored-by: affeldt-aist <[email protected]> Co-authored-by: Pierre Roux <[email protected]>
favor use of `measurable_fun_comp` Co-authored-by: Alessandro Bruni <[email protected]> Co-authored-by: Reynald Affeldt <[email protected]> Co-authored-by: affeldt-aist <[email protected]>
Motivation for this change
I've changed the formulation of some lemmas in the lebesgue measure theory.
The lemmas state that the measurability of functions in R is preserved when composed with
Things Done
Lemma measurable_funrM is now
instead of
Lemma measurable_funN is now
instead of
Lemma measurable_fun_exprn is now
instead of
Lemma measurable_fun_sqr is now
instead of
Automatic note to reviewers
Read this Checklist and put a milestone if possible.