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 321 to 340 of 781 declarations.
lemma
TileStructure.Forest.density_tree_bound2
Second part of Lemma 7.3.1.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:475
lemma
smul_le_indicator
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:522
lemma
TileStructure.Forest.union_𝓙₆
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:31
lemma
TileStructure.Forest.thin_scale_impact_prelims
Some preliminary relations for Lemma 7.6.3.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:99
lemma
TileStructure.Forest.thin_scale_impact_key
The key relation of Lemma 7.6.3, which will eventually be shown to lead to a contradiction.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:133
lemma
TileStructure.Forest.thin_scale_impact
Lemma 7.6.3.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:191
lemma
TileStructure.Forest.square_function_count
Lemma 7.6.4.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:241
lemma
TileStructure.Forest.sum_𝓙₆_indicator_sq_eq
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:369
lemma
TileStructure.Forest.btp_expansion
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:385
lemma
TileStructure.Forest.e763
Equation (7.6.3) of Lemma 7.6.2.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:426
lemma
TileStructure.Forest.btp_integral_bound
The critical bound on the integral in Equation (7.6.3). It holds for any cubes I, J.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:502
lemma
TileStructure.Forest.e764_preCS
Equation (7.6.4) of Lemma 7.6.2 (before applying Cauchy–Schwarz).
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:563
lemma
TileStructure.Forest.e764_postCS
Equation (7.6.4) of Lemma 7.6.2 (after applying Cauchy–Schwarz and simplification).
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:627
lemma
TileStructure.Forest.btp_constant_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:702
lemma
TileStructure.Forest.cntp_approxOnCube_eq
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:774
lemma
TileStructure.Forest.correlation_near_tree_parts
Lemma 7.4.6
Carleson.ForestOperator.RemainingTiles · Carleson/ForestOperator/RemainingTiles.lean:819
lemma
Grid.isMin_iff
Open the record for the exact Lean statement and complete source.
Carleson.GridStructure · Carleson/GridStructure.lean:213
lemma
Grid.exists_unique_succ
There exists a unique successor of each non-maximal cube.
Carleson.GridStructure · Carleson/GridStructure.lean:235
lemma
Grid.exists_supercube
Open the record for the exact Lean statement and complete source.
Carleson.GridStructure · Carleson/GridStructure.lean:295
lemma
Grid.dist_strictMono
Stronger version of Lemma 2.1.2.
Carleson.GridStructure · Carleson/GridStructure.lean:397
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.