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 141 to 160 of 781 declarations.
lemma
dyadic_union
Lemma 5.2.4
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:182
lemma
john_nirenberg_aux1
Equation (5.2.7) in the proof of Lemma 5.2.5.
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:202
lemma
john_nirenberg_aux2
Equation (5.2.11) in the proof of Lemma 5.2.5.
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:261
lemma
john_nirenberg
Lemma 5.2.5
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:312
lemma
layervol_eq_zero_of_lt
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:405
lemma
lintegral_Ioc_layervol_le
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:432
lemma
top_tiles
Lemma 5.2.7
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:477
lemma
tree_count
Lemma 5.2.8
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:660
lemma
boundary_exception
Lemma 5.2.9
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:682
lemma
third_exception
Lemma 5.2.10
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:869
lemma
exists_mem_aux𝓒
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:26
lemma
exists_k_of_mem_𝔓pos
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:47
lemma
dens'_le_of_mem_𝔓pos
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:65
lemma
exists_E₂_volume_pos_of_mem_𝔓pos
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:83
lemma
dens'_pos_of_mem_𝔓pos
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:93
lemma
exists_k_n_of_mem_𝔓pos
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:103
lemma
exists_j_of_mem_𝔓pos_ℭ
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:147
lemma
mem_iUnion_iff_mem_of_mem_ℭ
Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.1.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:198
lemma
notMem_ℭ₅_iff_mem_𝔏₃
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:218
lemma
antichain_decomposition
Lemma 5.5.1.
We will not use the lemma in this form, as to decompose the Carleson sum it is also crucial that the union is disjoint. This is easier to formalize by decomposing into successive terms, taking advantage of disjointess at each step, instead of doing everything in one go. Still, we keep this lemma as it corresponds to the blueprint, and the key steps of its proof will also be the key steps when doing the successive decompositions.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:250
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.