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

[Merged by Bors] - feat: Levy-Prokhorov topology is finer than convergence in distribution #10406

Closed
wants to merge 39 commits into from

Conversation

kkytola
Copy link
Collaborator

@kkytola kkytola commented Feb 10, 2024

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.


Open in Gitpod

@kkytola kkytola added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters t-measure-probability Measure theory / Probability theory labels Feb 10, 2024
kkytola and others added 2 commits February 10, 2024 22:14
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 10, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 17, 2024
@kkytola kkytola 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 Mar 16, 2024
Copy link
Contributor

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

Looks good to me, thanks!
bors d+

Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 16, 2024

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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 16, 2024
@kkytola
Copy link
Collaborator Author

kkytola commented Mar 17, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 17, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@mathlib-bors
Copy link

mathlib-bors bot commented Mar 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Levy-Prokhorov topology is finer than convergence in distribution [Merged by Bors] - feat: Levy-Prokhorov topology is finer than convergence in distribution Mar 17, 2024
@mathlib-bors mathlib-bors bot closed this Mar 17, 2024
@mathlib-bors mathlib-bors bot deleted the kkytola/LevyProkhorov_le branch March 17, 2024 15:23
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
utensil pushed a commit that referenced this pull request Mar 26, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Louddy pushed a commit that referenced this pull request Apr 15, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
…on (#10406)

This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated t-measure-probability Measure theory / Probability theory t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants