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

feat(measure_theory/function/intersectivity): Bergelson Intersectivity Lemma #18732

Closed
wants to merge 26 commits into from
Closed

feat(measure_theory/function/intersectivity): Bergelson Intersectivity Lemma #18732

wants to merge 26 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Apr 4, 2023 •
edited by github-actions bot
Loading

Prove a weak version of the Bergelson intersectivity lemma. The proof gives the strong version, but we need natural density to state it. This is a prerequisite to Tao and Ziegler's recent paper Infinite partial sumsets in the primes.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR 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 Apr 4, 2023
@YaelDillies YaelDillies requested a review from a team as a code owner April 4, 2023 09:09
@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 Jun 11, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 11, 2023
@YaelDillies YaelDillies removed the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 11, 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 Jun 16, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 16, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 17, 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 Jun 21, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@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 Jun 21, 2023
urkud
urkud reviewed Jun 21, 2023
View reviewed changes
src/measure_theory/function/intersectivity.lean
refine ⟨{n | x ∈ s n}, λ hxs, _, λ u hux hu, _⟩,
-- This next block proves that a set of strictly positive natural density is infinite, mixed with
-- the fact that `{n | x ∈ s n}` has strictly positive natural density.
-- TODO: Separate it out to a lemma once we have a natural density API.
Copy link
Member

Choose a reason for hiding this comment

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

IMHO, you should separate it to a lemma now, then migrate to a new API when it's available.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Eh I'm not sure how to go about this. There's some plumbing involved and figuring it out is probably as hard as writing the density API in the first place. The density API is on my todo list, so I'm definitely not forgetting that todo.

@YaelDillies YaelDillies 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 Jul 15, 2023
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@YaelDillies
Copy link
Collaborator Author

Wait, why is this marked too-late?

@YaelDillies YaelDillies added not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 and removed too-late This PR was ready too late for inclusion in mathlib3 labels Sep 13, 2023
@YaelDillies
Copy link
Collaborator Author

Ported to LeanCamCombi

@YaelDillies YaelDillies deleted the bergelson_intersectivity branch November 18, 2023 11:24
@YaelDillies YaelDillies mentioned this pull request Mar 4, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 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
5 participants
@YaelDillies @mathlib-dependent-issues-bot @urkud @sgouezel @semorrison