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

Added some \lean's and \leanok's to the blueprint, split proofs in 10.2 and 11.6. #87

Merged
merged 151 commits into from
Jul 25, 2024
Merged

Added some \lean's and \leanok's to the blueprint, split proofs in 10.2 and 11.6. #87

merged 151 commits into from
Jul 25, 2024

Conversation

ldiedering
Copy link
Collaborator

No description provided.

@ldiedering
Initial experiments and formulation of the Classical Carleson Theorem
4b7e007
@ldiedering
Small improvement
92fedb5
@ldiedering
Formulated some more definitions and lemmas in context, a bit messy h…
41346b3 
…owever.
@ldiedering
Reduced main theorem to lemmas, modulo some left sorry's
2b97390
@ldiedering
Added missing last calc step
a330171
@ldiedering
State after meeting with recommendations
7b04c67
@ldiedering
Changed back to volume.real in all places; filled in some gaps; minor…
1e50909 
… corrections
@ldiedering
Proved that δ can be chosen less than π and moved this statement to a…
9c7f7aa 
… new lemma
@ldiedering
Stated lemma 10.4
1a0410b
@ldiedering
Incorporated recent updates to definitions and theorem numbering.
2659f12
@ldiedering
Created first outline of the proof of Lemma 10.4, i.e. of section 10.7
eaf5125
@ldiedering
Worked on section 10.7; problem occured with Finset in ballsCoverBalls
69089dd
@ldiedering
Proved lemma 10.37 (Hilbert kernel bound)
5f600d4
@ldiedering
Continued work on section 10.7 and moved this part to a separate file.
0f7d4bc
@ldiedering
Correct statement and proof of lemma Hilbert kernel bound.
1bf2e0a
@ldiedering
Minor changes
960aa77
@ldiedering
Added and proved some lemmas needed for fourierConv_ofTwiceDifferenti…
189d91f 
…able
@ldiedering
Almost done with the top level approximation argument.
21104fa
@ldiedering
Added and proved lemma about periodicity of deriv.
9c425d1
@ldiedering
Proved lemma int_sum_nat. Simpler parts of approximation argument done.
d325494
@ldiedering
Split the main file, part 1.
9defded
@ldiedering
Split main file, part 2.
f1966c1
@ldiedering
Added basic facts about partialFourierSum.
120cdf2
@ldiedering
Finished proof of Classical Carleson module Lemma 10.3
803d7ff
@ldiedering
Reshuffling sections
94bfd44
@ldiedering
Merge branch 'differentiable_f0_experiment' into proof_of_theorem_1_1
5c7bfaf
@ldiedering
Proved lemma 10.11 (lower secant bound)
4441f37
@ldiedering
Did much of the proof of lemma 10.14 (Hilbert kernel regularity).
588d2f5
@ldiedering
Proved Hilbert_kernel_regularity (almost)
ea33da6
@ldiedering
Reshuffled and added some definitions
6b5bcf5
@ldiedering ldiedering marked this pull request as draft July 19, 2024 22:04
@ldiedering ldiedering marked this pull request as ready for review July 19, 2024 22:46
@ldiedering ldiedering marked this pull request as draft July 21, 2024 10:15
@ldiedering ldiedering marked this pull request as ready for review July 25, 2024 09:06
@ldiedering ldiedering changed the title Added some \lean's and \leanok's to the blueprint. Added some \lean's and \leanok's to the blueprint, split proofs in 10.2 and 11.6. Jul 25, 2024
@fpvandoorn
Copy link
Owner

Thanks!

@fpvandoorn fpvandoorn merged commit 74b37f8 into fpvandoorn:master Jul 25, 2024
2 checks passed
@fpvandoorn
Copy link
Owner

Were the new comments at the bottom of CarlesonOperatorReal intentional?

@ldiedering
Copy link
Collaborator Author

Were the new comments at the bottom of CarlesonOperatorReal intentional?

Ah, yes. It's a suggestion for auxiliary statements to break up the proof of CarlesonOperatorReal_measurable that you sent me on Zulip but which I have not yet worked on.

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
@ldiedering @fpvandoorn