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 221 to 240 of 781 declarations.
lemma
exists_Grid
Open the record for the exact Lean statement and complete source.
Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:56
theorem
tile_sum_operator
Lemma 4.0.3
Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:70
theorem
finitary_carleson
Proposition 2.0.1
Carleson.FinitaryCarleson · Carleson/FinitaryCarleson.lean:110
lemma
TileStructure.Forest.adjoint_tile_support1
Part 1 of Lemma 7.4.1. Todo: update blueprint with precise properties needed on the function.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:35
lemma
TileStructure.Forest.adjoint_tile_support2_sum
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:63
lemma
TileStructure.Forest.enorm_adjointCarleson_le
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:82
lemma
TileStructure.Forest.enorm_adjointCarleson_le_mul_indicator
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:106
lemma
TileStructure.Forest.adjoint_tree_estimate
Part 1 of Lemma 7.4.2.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:132
lemma
TileStructure.Forest.indicator_adjoint_tree_estimate
Part 2 of Lemma 7.4.2.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:154
lemma
TileStructure.Forest.le_C7_4_3
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:177
lemma
TileStructure.Forest.adjoint_tree_control
Lemma 7.4.3.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:214
lemma
TileStructure.Forest.overlap_implies_distance
Part 1 of Lemma 7.4.7.
Carleson.ForestOperator.AlmostOrthogonality · Carleson/ForestOperator/AlmostOrthogonality.lean:243
lemma
TileStructure.Forest.estimate_C7_4_5
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:27
lemma
TileStructure.Forest.estimate_C7_4_6
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:43
lemma
TileStructure.Forest.correlation_separated_trees_of_subset
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:92
lemma
TileStructure.Forest.correlation_separated_trees
Lemma 7.4.4
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:135
lemma
TileStructure.Forest.rowDecomp_zornset_chain_Union_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:167
lemma
TileStructure.Forest.stackSize_remainder_ge_one_of_exists
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:237
lemma
TileStructure.Forest.remainder_stackSize_le
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:254
lemma
TileStructure.Forest.pairwiseDisjoint_rowDecomp
Part of Lemma 7.7.1
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:329
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.