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: Order-connected sets in ℝⁿ are null-measurable #13633

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: Order-connected sets in ℝⁿ are null-measurable #13633

wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jun 8, 2024 •
edited by github-actions bot
Loading

Prove that the frontier of an order-connected set in ℝⁿ (with the ∞-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in ℝⁿ have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged RFC Request for comment t-topology Topological spaces, uniform spaces, metric spaces, filters t-measure-probability Measure theory / Probability theory labels Jun 8, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 8, 2024 •
edited
Loading

PR summary 8d30fcbe02

Import changes

No significant changes to the import graph

Declarations diff

+ IsAntichain.volume_eq_zero
+ IsLowerSet.null_frontier
+ IsUpperSet.null_frontier
+ Set.OrdConnected.nullMeasurableSet
+ Set.OrdConnected.null_frontier

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies
feat: Order-connected sets in ℝⁿ are measurable
b598ec4 
Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976
@YaelDillies
proof sketch
b108073
@YaelDillies
not Lebesgue point
0109c3f
@YaelDillies YaelDillies force-pushed the ord_connected_measurable branch from 6cbd8a8 to 0109c3f Compare June 17, 2024 12:18
@YaelDillies YaelDillies removed the RFC Request for comment label Jun 17, 2024
@kex-y
Copy link
Member

kex-y commented Jun 18, 2024

Thanks!
maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by JasonKYi.

@sgouezel sgouezel changed the title feat: Order-connected sets in ℝⁿ are measurable feat: Order-connected sets in ℝⁿ are null-measurable Jun 18, 2024
@sgouezel
Copy link
Contributor

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 18, 2024
@YaelDillies
feat: Order-connected sets in ℝⁿ are null-measurable (#13633)
766e2c1 
Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Order-connected sets in ℝⁿ are null-measurable [Merged by Bors] - feat: Order-connected sets in ℝⁿ are null-measurable Jun 18, 2024
@mathlib-bors mathlib-bors bot closed this Jun 18, 2024
@mathlib-bors mathlib-bors bot deleted the ord_connected_measurable branch June 18, 2024 13:04
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
feat: Order-connected sets in ℝⁿ are null-measurable (#13633)
a6b025f 
Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976
grunweg pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @grunweg
feat: Order-connected sets in ℝⁿ are null-measurable (#13633)
780eecc 
Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@YaelDillies @kbuzzard
feat: Order-connected sets in ℝⁿ are null-measurable (#13633)
f50fe1d 
Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero.

This is not so trivial as one might think. The proof Kexing and I came up with involves the Lebesgue density theorem.

Partially forward-port leanprover-community/mathlib3#16976
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

Assignees
No one assigned
Labels
maintainer-merge mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@YaelDillies @leanprover-community-mathlib4-bot @kex-y @sgouezel