Head version
74ef907d6bdb
74ef907d6bdb60797b88655bc16e3032fb835fdc
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 23 Jul 2026
- Dependencies
- 10
- Versions
- 38
All packages
fpvandoorn/carleson
carleson
A formalized proof of Carleson's theorem in Lean
Therefore indexed 781 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
External build observation
Exact head commit and toolchain
No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.
Pin this source in lakefile.lean
require carleson from git "https://github.com/fpvandoorn/carleson.git" @ "74ef907d6bdb60797b88655bc16e3032fb835fdc"
Source declarations
781 indexed proofs
Showing 201 to 220 of 781 declarations.
lemma
carlesonSum_ℭ₅_eq_ℭ₆
The Carleson sum over ℭ₅ and ℭ₆ coincide, for points in G \ G'.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:714
lemma
carlesonSum_ℭ₆_eq_sum
The Carleson sum over ℭ₆ can be decomposed as a sum over 4 n + 12 forests
based on 𝔘₄ k n j l.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:734
lemma
lintegral_carlesonSum_forest
For each forest, the integral of the norm of the Carleson sum can be controlled thanks to
the forest theorem and to the density control coming from the fact we are away from G₁.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:752
lemma
lintegral_carlesonSum_forest'
For each forest, the integral of the norm of the Carleson sum can be controlled thanks to
the forest theorem and to the density control coming from the fact we are away from G₁. Second
version, with the volume of F.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:796
lemma
forest_union_sum_aux1
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:882
lemma
forest_union_sum_aux2
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:930
lemma
forest_union_optimized
Version of the forest union result with a better constant.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:971
lemma
C5_1_2_optimized_le'
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:999
lemma
le_C2_0_2
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.MainTheorem · Carleson/Discrete/MainTheorem.lean:21
theorem
discrete_carleson
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.MainTheorem · Carleson/Discrete/MainTheorem.lean:44
lemma
le_localOscillation
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:211
lemma
enorm_integral_exp_le
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:242
lemma
isCancellative_of_norm_integral_exp_le
Constructor of IsCancellative in terms of real norms instead of extended reals.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:262
lemma
enorm_K_sub_le
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:443
lemma
integrableOn_K_mul
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:459
lemma
integrableOn_K_Icc
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:472
lemma
le_cdist_iterate
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:494
lemma
cdist_le_iterate
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:507
lemma
cdist_le_mul_cdist
Open the record for the exact Lean statement and complete source.
Carleson.DoublingMeasure · Carleson/DoublingMeasure.lean:519
theorem
integrable_tile_sum_operator
Open the record for the exact Lean statement and complete source.
Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:16
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.