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

Lemma 7.5.1 #194

Open
wants to merge 30 commits into
base: master
Choose a base branch
from
Open

Lemma 7.5.1 #194

wants to merge 30 commits into from
+108 βˆ’22

Conversation

lakesare
Copy link
Contributor

@lakesare lakesare commented Dec 15, 2024 •
edited
Loading

[blueprint]

This can be merged!
PR review is appreciated.

TODOs

  • prove the remaining π“˜ u₁ βŠ‚ cube subgoal (lemma union_𝓙₅)
  • prove the second theorem (lemma pairwiseDisjoint_𝓙₅)
  • add \leanok
  • refactor (lemma union_𝓙₅)
  • refactor (lemma pairwiseDisjoint_𝓙₅)
  • update the blueprint to not use strict containment
  • address PR review suggestions

@lakesare
proof - proved barring the π“˜ u₁ βŠ‚ cube part
8e187a3 
proof - intermediate 2

proof - intermediate 3

proof - intermediate 4

proof - proved barring `π“˜ u₁ βŠ‚ cube` part
@lakesare lakesare force-pushed the lakesare/lemma_7.5.1 branch from dbecfd4 to 8e187a3 Compare December 17, 2024 00:16
@lakesare lakesare marked this pull request as ready for review December 18, 2024 03:32
@lakesare lakesare marked this pull request as draft December 19, 2024 02:30
@lakesare lakesare marked this pull request as ready for review December 19, 2024 09:02
fpvandoorn
fpvandoorn reviewed Dec 19, 2024
View reviewed changes
Copy link
Owner

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

This looks good!
I mostly have some stylistic comments,
I didn't open this PR in Lean myself to check whether all my suggestions work.

Carleson/Forest.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
Carleson/ForestOperator/LargeSeparation.lean Outdated Show resolved Hide resolved
@lakesare lakesare marked this pull request as draft December 20, 2024 06:54
@lakesare
Copy link
Contributor Author

Implemented the suggestions, they all worked.
Thanks for the review! This can be merged.

@lakesare lakesare marked this pull request as ready for review December 24, 2024 06:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fpvandoorn fpvandoorn fpvandoorn left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@lakesare @fpvandoorn