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

Commits on Apr 11, 2024

  1. Initial experiments and formulation of the Classical Carleson Theorem

    @ldiedering
    ldiedering committed Apr 11, 2024
    Configuration menu
    Copy the full SHA
    4b7e007 View commit details
    Browse the repository at this point in the history

  2. Small improvement

    @ldiedering
    ldiedering committed Apr 11, 2024
    Configuration menu
    Copy the full SHA
    92fedb5 View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2024

  1. Formulated some more definitions and lemmas in context, a bit messy h… 

    …owever.
    @ldiedering
    ldiedering committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    41346b3 View commit details
    Browse the repository at this point in the history

  2. Reduced main theorem to lemmas, modulo some left sorry's

    @ldiedering
    ldiedering committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    2b97390 View commit details
    Browse the repository at this point in the history

  3. Added missing last calc step

    @ldiedering
    ldiedering committed Apr 13, 2024
    Configuration menu
    Copy the full SHA
    a330171 View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2024

  1. State after meeting with recommendations

    @ldiedering
    ldiedering committed Apr 20, 2024
    Configuration menu
    Copy the full SHA
    7b04c67 View commit details
    Browse the repository at this point in the history

  2. Changed back to volume.real in all places; filled in some gaps; minor… 

    … corrections
    @ldiedering
    ldiedering committed Apr 20, 2024
    Configuration menu
    Copy the full SHA
    1e50909 View commit details
    Browse the repository at this point in the history

  3. Proved that δ can be chosen less than π and moved this statement to a… 

    … new lemma
    @ldiedering
    ldiedering committed Apr 20, 2024
    Configuration menu
    Copy the full SHA
    9c7f7aa View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2024

  1. Stated lemma 10.4

    @ldiedering
    ldiedering committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    1a0410b View commit details
    Browse the repository at this point in the history

  2. Incorporated recent updates to definitions and theorem numbering.

    @ldiedering
    ldiedering committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    2659f12 View commit details
    Browse the repository at this point in the history

  3. Created first outline of the proof of Lemma 10.4, i.e. of section 10.7

    @ldiedering
    ldiedering committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    eaf5125 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2024

  1. Worked on section 10.7; problem occured with Finset in ballsCoverBalls

    @ldiedering
    ldiedering committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    69089dd View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2024

  1. Proved lemma 10.37 (Hilbert kernel bound)

    @ldiedering
    ldiedering committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    5f600d4 View commit details
    Browse the repository at this point in the history

Commits on May 1, 2024

  1. Continued work on section 10.7 and moved this part to a separate file.

    @ldiedering
    ldiedering committed May 1, 2024
    Configuration menu
    Copy the full SHA
    0f7d4bc View commit details
    Browse the repository at this point in the history

Commits on May 8, 2024

  1. Correct statement and proof of lemma Hilbert kernel bound.

    @ldiedering
    ldiedering committed May 8, 2024
    Configuration menu
    Copy the full SHA
    1bf2e0a View commit details
    Browse the repository at this point in the history

  2. Minor changes

    @ldiedering
    ldiedering committed May 8, 2024
    Configuration menu
    Copy the full SHA
    960aa77 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2024

  1. Added and proved some lemmas needed for fourierConv_ofTwiceDifferenti… 

    …able
    @ldiedering
    ldiedering committed May 10, 2024
    Configuration menu
    Copy the full SHA
    189d91f View commit details
    Browse the repository at this point in the history

Commits on May 11, 2024

  1. Almost done with the top level approximation argument.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    21104fa View commit details
    Browse the repository at this point in the history

  2. Added and proved lemma about periodicity of deriv.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    9c425d1 View commit details
    Browse the repository at this point in the history

  3. Proved lemma int_sum_nat. Simpler parts of approximation argument done.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    d325494 View commit details
    Browse the repository at this point in the history

  4. Split the main file, part 1.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    9defded View commit details
    Browse the repository at this point in the history

  5. Split main file, part 2.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    f1966c1 View commit details
    Browse the repository at this point in the history

  6. Added basic facts about partialFourierSum.

    @ldiedering
    ldiedering committed May 11, 2024
    Configuration menu
    Copy the full SHA
    120cdf2 View commit details
    Browse the repository at this point in the history

Commits on May 12, 2024

  1. Finished proof of Classical Carleson module Lemma 10.3

    @ldiedering
    ldiedering committed May 12, 2024
    Configuration menu
    Copy the full SHA
    803d7ff View commit details
    Browse the repository at this point in the history

Commits on May 15, 2024

  1. Reshuffling sections

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    94bfd44 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'differentiable_f0_experiment' into proof_of_theorem_1_1

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    5c7bfaf View commit details
    Browse the repository at this point in the history

  3. Proved lemma 10.11 (lower secant bound)

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    4441f37 View commit details
    Browse the repository at this point in the history

  4. Did much of the proof of lemma 10.14 (Hilbert kernel regularity).

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    588d2f5 View commit details
    Browse the repository at this point in the history

  5. Proved Hilbert_kernel_regularity (almost)

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    ea33da6 View commit details
    Browse the repository at this point in the history

  6. Reshuffled and added some definitions

    @ldiedering
    ldiedering committed May 15, 2024
    Configuration menu
    Copy the full SHA
    6b5bcf5 View commit details
    Browse the repository at this point in the history

Commits on May 16, 2024

  1. Various minor improvements

    @ldiedering
    ldiedering committed May 16, 2024
    Configuration menu
    Copy the full SHA
    da62163 View commit details
    Browse the repository at this point in the history

Commits on May 18, 2024

  1. Proved Lemma 10.10 (Dirichlet Kernel)

    @ldiedering
    ldiedering committed May 18, 2024
    Configuration menu
    Copy the full SHA
    a2edd24 View commit details
    Browse the repository at this point in the history

Commits on May 19, 2024

  1. Proved helper lemma for control_approximation_effect

    @ldiedering
    ldiedering committed May 19, 2024
    Configuration menu
    Copy the full SHA
    6f75d5b View commit details
    Browse the repository at this point in the history

Commits on May 20, 2024

  1. Progress on many different parts of control_approximation_effect

    @ldiedering
    ldiedering committed May 20, 2024
    Configuration menu
    Copy the full SHA
    560c025 View commit details
    Browse the repository at this point in the history

  2. Mathlib update and further work on control_approximation_effect

    @ldiedering
    ldiedering committed May 20, 2024
    Configuration menu
    Copy the full SHA
    2a22814 View commit details
    Browse the repository at this point in the history

  3. open Complex in Control_Approximation_Effect

    @ldiedering
    ldiedering committed May 20, 2024
    Configuration menu
    Copy the full SHA
    0c48531 View commit details
    Browse the repository at this point in the history

Commits on May 21, 2024

  1. More sorry's in Control_Approximation_Effect

    @ldiedering
    ldiedering committed May 21, 2024
    Configuration menu
    Copy the full SHA
    332b181 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2024

  1. Cleanup of Carleson_on_the_real_line, part 1

    @ldiedering
    ldiedering committed May 22, 2024
    Configuration menu
    Copy the full SHA
    5a53738 View commit details
    Browse the repository at this point in the history

  2. Cleanup Carleson_on_the_real_line part 2

    @ldiedering
    ldiedering committed May 22, 2024
    Configuration menu
    Copy the full SHA
    82a562c View commit details
    Browse the repository at this point in the history

  3. Cleanup, proved some minor lemmas

    @ldiedering
    ldiedering committed May 22, 2024
    Configuration menu
    Copy the full SHA
    76b5908 View commit details
    Browse the repository at this point in the history

  4. small improvements of control_approximation_effect; no change to ENNR… 

    …eal yet
    @ldiedering
    ldiedering committed May 22, 2024
    Configuration menu
    Copy the full SHA
    ad122ec View commit details
    Browse the repository at this point in the history

Commits on May 23, 2024

  1. Minor exploration of ideas but still stuck.

    @ldiedering
    ldiedering committed May 23, 2024
    Configuration menu
    Copy the full SHA
    23d6860 View commit details
    Browse the repository at this point in the history

  2. Minor additions in Basic

    @ldiedering
    ldiedering committed May 23, 2024
    Configuration menu
    Copy the full SHA
    0c5f550 View commit details
    Browse the repository at this point in the history

  3. Stated van der Corput lemma. Discovered possible 

    issues with defs of IsCancellative and iLipNorm.
    @ldiedering
    ldiedering committed May 23, 2024
    Configuration menu
    Copy the full SHA
    2c096f2 View commit details
    Browse the repository at this point in the history

Commits on May 28, 2024

  1. Added dirichlet_Hilbert_eq lemma

    @ldiedering
    ldiedering committed May 28, 2024
    Configuration menu
    Copy the full SHA
    4c3b00c View commit details
    Browse the repository at this point in the history

  2. le_CarlesonOperatorReal' shoud be mostly working now

    @ldiedering
    ldiedering committed May 28, 2024
    Configuration menu
    Copy the full SHA
    78a6152 View commit details
    Browse the repository at this point in the history

  3. Reorganized proof of control_approximation_effect'

    @ldiedering
    ldiedering committed May 28, 2024
    Configuration menu
    Copy the full SHA
    bbc8b48 View commit details
    Browse the repository at this point in the history

Commits on May 29, 2024

  1. Rewrote proof of control_approximation_effect for ENNReal

    @ldiedering
    ldiedering committed May 29, 2024
    Configuration menu
    Copy the full SHA
    8e81093 View commit details
    Browse the repository at this point in the history

  2. Slightly generalized rcarleson' and other minor changes

    @ldiedering
    ldiedering committed May 29, 2024
    Configuration menu
    Copy the full SHA
    63ad820 View commit details
    Browse the repository at this point in the history

  3. Improved a proof

    @ldiedering
    ldiedering committed May 29, 2024
    Configuration menu
    Copy the full SHA
    0647291 View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2024

  1. Filled in sorry's in Control_Approximation_Effect

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    b6f6bcf View commit details
    Browse the repository at this point in the history

  2. Further cleanup of Control_Approximation_Effect

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    bff22d8 View commit details
    Browse the repository at this point in the history

  3. Updated classical_carleson to current version of control_approximatio… 

    …n_effect
    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    c6641de View commit details
    Browse the repository at this point in the history

  4. Further Cleanup of Control_Approximation_Effect

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    341900c View commit details
    Browse the repository at this point in the history

  5. Control_Approximation_Effect finally sorry-free :)

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    14b987d View commit details
    Browse the repository at this point in the history

  6. Cleanup CarlesonOperatorReal

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    ea60b6e View commit details
    Browse the repository at this point in the history

  7. Merge branch 'control_approximation_effect_ennreal_experiment'

    @ldiedering
    ldiedering committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    3ace239 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2024

  1. Removed arguments for piecewise constant approximation

    @ldiedering
    ldiedering committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    93fac8b View commit details
    Browse the repository at this point in the history

  2. Minor correction in the proof of integer ball cover

    @ldiedering
    ldiedering committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    192cdbb View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2024

  1. Update blueprint section 10, add \leanok's

    @ldiedering
    ldiedering committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    d1e58f1 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/ldiedering/carleson

    @ldiedering
    ldiedering committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    4b8a654 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'development'

    @ldiedering
    ldiedering committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    9eb6008 View commit details
    Browse the repository at this point in the history

  4. Corrected reference of Theorem 1.1

    @ldiedering
    ldiedering committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    c02be26 View commit details
    Browse the repository at this point in the history

Commits on Jun 9, 2024

  1. Try to fix lake-manifest.json and lean-toolchain by reverting to prev… 

    …ious version.
    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    babd40b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'fpvandoorn:master' into main

    @ldiedering
    ldiedering authored Jun 9, 2024
    Configuration menu
    Copy the full SHA
    c6a9006 View commit details
    Browse the repository at this point in the history

  3. Revert "Try to fix lake-manifest.json and lean-toolchain by reverting… 

    … to previous version."

