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
[Merged by Bors] - feat(measure_theory): preliminaries for Haar measure #3195
Conversation
43d89a0
to
e829dc1
Compare
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.
Looks good to me.
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.
LGTM, but I would be happy to have the opinion of @urkud since he's into measure theory currently.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
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.
I think this looks really good now. However, I'm a bit hesitant to merge this, because of @urkud s ongoing refactor of measure theory and integration stuff.
Ok, I'm happy to let @urkud decide which PR to merge first (and to fix merge conflicts if my PR gets deferred). |
bors merge |
Move properties about lattice operations on encodable types to a new file. These are generalized from lemmas in the measure theory folder, for lattice operations and not just for `ennreal`. Also move them to the `encodable` namespace. Rename `outer_measure.Union_aux` to `encodable.Union_decode2`. Generalize some properties for outer measures to arbitrary complete lattices. This is useful for operations that behave like outer measures on a subset of `set \a`.
Build failed: |
bors d+ |
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
merge conflict |
Odd, I pushed a fix to |
Let's see if closing and reopening helps? |
bors merge |
Move properties about lattice operations on encodable types to a new file. These are generalized from lemmas in the measure theory folder, for lattice operations and not just for `ennreal`. Also move them to the `encodable` namespace. Rename `outer_measure.Union_aux` to `encodable.Union_decode2`. Generalize some properties for outer measures to arbitrary complete lattices. This is useful for operations that behave like outer measures on a subset of `set α`. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Thanks for fixing! |
Move properties about lattice operations on encodable types to a new file. These are generalized from lemmas in the measure theory folder, for lattice operations and not just for
ennreal
. Also move them to theencodable
namespace.Rename
outer_measure.Union_aux
toencodable.Union_decode2
.Generalize some properties for outer measures to arbitrary complete lattices. This is useful for operations that behave like outer measures on a subset of
set α
.Depends on
#3189 and #3190 and #3194