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

Update blueprint section 10 #22

Merged
merged 62 commits into from
Jun 9, 2024
Merged

Update blueprint section 10 #22

merged 62 commits into from
Jun 9, 2024

Conversation

ldiedering
Copy link
Collaborator

Various rewrites in the blueprint to change from piecewise constant to smooth approximation, as already done in the Lean version.
Many other small changes and corrections to sync blueprint and Lean code, in particular some more \leanok's have been added.
However, I realized that the paper has changed regarding the "local oscillation" (this term does not even appear any more) and that the Lean code needs some updates of definitions to reflect this change before I can add more \leanok's to things from subsection 10.9 .

@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
More sorry's in Control_Approximation_Effect
332b181
@ldiedering
Cleanup of Carleson_on_the_real_line, part 1
5a53738
@ldiedering
Cleanup Carleson_on_the_real_line part 2
82a562c
@ldiedering
Cleanup, proved some minor lemmas
76b5908
@ldiedering
small improvements of control_approximation_effect; no change to ENNR…
ad122ec 
…eal yet
@ldiedering
Minor exploration of ideas but still stuck.
23d6860
@ldiedering
Minor additions in Basic
0c5f550
@ldiedering
Added dirichlet_Hilbert_eq lemma
4c3b00c
@ldiedering
le_CarlesonOperatorReal' shoud be mostly working now
78a6152
@ldiedering
Reorganized proof of control_approximation_effect'
bbc8b48
@ldiedering
Rewrote proof of control_approximation_effect for ENNReal
8e81093
@ldiedering
Slightly generalized rcarleson' and other minor changes
63ad820
@ldiedering
Improved a proof
0647291
@ldiedering
Filled in sorry's in Control_Approximation_Effect
b6f6bcf
@ldiedering
Further cleanup of Control_Approximation_Effect
bff22d8
@ldiedering
Updated classical_carleson to current version of control_approximatio…
c6641de 
…n_effect
@ldiedering
Further Cleanup of Control_Approximation_Effect
341900c
@ldiedering
Control_Approximation_Effect finally sorry-free :)
14b987d
@ldiedering
Cleanup CarlesonOperatorReal
ea60b6e
@ldiedering
Merge branch 'control_approximation_effect_ennreal_experiment'
3ace239
@ldiedering
Removed arguments for piecewise constant approximation
93fac8b
@ldiedering
Minor correction in the proof of integer ball cover
192cdbb
@ldiedering
Update blueprint section 10, add \leanok's
d1e58f1
@ldiedering
Merge branch 'master' of https://github.com/ldiedering/carleson
4b8a654
@ldiedering
Merge branch 'development'
9eb6008
@ldiedering
Corrected reference of Theorem 1.1
c02be26
@fpvandoorn fpvandoorn merged commit 823dd5f into fpvandoorn:master Jun 9, 2024
1 check passed
@fpvandoorn
Copy link
Owner

Thanks! I'll work on the existing Lean code in the upcoming week

@ldiedering ldiedering deleted the master branch June 9, 2024 14:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fpvandoorn fpvandoorn Awaiting requested review from fpvandoorn

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