Skip to content

[Merged by Bors] - feat(Archive): Buffon's Needle #10189

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
Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat(Archive): Buffon's Needle #10189

wants to merge 20 commits into from
+361 −0

Conversation

@enricozb
Copy link
Contributor

@enricozb enricozb commented Feb 2, 2024 •
edited by eric-wieser
Loading

@enricozb enricozb changed the title Enricozb/buffon Formalization of Buffon's Needle Feb 2, 2024
@enricozb enricozb marked this pull request as ready for review February 3, 2024 01:51
@enricozb enricozb added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 3, 2024
@jcommelin jcommelin changed the title Formalization of Buffon's Needle feat(Archive): Buffon's Needle Feb 3, 2024
jcommelin
jcommelin reviewed Feb 3, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

A super minor comment. A longer review should maybe be done by someone with a bit more familiarity with integration/measure theory in mathlib.

tb65536
tb65536 reviewed Feb 3, 2024
View reviewed changes
@tb65536 tb65536 added the t-measure-probability Measure theory / Probability theory label Feb 6, 2024
kex-y
kex-y reviewed Feb 13, 2024
View reviewed changes
kex-y
kex-y reviewed Feb 13, 2024
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde reviewed Feb 13, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

Thanks for this! A few stylistic comments below. Maybe we could also add some more documentation about how the proof works, next to each of the main lemmas?

@enricozb
Copy link
Contributor Author

enricozb commented Feb 13, 2024

Thanks for the thorough reviews!

Since there have been some changes to pdf.IsUniform, I was able to remove some unnecessary lemmas. And I think the naming and styling is in line with the guide.

@kex-y
Copy link
Member

kex-y commented Feb 19, 2024

There was a new PR which changed uniform distribution a bit. Can you merge master and see if it still compiles?

@enricozb
Copy link
Contributor Author

enricozb commented Feb 19, 2024

There was a new PR which changed uniform distribution a bit. Can you merge master and see if it still compiles?

Indeed some of my rewrites that made use of the old definition (Measure.map B ℙ = (μ s)⁻¹ • μ.restrict s) have broken.

@enricozb
Copy link
Contributor Author

enricozb commented Feb 19, 2024

Ok, looks like it wasn't hard to fix. Updated

@enricozb enricozb requested a review from kex-y February 19, 2024 11:59
kex-y
kex-y reviewed Feb 19, 2024
View reviewed changes
kex-y
kex-y reviewed Feb 19, 2024
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Mar 18, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

I don't know enough about probability to be confident in my review, but it mostly looks good to me. You might want to merge master into this branch to make sure nothing broke since you made the PR

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically 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 Mar 21, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 24, 2024

This PR/issue depends on:

@enricozb enricozb added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 30, 2024
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Apr 18, 2024
View reviewed changes
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link

github-actions bot commented Apr 18, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 18, 2024
eric-wieser
eric-wieser reviewed Apr 19, 2024
View reviewed changes
@enricozb enricozb requested a review from eric-wieser April 22, 2024 11:29
eric-wieser
eric-wieser reviewed Apr 22, 2024
View reviewed changes
eric-wieser
eric-wieser approved these changes Apr 22, 2024
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

LGTM, thanks! Just some very minor style nits; feel free to merge after addressing the ones you agree with.

@eric-wieser
Copy link
Member

eric-wieser commented Apr 22, 2024

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 22, 2024

✌️ enricozb 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Apr 22, 2024
@enricozb
Copy link
Contributor Author

enricozb commented Apr 23, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Apr 23, 2024
@enricozb
feat(Archive): Buffon's Needle (#10189)
e408da1 
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Buffon's.20Needle/near/419359856)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Archive): Buffon's Needle [Merged by Bors] - feat(Archive): Buffon's Needle Apr 23, 2024
@mathlib-bors mathlib-bors bot closed this Apr 23, 2024
@mathlib-bors mathlib-bors bot deleted the enricozb/buffon branch April 23, 2024 06:32
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
@enricozb @Jun2M
feat(Archive): Buffon's Needle (#10189)
5b43be9 
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Buffon's.20Needle/near/419359856)
callesonne pushed a commit that referenced this pull request May 16, 2024
@enricozb @callesonne
feat(Archive): Buffon's Needle (#10189)
dead09d 
[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Buffon's.20Needle/near/419359856)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@kex-y kex-y kex-y left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

10 participants

@enricozb @kex-y @leanprover-community-mathlib4-bot @eric-wieser @jcommelin @tb65536 @YaelDillies @Ruben-VandeVelde @kmill