-
Notifications
You must be signed in to change notification settings - Fork 298
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/integral/set_integral): First moment method #18731
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This PR/issue depends on:
|
measure. -/ | ||
lemma measure_le_set_integral_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : integrable_on f s μ) | ||
(hs : null_measurable_set s μ) : | ||
0 < μ {x ∈ s | f x ≤ ∫ a in s, f a ∂μ / (μ s).to_real} := |
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.
Can you add the lintegral
version as well?
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.
Combining this with @sgouezel's suggestion, should I define laverage
for the Lebesgue average of an ennreal
-valued function?
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 just want to say I don't have any opinion on defining laverage
since I'm not sure of any cases where it is more convinent than writting the definition out explicitly.
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 turns out to be much more work than expected, so I am leaving a todo. You can have a look at the current state of things on branch first_moment_lintegral
.
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 happy with this. Can you have another look @sgouezel?
Since there's not been anymore comments lets merge this! |
🚀 Pull request has been placed on the maintainer queue by JasonKYi. |
bors r+ |
Integrable functions are smaller/larger than their mean on a set of positive measure. We prove it for the Bochner and Lebesgue integrals.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Partially forward-port leanprover-community/mathlib#18731
Also correct some `simp`s. Partially forward-port leanprover-community/mathlib#18731
Forward-port leanprover-community/mathlib#18731 Also sync some parentheses with the lates `mathport` output.
Also correct some `simp`s. Partially forward-port leanprover-community/mathlib#18731
Also correct some `simp`s. Partially forward-port leanprover-community/mathlib#18731
Also correct some `simp`s. Partially forward-port leanprover-community/mathlib#18731
Forward-port leanprover-community/mathlib#18731 Also sync some parentheses with the lates `mathport` output. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Forward-port leanprover-community/mathlib#18731 Also sync some parentheses with the lates `mathport` output. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Forward-port leanprover-community/mathlib#18731 Also sync some parentheses with the lates `mathport` output. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Integrable functions are smaller/larger than their mean on a set of positive measure. We prove it for the Bochner and Lebesgue integrals.