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.

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/disintegration): integral against cond_kernel #19066

Closed
wants to merge 34 commits into from
Closed

[Merged by Bors] - feat(probability/kernel/disintegration): integral against cond_kernel #19066

wants to merge 34 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

@RemyDegenne RemyDegenne commented May 23, 2023 •
edited

@RemyDegenne
integral of comp_prod
5e1154b
@RemyDegenne
move, rename, reorganize
0443123
@RemyDegenne
Merge remote-tracking branch 'origin/master' into RD_integral_kernel
7e0ae5f
@RemyDegenne
fix
51ea4c0
@RemyDegenne
remvoe merge lines
80a5ab1
@RemyDegenne
fix
d0e525e
@RemyDegenne
Merge remote-tracking branch 'origin/master' into RD_integral_kernel
dfe6607
@RemyDegenne
fix
c937840
@RemyDegenne
fix names
68f920d
@RemyDegenne
add set_integral variant
b9741cc
@RemyDegenne
remove an intro
193cb5f
@RemyDegenne
minor
1fa5be7
@RemyDegenne
place measurable lemmas in the right namespace
068ecae
@RemyDegenne
fix docstring
8fbf3c9
@RemyDegenne
fix
7112d4b
@RemyDegenne
Merge remote-tracking branch 'origin/RD_measurable_integral' into RD_…
8ea6f27 
…integral_kernel
@RemyDegenne
clean, docstrings, etc
eb6b613
@RemyDegenne
Merge remote-tracking branch 'origin/master' into RD_integral_kernel
f4a3d26
@RemyDegenne
remove some measurable assumptions
f8ee998
@RemyDegenne
move
dbb55da
@RemyDegenne
style
76d40fc
@RemyDegenne
add lintegral versions of 3 lemmas
9e9ca7a
@RemyDegenne
fix import
b9956e0
@RemyDegenne
Merge remote-tracking branch 'origin/master' into RD_integral_kernel
69dec03
@RemyDegenne
fix import
bd1c544
@RemyDegenne
review names
108e15e
@RemyDegenne
integral of cond_kernel
fcbc09f
@RemyDegenne
Merge remote-tracking branch 'origin/RD_integral_kernel' into RD_inte…
2ca4274 
…gral_cond_kernel
@RemyDegenne RemyDegenne added 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 23, 2023
@RemyDegenne RemyDegenne requested a review from a team as a code owner May 23, 2023 05:06
@RemyDegenne RemyDegenne added the awaiting-author A reviewer has asked the author a question or requested changes label May 23, 2023
@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 23, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@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
@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 23, 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
@sgouezel
Copy link
Collaborator

bors r+
Thanks!

@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 May 24, 2023
bors bot pushed a commit that referenced this pull request May 24, 2023
@RemyDegenne
feat(probability/kernel/disintegration): integral against `cond_kerne…
6315581 
…l` (#19066)




Co-authored-by: RemyDegenne <remydegenne@gmail.com>
@bors
Copy link

bors bot commented May 24, 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/disintegration): integral against cond_kernel [Merged by Bors] - feat(probability/kernel/disintegration): integral against cond_kernel May 24, 2023
@bors bors bot closed this May 24, 2023
@bors bors bot deleted the RD_integral_cond_kernel branch May 24, 2023 12:44
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
3 participants
@RemyDegenne @mathlib-dependent-issues-bot @sgouezel