-
Notifications
You must be signed in to change notification settings - Fork 297
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): image of Lebesgue measure under shift/rescale #3760
Conversation
Add lemmas `preimage_mul_const_Ixx` and `preimage_const_mul_Ixx`. Other changes: * `to_units` doesn't work with `to_additive`, so move the `to_fun` part to `units.mk'`. * Generalize `equiv.mul_left` and `equiv.mul_right` to `units`.
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 is great! You have some ext
lemmas that were nicer than mine, but I generalized the last special case a bit, without giving up (much) usability.
Note: not all lemmas about =ᵐ
consistently use ae_eq
, some use eventually_eq
(this can be fixed in a different PR).
@@ -1049,7 +1233,13 @@ class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = | |||
/-- A measure `μ` is called finite if `μ univ < ⊤`. -/ | |||
class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ⊤) | |||
|
|||
export probability_measure (measure_univ) | |||
/-- Measure `μ` *has no atoms* if the measure of each singleton is zero.-/ | |||
class no_atoms_measure (μ : measure α) : Prop := |
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 I would prefer the name has_no_atoms
instead.
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've also seen the term continuous measure
for this property. The doc-string should mention this term.
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.
Renamed. Feel free to add "continuous measure" to the doc string. I don't want to do it myself because I never saw it (only "absolutely continuous" but this is a different property). I also commented on the definition. I don't want to change it in this PR but probably we should do it in the future.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
What is the status of this PR? Are you still working on the review comments? |
I'm sorry for the delay. I'll push update in about 1 hour. |
Thanks for the fixes. bors r+ |
Pull request successfully merged into master. Build succeeded: |
Depends on
#3757#3758#3759