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 261 to 280 of 781 declarations.
lemma
TileStructure.Forest.le_C7_2_2
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:335
lemma
TileStructure.Forest.nontangential_operator_bound
Lemma 7.2.2.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:358
lemma
TileStructure.Forest.subset_of_kissing
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:400
lemma
TileStructure.Forest.volume_le_of_kissing
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:417
lemma
TileStructure.Forest.boundary_overlap
Lemma 7.2.4.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:447
lemma
TileStructure.Forest.e728_push_toReal
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:463
lemma
TileStructure.Forest.e728
Equation (7.2.8) in the proof of Lemma 7.2.3.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:531
lemma
TileStructure.Forest.boundary_operator_bound
Lemma 7.2.3.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:734
lemma
TileStructure.Forest.tree_projection_estimate
Lemma 7.2.1.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:874
lemma
TileStructure.Forest.union_𝓙₅
Part of Lemma 7.5.1.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:129
lemma
TileStructure.Forest.moderate_scale_change
Lemma 7.5.3 (stated somewhat differently).
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:206
lemma
TileStructure.Forest.sum_χ
Part of Lemma 7.5.2.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:237
lemma
TileStructure.Forest.boundedCompactSupport_toReal_χ
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:266
lemma
TileStructure.Forest.quarter_add_two_mul_D_mul_card_le
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:289
lemma
TileStructure.Forest.dist_χ_le
Part of Lemma 7.5.2.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:384
lemma
TileStructure.Forest.ψ_le_max
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:482
lemma
TileStructure.Forest.le_of_mem_E
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:494
lemma
TileStructure.Forest.enorm_ψ_le_edist
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:513
lemma
TileStructure.Forest.integrable_adjointCarleson_interior
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:575
lemma
TileStructure.Forest.QQQQ_bound_real
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:668
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.