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 241 to 260 of 781 declarations.
lemma
TileStructure.Forest.adjointCarlesonRowSum_adjoint
adjointCarlesonRowSum is the adjoint of carlesonRowSum.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:359
lemma
TileStructure.Forest.row_bound_common
Common proof structure for the two parts of Lemma 7.7.2.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:377
lemma
TileStructure.Forest.le_C7_7_2_1
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:428
lemma
TileStructure.Forest.le_C7_7_2_2
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:453
lemma
TileStructure.Forest.row_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:472
lemma
TileStructure.Forest.indicator_row_bound
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:491
lemma
TileStructure.Forest.row_correlation
Lemma 7.7.3.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:564
lemma
TileStructure.Forest.disjoint_of_ne_of_mem
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:640
lemma
TileStructure.Forest.forest_operator_g_prelude
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:688
lemma
TileStructure.Forest.le_sq_G2_0_4
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:726
lemma
TileStructure.Forest.forest_operator_g_main
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:758
lemma
TileStructure.Forest.forest_operator_g
The g side of Proposition 2.0.4.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:829
lemma
TileStructure.Forest.forest_operator_f_prelude
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:851
lemma
TileStructure.Forest.forest_operator_f_inner
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:876
lemma
TileStructure.Forest.forest_operator_f_main
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:921
lemma
TileStructure.Forest.forest_operator_f
The f side of Proposition 2.0.4.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:990
theorem
forest_operator
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:1017
theorem
forest_operator'
Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:1068
theorem
forest_operator_le_volume
Version of the forest operator theorem, but controlling the integral of the norm instead of
the integral of the function multiplied by another function, and with the upper bound in terms
of volume F and volume G.
Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:1110
lemma
integrableOn_K_mul_f
Open the record for the exact Lean statement and complete source.
Carleson.ForestOperator.L2Estimate · Carleson/ForestOperator/L2Estimate.lean:17
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.