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 301 to 320 of 781 declarations.
lemma
TileStructure.Forest.cdtp_le_iHolENorm
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:1952
lemma
TileStructure.Forest.correlation_distant_tree_parts
Lemma 7.4.5
Carleson.ForestOperator.LargeSeparation · Carleson/ForestOperator/LargeSeparation.lean:2012
lemma
TileStructure.Forest.S_eq_zero_of_topCube_mem_𝓙₀
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:66
lemma
TileStructure.Forest.approxOnCube_apply
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:129
lemma
TileStructure.Forest.lintegral_eq_lintegral_approxOnCube
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:158
lemma
TileStructure.Forest.laverage_le_biInf_MB'
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:285
lemma
TileStructure.Forest.convex_scales
Lemma 7.1.1, freely translated.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:301
lemma
TileStructure.Forest.biUnion_𝓙
Part of Lemma 7.1.2
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:320
lemma
TileStructure.Forest.biUnion_𝓛
Part of Lemma 7.1.2
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:333
lemma
TileStructure.Forest.first_tree_pointwise
Lemma 7.1.4
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:601
lemma
TileStructure.Forest.second_tree_pointwise
Lemma 7.1.5
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:669
lemma
TileStructure.Forest.sum_p_eq_sum_I_sum_p
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:924
lemma
TileStructure.Forest.le_C7_1_6
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:950
lemma
TileStructure.Forest.third_tree_pointwise
Lemma 7.1.6
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:970
lemma
TileStructure.Forest.pointwise_tree_estimate
Lemma 7.1.3.
Carleson.ForestOperator.PointwiseEstimate · Carleson/ForestOperator/PointwiseEstimate.lean:1088
lemma
TileStructure.Forest.local_dens1_tree_bound_exists
Part 1 of Lemma 7.3.2.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:28
lemma
TileStructure.Forest.volume_bound_of_Grid_lt
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:66
lemma
TileStructure.Forest.local_dens1_tree_bound
Lemma 7.3.2.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:89
lemma
TileStructure.Forest.local_dens2_tree_bound
Lemma 7.3.3.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:215
lemma
TileStructure.Forest.density_tree_bound1
First part of Lemma 7.3.1.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:460
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.