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.6 #176

Draft
wants to merge 9 commits into
base: master
Choose a base branch
from
Draft

Lemma 7.5.6 #176

wants to merge 9 commits into from

Conversation

lakesare
Copy link
Contributor

@lakesare lakesare commented Nov 14, 2024 •
edited
Loading

[blueprint]

This needs to be refactored, so leaving as a draft for now.

TODOs

  • prove have notMax : ¬IsMax J
  • add a typo correction (64⁻¹ version of the hypothesis) to blueprint
  • add \leanok
  • refactor

@lakesare
proof - ready [barring the "notMax" part]
b58d41a 
proof - elegant proof of `disjoint`

proof - prove `dist(c J, 𝔠 p) ≤ D^(s J) / 8 + 8 D^(𝔰 p)`

proof - prove `thus : ≥ 64⁻¹`

proof - confusion state

proof - first estimate [DONE]

proof - factor out `lemma first_estimate`

proof - second estimate, prove the "By definition of `t.𝓙₅ u₁ u₂`" line

proof - factor out `lemma byDefinition`

proof - refactor `lemma byDefinition`

proof - prove the 1st sentence [partially, IsMax is left]

proof - prove the 3rd sentence

proof - prove 4/7 of the "last calculation"

proof - prove 5/7 of the "last calculation"

proof- prove 6/7 of the "last calculation"

proof - prove 7/7 of the "last calculation"

proof - finish the proof
@lakesare
Merge branch 'master' of https://github.com/fpvandoorn/carleson into …
93e1b7d 
…lakesare/limited_scale_impact
@lakesare
refactor 1
afc0028 
refactor - factor out `hundred_lt_realD`

refactor - use `<;>`, use `all_goals`, use `gcongr with a pattern`

refactor - inline `useful`

refactor - remove unused variables

refactor -  factor out `calculation_1`

refactor - go bottom-up

refactor
@lakesare
blueprint - fix typo:64 => 64^-1
b45a28b
@lakesare
refactor 2
532e6f6
@lakesare lakesare changed the title Lemma 7.5.6 (limited scale impact) Lemma 7.5.6 Dec 15, 2024
@fpvandoorn
Copy link
Owner

fpvandoorn commented Dec 19, 2024 •
edited
Loading

I'm looking at the proof in the blueprint, and I think there is indeed a gap where you have your sorry. I'll ask the harmonic analysis group here what the right way is to fix this.

@fpvandoorn
Copy link
Owner

Nevermind, the proof is fine.
In your goal, assume by contradiction that s J + 3 < 𝔰 p. Then you can prove ¬IsMax J using Grid.isMax_iff and Grid.le_topCube

@lakesare
Copy link
Contributor Author

Great, that worked, thanks!

@lakesare
Copy link
Contributor Author

Is it okay if I leave refactoring to a later PR (either by myself or someone else, maybe add #TODO refactor to keep track of what theorems need to be refactored) and merge it, or is it better to refactor right away?

Assume I'll do minimal preparation before the merge, e.g. prepend every auxiliary lemma with limited_scale_impact (so lemma first_estimate would be renamed to lemma limited_scale_impact__first_estimate).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
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