Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: tendsto_of_integral_tendsto_of_monotone #11167

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: tendsto_of_integral_tendsto_of_monotone #11167

wants to merge 8 commits into from

Conversation

RemyDegenne
Copy link
Contributor

@RemyDegenne RemyDegenne commented Mar 5, 2024 •
edited

Add tendsto_of_integral_tendsto_of_monotone, as well as ...of_antitone and the corresponding results for lintegral.

Also:

  • move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
  • add lintegral_iInf', a version of lintegral_iInf for a.e.-measurable functions. We already have the corresponding lintegral_iSup'.

Open in Gitpod

@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR t-measure-probability Measure theory / Probability theory WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Mar 5, 2024
@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Mar 6, 2024
sgouezel
sgouezel reviewed Mar 6, 2024
View reviewed changes
Copy link
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean Show resolved Hide resolved
Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Integral/Lebesgue.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Integral/Lebesgue.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Integral/Lebesgue.lean Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 6, 2024
@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 6, 2024
@RemyDegenne RemyDegenne mentioned this pull request Mar 6, 2024
Closed
1 task
sgouezel
sgouezel reviewed Mar 8, 2024
View reviewed changes
Copy link
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm happy with your code. Can you check if you are happy with my addition, and then send it to bors or change whatever you like?
bors d+

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 8, 2024

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 8, 2024
@RemyDegenne
Copy link
Contributor Author

Thanks a lot for the improvements!

@RemyDegenne
Copy link
Contributor Author

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Mar 9, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 9, 2024
@RemyDegenne @sgouezel
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
95abf56 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: tendsto_of_integral_tendsto_of_monotone [Merged by Bors] - feat: tendsto_of_integral_tendsto_of_monotone Mar 9, 2024
@mathlib-bors mathlib-bors bot closed this Mar 9, 2024
@mathlib-bors mathlib-bors bot deleted the RD_tendstoIntegral branch March 9, 2024 09:31
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@RemyDegenne @sgouezel @kbuzzard
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
0e80c16 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@RemyDegenne @sgouezel @dagurtomas
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
f04c756 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@RemyDegenne @sgouezel @utensil
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
268dfad 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@RemyDegenne @sgouezel @Louddy
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
7b4bbd6 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@RemyDegenne @sgouezel @uniwuni
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
8008bac 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@RemyDegenne @sgouezel @callesonne
feat: tendsto_of_integral_tendsto_of_monotone (#11167)
0b5312b 
Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`.

Also:
- move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue.
- add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
delegated ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@RemyDegenne @sgouezel @leanprover-community-mathlib4-bot