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 metric space Carleson variant for two-sided Calderon-Zygmund kernel #36

Merged
merged 119 commits into from
Jul 18, 2024
Merged

Added metric space Carleson variant for two-sided Calderon-Zygmund kernel #36

merged 119 commits into from
Jul 18, 2024

Conversation

ldiedering
Copy link
Collaborator

The previous chapter 10 is split into two parts.
The first one is a variant of metric space Carleson for a two-sided Calderon-Zygmund kernel and where the assumption on T* is replaced with a weaker one (for an operator without the two suprema).
The second one then uses this new variant to prove classical Carleson.

This changes mainly required to rewrite the previous 10.3 and 10.5 to the general case of doubling metric measure spaces.

@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
Update to new definitions
006f67c
@ldiedering
changed TODO's to fixme's
4613ce6
@ldiedering
Merge branch 'van_der_corput' into catch-up
48abb24
@ldiedering
Finished van der Corput and most of the part where it is used.
1b1cc83
@ldiedering
Proved uniformContinuous_of_continuous; Basic.lean is now sorry-free :)
2dc04e0
@ldiedering
Small corrections
193f62d
@ldiedering
Filled in sorry's in Dirichlet_kernel.lean
5ab4695
@ldiedering
Filled in more sorry's
4a2769f
@ldiedering
Added some fixme to blueprint
ed5672e
@ldiedering
Finally finished measurability of CarlesonOperatorReal. However, stil…
25a5dc6 
…l some Cleanup required.
@ldiedering
Adjusted Control_Approximation_Effect.lean; no sorry's outside of Car…
75f84f1 
…leson_on_the_real_line left :)
@ldiedering
Corrections and clarifications in real van der Corput.
e96c6ad
@ldiedering
Removed todo in Van_der_Corput.lean
77fa82f
@ldiedering
Updated 10.1 (Proof of Cotlar).
720b276
@ldiedering
Filled gaps in 10.2 (Calderon-Zygmund decomposition)
0ed3988
@ldiedering
Small corrections.
0cbe38f
@ldiedering
Merge branch 'master' of https://github.com/fpvandoorn/carleson
e0d7f2b
@ldiedering
Fixed some problems caused by updated definitions.
7c1e9a8
@ldiedering
Renamed operators and made Dirichlet uppercase everywhere.
7ac215c
@ldiedering
Filled in two small sorry's
f59311c
@ldiedering
Corrections in chapter 10
e93f8a4
@ldiedering ldiedering marked this pull request as ready for review July 16, 2024 07:16
@fpvandoorn fpvandoorn merged commit 2f85189 into fpvandoorn:master Jul 18, 2024
2 checks passed
@fpvandoorn
Copy link
Owner

Great! Thanks!

@pitmonticone pitmonticone mentioned this pull request Jul 19, 2024
Merged
fpvandoorn pushed a commit that referenced this pull request Jul 19, 2024
@pitmonticone
Golf #36 (#84)
aae66cc 
Golf #36
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
@ldiedering @fpvandoorn