Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(measure_theory/integral): finiteness of lower Lebesgue integral#16514

Closed
mcdoll wants to merge 10 commits intomasterfrom
mcdoll/lintegral_lemmas
Closed

[Merged by Bors] - feat(measure_theory/integral): finiteness of lower Lebesgue integral#16514
mcdoll wants to merge 10 commits intomasterfrom
mcdoll/lintegral_lemmas

Conversation

@mcdoll
Copy link
Copy Markdown
Member

@mcdoll mcdoll commented Sep 15, 2022

This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite.

Co-authored-by: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr
Co-authored-by: Remy Degenne remydegenne@gmail.com


Open in Gitpod

@mcdoll mcdoll added WIP Work in progress t-measure-probability Measure theory / Probability theory labels Sep 15, 2022
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 15, 2022
@mcdoll mcdoll added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Sep 15, 2022
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 15, 2022
@RemyDegenne RemyDegenne 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 Sep 15, 2022
mcdoll and others added 3 commits September 14, 2022 23:04
@mcdoll
Copy link
Copy Markdown
Member Author

mcdoll commented Sep 15, 2022

Maybe lintegral_norm_eq_of_ae_nonneg should use nnnorm?

@mcdoll mcdoll 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 Sep 15, 2022
@mcdoll mcdoll added the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 15, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 15, 2022
@RemyDegenne
Copy link
Copy Markdown
Collaborator

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 18, 2022
bors bot pushed a commit that referenced this pull request Sep 18, 2022
…16514)

This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite.

Co-authored-by: Sébastien Gouëzel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Remy Degenne <remydegenne@gmail.com>



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/integral): finiteness of lower Lebesgue integral [Merged by Bors] - feat(measure_theory/integral): finiteness of lower Lebesgue integral Sep 18, 2022
@bors bors bot closed this Sep 18, 2022
@bors bors bot deleted the mcdoll/lintegral_lemmas branch September 18, 2022 08:56
b-mehta pushed a commit that referenced this pull request Sep 21, 2022
…16514)

This PR proves that if a function is integrable and non-negative, then it's lower Lebesgue integral is finite.

Co-authored-by: Sébastien Gouëzel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Remy Degenne <remydegenne@gmail.com>



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-measure-probability Measure theory / Probability theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants