Skip to content

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable#10041

Closed
mo271 wants to merge 6 commits intomasterfrom
mo271/mv_from_prob_kernel3
Closed

[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable#10041
mo271 wants to merge 6 commits intomasterfrom
mo271/mv_from_prob_kernel3

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Jan 26, 2024 •
edited
Loading

@mo271 mo271 changed the title Mo271/mv from prob kernel3 refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable Jan 26, 2024
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Jan 26, 2024 •
edited
Loading

Cannot move lintegral_iInf_directed_of_measurable to MeasureTheory/MeasurableSpace, because we need Lebesgue an dthat would lead to circular dependence. So moving to Lebesgue instead.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 26, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 27, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jan 28, 2024

This PR/issue depends on:

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 28, 2024
mo271
mo271 commented Jan 28, 2024
View reviewed changes
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 29, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2024
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Jan 31, 2024

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 31, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2024
@mo271
refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_m…
040db1b 
…easurable (#10041)

- [x] depends on: #10036 



Co-authored-by: Moritz Firsching <firsching@google.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jan 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable [Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv lintegral_iInf_directed_of_measurable Jan 31, 2024
@mathlib-bors mathlib-bors bot closed this Jan 31, 2024
@mathlib-bors mathlib-bors bot deleted the mo271/mv_from_prob_kernel3 branch January 31, 2024 15:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@Parcly-Taxel Parcly-Taxel Parcly-Taxel approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mo271 @RemyDegenne @Parcly-Taxel