[Merged by Bors] - feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. by Felix-Weilacher · Pull Request #10856 · leanprover-community/mathlib4

Felix-Weilacher · 2024-02-22T17:59:04Z

add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in MeasureTheory/Measure/NullMeasurable.lean to be an instance of this general construction.

The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition.

TODO: Similarly generalize things about AEMeasurable, where appropriate.

JADekker

I'm new to reviewing, so I just left some very basic comments. I think it looks good in general, thanks!

Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean

Co-authored-by: Josha Dekker <114015169+JADekker@users.noreply.github.com>

Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel · 2024-06-07T18:53:42Z

bors r+
Thanks!

… sigma filter. (#10856) add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in `MeasureTheory/Measure/NullMeasurable.lean` to be an instance of this general construction. The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition. *TODO*: Similarly generalize things about `AEMeasurable`, where appropriate. Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com>

mathlib-bors · 2024-06-07T19:37:33Z

Build failed (retrying...):

Build

mathlib-bors · 2024-06-07T20:04:39Z

Canceled.

github-actions · 2024-06-07T20:05:13Z

PR summary

Import changes

No significant changes to the import graph

Declarations diff

+ EventuallyMeasurable
+ EventuallyMeasurable.congr
+ EventuallyMeasurableSet
+ EventuallyMeasurableSet.congr
+ EventuallyMeasurableSpace
+ EventuallyMeasurableSpace.measurable_le
+ Measurable.comp_eventuallyMeasurable
+ Measurable.eventuallyMeasurable
+ Measurable.eventuallyMeasurable_of_eventuallyEq
+ MeasurableSet.eventuallyMeasurableSet
+ eventuallyMeasurableSet_of_mem_filter
+ measurableSingleton

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

fixing proof

forgot to fetch

…ity/mathlib4 into baire_category ???

Felix-Weilacher · 2024-06-07T22:03:23Z

I have fixed the conflict

ghost · 2024-06-08T16:50:49Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

… sigma filter. (#10856) add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in `MeasureTheory/Measure/NullMeasurable.lean` to be an instance of this general construction. The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition. *TODO*: Similarly generalize things about `AEMeasurable`, where appropriate. Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2024-06-08T18:34:03Z

Pull request successfully merged into master.

Build succeeded:

… sigma filter. (#10856) add a general construction of a measurable space consisting of sets measurable with respect to some underlying sigma algebra modulo a given sigma filter. Refactor basic definitions and lemmas in `MeasureTheory/Measure/NullMeasurable.lean` to be an instance of this general construction. The reason is that in the immediate future I would like to define Baire measurability in mathlib, and want to avoid repetition. *TODO*: Similarly generalize things about `AEMeasurable`, where appropriate. Co-authored-by: Felix-Weilacher <112423742+Felix-Weilacher@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Felix-Weilacher added 2 commits February 22, 2024 12:52

initial commit

bff3c62

Mathlib.lean imports

f29ba9f

Felix-Weilacher added the t-measure-probability Measure theory / Probability theory label Feb 22, 2024

EventuallyMeasurable imports

5f26e27

Felix-Weilacher added the awaiting-review label Feb 22, 2024

JADekker reviewed Apr 2, 2024

View reviewed changes

Felix-Weilacher and others added 2 commits April 2, 2024 13:14

Update Mathlib/MeasureTheory/Constructions/EventuallyMeasurable.lean

d19acd2

Co-authored-by: Josha Dekker <114015169+JADekker@users.noreply.github.com>

TODO in docstring

aeb1c62

ADedecker requested a review from sgouezel April 6, 2024 20:47

sgouezel reviewed May 4, 2024

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 4, 2024

Felix-Weilacher and others added 2 commits May 4, 2024 12:32

Apply suggestions from code review

3a85223

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

congr fixes

794aa19

Felix-Weilacher added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 4, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 4, 2024

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 13, 2024

docstring for baire

9680eb6

Felix-Weilacher added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 13, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 7, 2024

Merge branch 'master' into baire_category

7d65600

alreadydone added ready-to-merge This PR has been sent to bors. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed ready-to-merge This PR has been sent to bors. labels Jun 7, 2024

alreadydone removed the ready-to-merge This PR has been sent to bors. label Jun 7, 2024

Felix-Weilacher added 4 commits June 7, 2024 16:40

Merge remote-tracking branch 'origin/master' into baire_category

92afdeb

fixing proof

Merge remote-tracking branch 'origin/master' into baire_category

70aa943

forgot to fetch

Merge branch 'baire_category' of https://github.com/leanprover-commun…

9a9eaec

…ity/mathlib4 into baire_category ???

Measure.ae fix

c38df94

Felix-Weilacher added the awaiting-review label Jun 7, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 7, 2024

Felix-Weilacher added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 7, 2024

Merge branch 'master' into baire_category

f9b4f1a

alreadydone added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jun 8, 2024

mathlib-bors bot changed the title ~~feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter.~~ [Merged by Bors] - feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. Jun 8, 2024

mathlib-bors bot closed this Jun 8, 2024

mathlib-bors bot deleted the baire_category branch June 8, 2024 18:34

alreadydone removed the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jun 8, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. #10856

[Merged by Bors] - feat(MeasureTheory): generalize NullMeasurable to measurability mod a sigma filter. #10856
Felix-Weilacher wants to merge 14 commits intomasterfrom
baire_category

Felix-Weilacher commented Feb 22, 2024 •

edited by ADedecker

Loading

Uh oh!

JADekker left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Jun 7, 2024

Uh oh!

mathlib-bors bot commented Jun 7, 2024

Uh oh!

mathlib-bors bot commented Jun 7, 2024

Uh oh!

github-actions bot commented Jun 7, 2024 •

edited

Loading

Declarations diff

Uh oh!

Felix-Weilacher commented Jun 7, 2024

Uh oh!

ghost commented Jun 8, 2024

Uh oh!

mathlib-bors bot commented Jun 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

Felix-Weilacher commented Feb 22, 2024 • edited by ADedecker Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JADekker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Jun 7, 2024

Uh oh!

mathlib-bors bot commented Jun 7, 2024

Uh oh!

mathlib-bors bot commented Jun 7, 2024

Uh oh!

github-actions bot commented Jun 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary

Import changes

Declarations diff

Uh oh!

Felix-Weilacher commented Jun 7, 2024

Uh oh!

ghost commented Jun 8, 2024

Uh oh!

mathlib-bors bot commented Jun 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Felix-Weilacher commented Feb 22, 2024 •

edited by ADedecker

Loading

github-actions bot commented Jun 7, 2024 •

edited

Loading