[Merged by Bors] - feat(measure_theory/tactic): add measurability tactic #7756
Conversation
… 1571 of lp_space.lean
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
RemyDegenne
added
awaiting-review
There was a problem hiding this comment.
This looks very good to me. The file-split makes sense. I'd be grateful if someone more tactic-inclined could have a look at the file measure_theory/tactic.lean (@robertylewis ? @fpvandoorn ?) as this will bitrot quickly if not merged soon.
| @@ -0,0 +1,76 @@ | |||
| /- | |||
There was a problem hiding this comment.
Could you add in this file a test for measurability?
There was a problem hiding this comment.
I am not sure about how to test that form yet, but I will look at other test files and find something.
There was a problem hiding this comment.
I really don't know how I should test that. measurability? just does show_term { measurability } and prints the term generated by the tactic. Hence if show_term works as intended and measurability succeeds on a test, then measurability? shows a term that succeeds.
I cannot find tests for show_term nor tests for the specific form tidy?. The tests for library_search simply report the expected message in a comment but don't test that what is returned actually match it. And actually the test in test/library_search/ordered_ring.lean does not match.
|
|
||
| Mark lemmas with `@[measurability]` to add them to the set of lemmas | ||
| used by `measurability`. Note: `to_additive` doesn't know yet how to | ||
| copy the attribute to the additive version. |
There was a problem hiding this comment.
This seems like something that should be fixed before merging
There was a problem hiding this comment.
Do you know how I would do that? I would very much like to do it. And then I'll make another PR to do it for the continuity tactic as well.
There was a problem hiding this comment.
Do I just add measurability to the list of names line 312 of algebra/group/to_additive.lean? I'll experiment with that file tomorrow and see if I can make it work.
There was a problem hiding this comment.
to_additive doesn't do this for continuity either, fwiw
There was a problem hiding this comment.
This is easily fixed after #5487 and need not hold up this PR.
github-actions
bot
added
the
merge-conflict
|
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
|
|
||
| Mark lemmas with `@[measurability]` to add them to the set of lemmas | ||
| used by `measurability`. Note: `to_additive` doesn't know yet how to | ||
| copy the attribute to the additive version. |
There was a problem hiding this comment.
This is easily fixed after #5487 and need not hold up this PR.
fpvandoorn
added
awaiting-author
github-actions
bot
removed
the
merge-conflict
|
bors r+ |
Add a measurability tactic defined in the file `measure_theory/tactic.lean`, which is heavily inspired from the continuity tactic. It proves goals of the form `measurable f`, `ae_measurable f µ` and `measurable_set s`. Some tests are provided in `tests/measurability.lean` and the tactic was used to replace a few lines in `integration.lean` and `mean_inequalities.lean`.
|
Build failed (retrying...): |
Add a measurability tactic defined in the file `measure_theory/tactic.lean`, which is heavily inspired from the continuity tactic. It proves goals of the form `measurable f`, `ae_measurable f µ` and `measurable_set s`. Some tests are provided in `tests/measurability.lean` and the tactic was used to replace a few lines in `integration.lean` and `mean_inequalities.lean`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Add a measurability tactic defined in the file
measure_theory/tactic.lean, which is heavily inspired from the continuity tactic. It proves goals of the formmeasurable f,ae_measurable f µandmeasurable_set s. Some tests are provided intests/measurability.leanand the tactic was used to replace a few lines inintegration.leanandmean_inequalities.lean.It is my first tactic and was obtained by iteratively modifying continuity until it worked, so please review it with extra care.
The majority of the changes in the PR, besides adding
[measurability]attibutes everywhere, are due to a split ofmeasurable_space.leanandmeasure_space.leaneach into two files.measurable_space_def.lean, which contains definitions (up to the definition of a measurable function), but without most of the measurability lemmas.outer_measure.leanthen depends only onmeasurable_space_def.lean, and the newmeasure_space_def.leandefines measure spaces (leaving out most properties) also importing onlymeasurable_space_defbut notmeasurable_space.The tactic then depends only on the def files, and the
[measurability]attribute is available for use inmeasurable_space.lean.I could also leave the files as they are and add the measurability attributes in the tactic file. This is already the way I dealt with the
measurable_setlemmas since I could not remove those from measurable_space_def because many were needed in pi_system, outer_measure or measure_space_def. I would like comments on the best way to proceed.