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(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels #18976

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels #18976

wants to merge 26 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

@RemyDegenne RemyDegenne commented May 9, 2023 •
edited by github-actions bot

@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. t-measure-probability Measure theory / Probability theory labels May 9, 2023
@RemyDegenne RemyDegenne requested a review from a team as a code owner May 9, 2023 17:02
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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 May 10, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

sgouezel
sgouezel reviewed May 14, 2023
View reviewed changes
src/probability/kernel/integral_comp_prod.lean Outdated Show resolved Hide resolved
src/probability/kernel/integral_comp_prod.lean
end

lemma integrable_kernel_prod_mk_left (a : α)
{s : set (β × γ)} (hs : measurable_set s) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
Copy link
Collaborator

Choose a reason for hiding this comment

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

ditto.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I agree that I don't need hs for the has_finite_integral part of integrable. I am struggling with the ae_strongly_measurable half though.

Copy link
Collaborator

Choose a reason for hiding this comment

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

You're right, the assumption is necessary here.

src/probability/kernel/integral_comp_prod.lean Outdated 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 May 15, 2023
@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 May 23, 2023
@RemyDegenne RemyDegenne mentioned this pull request May 23, 2023
Closed
1 task
sgouezel
sgouezel reviewed May 23, 2023
View reviewed changes
Copy link
Collaborator

@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.

bors r+
Thanks!

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 May 23, 2023
bors bot pushed a commit that referenced this pull request May 23, 2023
@RemyDegenne
feat(probability/kernel/integral_comp_prod): Bochner integral against…
c0d694d 
… the composition-product of two kernels (#18976)
@bors
Copy link

bors bot commented May 23, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels [Merged by Bors] - feat(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels May 23, 2023
@bors bors bot closed this May 23, 2023
@bors bors bot deleted the RD_integral_kernel branch May 23, 2023 09:41
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
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@RemyDegenne @mathlib-dependent-issues-bot @sgouezel @leanprover-community-bot-assistant