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 381 to 400 of 781 declarations.
lemma
exists_volume_slice_lt_eps
The sets G_n become arbitrarily small.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:147
lemma
slice_integral_bound_sum
The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:172
lemma
sum_le_four_div_q_sub_one
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:192
lemma
linearized_truncation
Lemma 3.0.4.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:223
lemma
S_truncation
Lemma 3.0.3. B is the blueprint's S.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:261
lemma
R₁_le_D_zpow_div_four
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:376
lemma
D_zpow_div_two_le_R₂
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:391
lemma
exists_uniform_annulus_bound
There exists a uniform bound for all possible values of L302 and U302 over the annulus in
R_truncation.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:422
lemma
enorm_setIntegral_annulus_le
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:445
lemma
enorm_carlesonOperatorIntegrand_le_T_S
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:487
lemma
lintegral_globalMaximalFunction_le
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:541
lemma
le_C1_0_2
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:576
lemma
R_truncation'
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:603
lemma
R_truncation
Lemma 3.0.2.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:662
lemma
exists_scale_add_le_of_mem_minLayer
Open the record for the exact Lean statement and complete source.
Carleson.MinLayerTiles · Carleson/MinLayerTiles.lean:16
lemma
exists_le_add_scale_of_mem_maxLayer
Open the record for the exact Lean statement and complete source.
Carleson.MinLayerTiles · Carleson/MinLayerTiles.lean:28
theorem
MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn
Open the record for the exact Lean statement and complete source.
Carleson.Operators · Carleson/Operators.lean:93
theorem
MeasureTheory.BoundedCompactSupport.carlesonOn
Open the record for the exact Lean statement and complete source.
Carleson.Operators · Carleson/Operators.lean:144
lemma
carlesonSum_inter_add_inter_compl
Open the record for the exact Lean statement and complete source.
Carleson.Operators · Carleson/Operators.lean:170
lemma
sum_carlesonSum_of_pairwiseDisjoint
Open the record for the exact Lean statement and complete source.
Carleson.Operators · Carleson/Operators.lean:180
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.