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

Fix dependency and added leanok in Section 10.1 #24

Merged
merged 74 commits into from
Jun 10, 2024
Merged

Fix dependency and added leanok in Section 10.1 #24

merged 74 commits into from
Jun 10, 2024

Conversation

ldiedering
Copy link
Collaborator

No description provided.

ldiedering added 30 commits April 11, 2024 23:33
@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 and others added 28 commits May 29, 2024 03:23
@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
@ldiedering
Try to fix lake-manifest.json and lean-toolchain by reverting to prev…
babd40b 
…ious version.
@ldiedering
Merge branch 'fpvandoorn:master' into main
c6a9006
@ldiedering
Revert "Try to fix lake-manifest.json and lean-toolchain by reverting…
9f19aef 
… to previous version."

This reverts commit babd40b.
@ldiedering
Dowongrade UnicodeBasic and «doc-gen4»
92be523
@ldiedering
Merge branch 'main' of https://github.com/ldiedering/carleson
0dbdf8f
@ldiedering
Revert "Dowongrade UnicodeBasic and «doc-gen4»"
590d8df 
This reverts commit 92be523.
@ldiedering
lake-manifest.json update
876bac0
@ldiedering
Has this finally fixed the lake-manifest?
e5c0894
@ldiedering
Merge branch 'master' of https://github.com/ldiedering/carleson
864c1f2
@ldiedering
Add fourier-coeff-derivative as dependency of convergence-of-coeffs-s…
25a6de8 
…ummable
@ldiedering
Fetch lake-manifest.json from upstream
39227c1
@ldiedering
Added leanok to smooth-approximation
0f0f038
@ldiedering ldiedering changed the title Fix dependency in Section 10.1 Fix dependency and added leanok in Section 10.1 Jun 9, 2024
@fpvandoorn fpvandoorn merged commit 1098b7d into fpvandoorn:master Jun 10, 2024
1 check passed
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