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 281 to 300 of 781 declarations.
lemma
TileStructure.Forest.QQQQ_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:749
lemma
TileStructure.Forest.holder_correlation_tile_two
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:765
lemma
TileStructure.Forest.holder_correlation_tile
Lemma 7.5.5.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:838
lemma
TileStructure.Forest.limited_scale_impact_first_estimate
Part of Lemma 7.5.6.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:857
lemma
TileStructure.Forest.limited_scale_impact_second_estimate
Part of Lemma 7.5.6.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:909
lemma
TileStructure.Forest.local_tree_control
Lemma 7.5.7.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1078
lemma
TileStructure.Forest.scales_impacting_interval
Lemma 7.5.8.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1150
lemma
TileStructure.Forest.volume_cpDsp_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1181
lemma
TileStructure.Forest.gtc_integral_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1197
lemma
TileStructure.Forest.global_tree_control1_edist_part1
Part 1 of equation (7.5.18) of Lemma 7.5.9.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1228
lemma
TileStructure.Forest.gtc_sum_Icc_le_two
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1301
lemma
TileStructure.Forest.global_tree_control1_edist_part2
Part 2 of equation (7.5.18) of Lemma 7.5.9.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1329
lemma
TileStructure.Forest.global_tree_control1_supbound
Equation (7.5.17) of Lemma 7.5.9.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1407
lemma
TileStructure.Forest.P7_5_4_le_adjointBoundaryOperator_mul
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1525
lemma
TileStructure.Forest.enorm_holderFunction_le
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1548
lemma
TileStructure.Forest.holder_correlation_tree_1
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1576
lemma
TileStructure.Forest.edist_holderFunction_le
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1698
lemma
TileStructure.Forest.le_C7_5_4
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1763
lemma
TileStructure.Forest.holder_correlation_tree
Lemma 7.5.4.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1783
lemma
TileStructure.Forest.lower_oscillation_bound
Lemma 7.5.11
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1867
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.