This reverts commit babd40b.
    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    9f19aef View commit details
    Browse the repository at this point in the history

  4. Dowongrade UnicodeBasic and «doc-gen4»

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    92be523 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'main' of https://github.com/ldiedering/carleson

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    0dbdf8f View commit details
    Browse the repository at this point in the history

  6. Revert "Dowongrade UnicodeBasic and «doc-gen4»" 

    This reverts commit 92be523.
    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    590d8df View commit details
    Browse the repository at this point in the history

  7. lake-manifest.json update

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    876bac0 View commit details
    Browse the repository at this point in the history

  8. Has this finally fixed the lake-manifest?

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    e5c0894 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' of https://github.com/ldiedering/carleson

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    864c1f2 View commit details
    Browse the repository at this point in the history

  10. Add fourier-coeff-derivative as dependency of convergence-of-coeffs-s… 

    …ummable
    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    25a6de8 View commit details
    Browse the repository at this point in the history

  11. Fetch lake-manifest.json from upstream

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    39227c1 View commit details
    Browse the repository at this point in the history

  12. Added leanok to smooth-approximation

    @ldiedering
    ldiedering committed Jun 9, 2024
    Configuration menu
    Copy the full SHA
    0f0f038 View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2024

  1. Added leanok to proof of smooth-approximation

    @ldiedering
    ldiedering committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    a0c8c4f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'fpvandoorn:master' into master

    @ldiedering
    ldiedering authored Jun 10, 2024
    Configuration menu
    Copy the full SHA
    5e62c48 View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2024

  1. Merge branch 'fpvandoorn:master' into master

    @ldiedering
    ldiedering authored Jun 17, 2024
    Configuration menu
    Copy the full SHA
    8852b65 View commit details
    Browse the repository at this point in the history

  2. Update estimate-x-shift

    @ldiedering
    ldiedering committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    179d1ba View commit details
    Browse the repository at this point in the history

  3. Further updates in 10.3; to finish it, 10.5 has to be updated first

    @ldiedering
    ldiedering committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    7f3330d View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2024

  1. Started updating Calderon-Zygmund decomposition. Tried using Vitali-c… 

    …overing from mathlib but running into issues with boundedness.
    @ldiedering
    ldiedering committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    3ae8c9b View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2024

  1. Calderon-Zygmund decomposition almost done.

    @ldiedering
    ldiedering committed Jun 22, 2024
    Configuration menu
    Copy the full SHA
    6cfbada View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2024

  1. Mostly finished generalizing/updating subsection Calderon-Zygmund Dec… 

    …omposition
    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    545c6a8 View commit details
    Browse the repository at this point in the history

  2. Reshuffling. Created new chapter for metric space Carleson variant.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    67c9b3a View commit details
    Browse the repository at this point in the history

  3. Completed reorganising of sections. Parts of subsec-cotlar still need… 

    … to be updated.
    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    679bdc3 View commit details
    Browse the repository at this point in the history

  4. Update 10carleson.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    bdeda74 View commit details
    Browse the repository at this point in the history

  5. Finished rewriting and reorganising up to smaller todo's.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    24cbfa4 View commit details
    Browse the repository at this point in the history

  6. Add proof of geometric-series-estimate.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    759e297 View commit details
    Browse the repository at this point in the history

  7. Fixed broken references.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    95a7116 View commit details
    Browse the repository at this point in the history

  8. Updated connections.

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    392547d View commit details
    Browse the repository at this point in the history

  9. Merge branch 'fpvandoorn:master' into master

    @ldiedering
    ldiedering authored Jun 23, 2024
    Configuration menu
    Copy the full SHA
    ecf8d70 View commit details
    Browse the repository at this point in the history

  10. Improved proof in Hilbert_kernel

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    30b18f2 View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' of https://github.com/ldiedering/carleson

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    c7ea74c View commit details
    Browse the repository at this point in the history

  12. Merge branch 'development'

    @ldiedering
    ldiedering committed Jun 23, 2024
    Configuration menu
    Copy the full SHA
    3311915 View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2024

  1. Update to new definitions

    @ldiedering
    ldiedering committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    006f67c View commit details
    Browse the repository at this point in the history

  2. changed TODO's to fixme's

    @ldiedering
    ldiedering committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    4613ce6 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'van_der_corput' into catch-up

    @ldiedering
    ldiedering committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    48abb24 View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2024

  1. Finished van der Corput and most of the part where it is used.

    @ldiedering
    ldiedering committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    1b1cc83 View commit details
    Browse the repository at this point in the history

  2. Proved uniformContinuous_of_continuous; Basic.lean is now sorry-free :)

    @ldiedering
    ldiedering committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    2dc04e0 View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2024

  1. Small corrections

    @ldiedering
    ldiedering committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    193f62d View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2024

  1. Filled in sorry's in Dirichlet_kernel.lean

    @ldiedering
    ldiedering committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    5ab4695 View commit details
    Browse the repository at this point in the history

  2. Filled in more sorry's

    @ldiedering
    ldiedering committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    4a2769f View commit details
    Browse the repository at this point in the history

  3. Added some fixme to blueprint

    @ldiedering
    ldiedering committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    ed5672e View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2024

  1. Finally finished measurability of CarlesonOperatorReal. However, stil… 

    …l some Cleanup required.
    @ldiedering
    ldiedering committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    25a5dc6 View commit details
    Browse the repository at this point in the history

  2. Adjusted Control_Approximation_Effect.lean; no sorry's outside of Car… 

    …leson_on_the_real_line left :)
    @ldiedering
    ldiedering committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    75f84f1 View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2024

  1. Corrections and clarifications in real van der Corput.

    @ldiedering
    ldiedering committed Jul 3, 2024
    Configuration menu
    Copy the full SHA
    e96c6ad View commit details
    Browse the repository at this point in the history

  2. Removed todo in Van_der_Corput.lean

    @ldiedering
    ldiedering committed Jul 3, 2024
    Configuration menu
    Copy the full SHA
    77fa82f View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2024

  1. Updated 10.1 (Proof of Cotlar).

    @ldiedering
    ldiedering committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    720b276 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2024

  1. Filled gaps in 10.2 (Calderon-Zygmund decomposition)

    @ldiedering
    ldiedering committed Jul 6, 2024
    Configuration menu
    Copy the full SHA
    0ed3988 View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2024

  1. Small corrections.

    @ldiedering
    ldiedering committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    0cbe38f View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/fpvandoorn/carleson

    @ldiedering
    ldiedering committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    e0d7f2b View commit details
    Browse the repository at this point in the history

  3. Fixed some problems caused by updated definitions.

    @ldiedering
    ldiedering committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    7c1e9a8 View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2024

  1. Renamed operators and made Dirichlet uppercase everywhere.

    @ldiedering
    ldiedering committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    7ac215c View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2024

  1. Filled in two small sorry's

    @ldiedering
    ldiedering committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    f59311c View commit details
    Browse the repository at this point in the history

  2. Corrections in chapter 10

    @ldiedering
    ldiedering committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    e93f8a4 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. small corrections

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    190fed7 View commit details
    Browse the repository at this point in the history

  2. Added Dirichlet-Hilbert lemma

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    b49292a View commit details
    Browse the repository at this point in the history

  3. .

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    4fd3fab View commit details
    Browse the repository at this point in the history

  4. nothing happened

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    d54b3af View commit details
    Browse the repository at this point in the history

  5. Restructured Section 11.6 (the error bound).

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    6fa58b8 View commit details
    Browse the repository at this point in the history

  6. Added file for spectral projection bound. Should be mostly in mathlib.

    @ldiedering
    ldiedering committed Jul 17, 2024
    Configuration menu
    Copy the full SHA
    2e6e20d View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Started reorganising Control_Approximation_Effect

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    024cad3 View commit details
    Browse the repository at this point in the history

  2. Update control approximation effect

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    d97a1c1 View commit details
    Browse the repository at this point in the history

  3. Renamed files.

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    c2c61a5 View commit details
    Browse the repository at this point in the history

  4. Further reorganising

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    b79b15a View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'upstream/master'

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    67d8a71 View commit details
    Browse the repository at this point in the history

  6. Corrected IsCancellative condition in metricCarleson.

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    87a3da4 View commit details
    Browse the repository at this point in the history

  7. Corrected a \uses reference.

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    f678c10 View commit details
    Browse the repository at this point in the history

  8. Corrected a Lean reference.

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    486b125 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'main' into polishing

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    9e0713a View commit details
    Browse the repository at this point in the history

  10. Cleaned up ControlApproximationEffect

    @ldiedering
    ldiedering committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    8c7a423 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2024

  1. Added more \leanok's and filled in \lean's

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    f0f5c44 View commit details
    Browse the repository at this point in the history

  2. More \leans.

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    92bba8c View commit details
    Browse the repository at this point in the history

  3. More \lean's

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    4f48333 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'upstream/master'

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    279363d View commit details
    Browse the repository at this point in the history

  5. Corrected some problems from merging.

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    6c37717 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'main' into polishing

    @ldiedering
    ldiedering committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    6f4d0c4 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2024

  1. Work on SpectralProjectionBound

    @ldiedering
    ldiedering committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    0915ca6 View commit details
    Browse the repository at this point in the history

  2. Proved spectral_projection_bound

    @ldiedering
    ldiedering committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    245a94a View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2024

  1. Corrected double chapter in blueprint.

    @ldiedering
    ldiedering committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    3347907 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2024

  1. Many small improvements.

    @ldiedering
    ldiedering committed Jul 22, 2024
    Configuration menu
    Copy the full SHA
    8ba6a2d View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. Added measurability proof to the blueprint.

    @ldiedering
    ldiedering committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    8b751bc View commit details
    Browse the repository at this point in the history

  2. Small correction

    @ldiedering
    ldiedering committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    53ee8c5 View commit details
    Browse the repository at this point in the history

  3. Broke up the proof of weak-1-1 into smaller parts.

    @ldiedering
    ldiedering committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    0852b46 View commit details
    Browse the repository at this point in the history

  4. Removed old comment.

    @ldiedering
    ldiedering committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    1a6b5b6 View commit details
    Browse the repository at this point in the history

  5. Correction in chapter 11.

    @ldiedering
    ldiedering committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    b197f86 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2024

  1. Removed old comment

    @ldiedering
    ldiedering committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    71e62f4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'fpvandoorn:master' into master

    @ldiedering
    ldiedering authored Jul 25, 2024
    Configuration menu
    Copy the full SHA
    1b4d87d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'polishing'

    @ldiedering
    ldiedering committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    94685e9 View commit details
    Browse the repository at this point in the history

  4. Indentation

    @ldiedering
    ldiedering committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    ec8f073 View commit details
    Browse the repository at this point in the history

  5. Fixed wrong \lean

    @ldiedering
    ldiedering committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    7116fa3 View commit details
    Browse the repository at this point in the history