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: generalize some lemmas using withDensity_apply'
#8383
Conversation
Perhaps |
Do we have a property |
I've defined s-finite measures in #8405, and proved there that |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Thanks to #8405 I could remove the |
rw [set_integral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν] | ||
#align measure_theory.measure.with_density_rn_deriv_to_real_eq MeasureTheory.Measure.set_integral_toReal_rnDeriv' | ||
|
||
lemma set_integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) : |
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 did not replace SigmaFinite ν
by SFinite ν
here because then HaveLebesgueDecomposition μ ν
cannot be inferred, which leads to this question: can the Lebesgue decomposition theorem be generalized to s-finite measures?
(if yes, let's not do it in this PR)
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.
Yes, many things hold for s-finite measures instead of sigma-finite (Fubini, for instance!). I'm not sure it's worth doing the change unless there are applications where it is useful to weaken some assumptions.
bors r+ |
@sgouezel added a version of `withDensity_apply` that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library. For results about `rnDeriv`, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
withDensity_apply'
withDensity_apply'
@sgouezel added a version of `withDensity_apply` that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library. For results about `rnDeriv`, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
@sgouezel added a version of `withDensity_apply` that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library. For results about `rnDeriv`, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
@sgouezel added a version of `withDensity_apply` that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library. For results about `rnDeriv`, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
@sgouezel added a version of
withDensity_apply
that does not require measurability of the set if the measure is s-finite. This PR uses that result in other files of the library.For results about
rnDeriv
, I put a prime on the version that assumes measurability of the set and no prime on the version for s-finite measures, as the second one should be the main use case.