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(measure_theory/integral): lintegral_tsum' #17309

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(measure_theory/integral): lintegral_tsum' #17309

wants to merge 6 commits into from

Conversation

AlexKontorovich
Copy link
Collaborator

@AlexKontorovich AlexKontorovich commented Nov 2, 2022 •
edited

A version of lintegral_supr_directed and lintegral_tsum assuming only ae_measurable and not measurable.

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Open in Gitpod

@AlexKontorovich AlexKontorovich requested a review from a team as a code owner November 2, 2022 13:58
@AlexKontorovich AlexKontorovich added awaiting-review The author would like community review of the PR t-measure-probability Measure theory / Probability theory labels Nov 2, 2022
@AlexKontorovich AlexKontorovich changed the title feat(measure_theory/integral): lintegral_supr_directed' feat(measure_theory/integral): lintegral_tsum' Nov 2, 2022
@fpvandoorn
Copy link
Member

I think it would be nicer if you remove the old lintegral_tsum, since the new version is strictly more general.
Also, the name lintegral_supr_directed should be for the most general/useful version (the old lintegral_supr_directed can be called lintegral_supr_directed_of_measurable or something).

@fpvandoorn
Copy link
Member

You should go through all occurrences of lintegral_tsum in the library (find them using ctrl+shift+F in VSCode) and add an .ae_measurable where appropriate.

@fpvandoorn fpvandoorn 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 Nov 7, 2022
@AlexKontorovich AlexKontorovich 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 Nov 7, 2022
@fpvandoorn
Copy link
Member

Thanks!

bors d+

Please merge once CI passes.

@bors
Copy link

bors bot commented Nov 7, 2022

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

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 7, 2022
@AlexKontorovich
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Nov 8, 2022
@AlexKontorovich @hrmacbeth
feat(measure_theory/integral): lintegral_tsum' (#17309)
946ab79 
A version of `lintegral_supr_directed` and `lintegral_tsum` assuming only `ae_measurable` and not `measurable`.

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
@bors
Copy link

bors bot commented Nov 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/integral): lintegral_tsum' [Merged by Bors] - feat(measure_theory/integral): lintegral_tsum' Nov 8, 2022
@bors bors bot closed this Nov 8, 2022
@bors bors bot deleted the lintegral_supr_directed_prime branch November 8, 2022 02:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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
2 participants
@AlexKontorovich @fpvandoorn