Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem #15335

Closed
wants to merge 6 commits into from
Closed

feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem #15335

wants to merge 6 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jul 14, 2022 •
edited
Loading

Prove the lower bound on the Ruzsa-Szemerédi problem, in implicit, explicit and asymptotic form.

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jul 14, 2022
@YaelDillies YaelDillies requested a review from kmill July 14, 2022 08:56
@ericrbg
Copy link
Collaborator

ericrbg commented Aug 5, 2022

should this prove the explicit bound now?

@YaelDillies
Copy link
Collaborator Author

Yes, but I'm not sure how to state it. The problem is that the explicit bound would need to quantify over all graphs over a certain size, hence over types. Further, the construction in this PR only gives graphs with a number of vertices divisible by 6, so we would get an explicit only on a sixth of the values (ven if that's mathematically irrelevant).

Thoughts?

@b-mehta b-mehta added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Aug 13, 2022
@YaelDillies YaelDillies requested a review from a team as a code owner June 18, 2023 09:38
@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 18, 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. t-combinatorics Combinatorics and removed WIP Work in progress labels Jun 18, 2023
@kim-em kim-em added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 16, 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 Nov 18, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies
Copy link
Collaborator Author

Ported to LeanCamCombi

@YaelDillies YaelDillies deleted the ruzsa_szemeredi branch November 18, 2023 12:13
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@b-mehta b-mehta b-mehta left review comments

@kmill kmill Awaiting requested review from kmill

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-combinatorics Combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@YaelDillies @ericrbg @mathlib-dependent-issues-bot @b-mehta @kim-em