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 181 to 200 of 781 declarations.
lemma
ordConnected_C4
Lemma 5.3.9
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:95
lemma
ordConnected_C5
Lemma 5.3.10
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:111
lemma
URel.not_disjoint
Lemma 5.4.1, part 2.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:151
lemma
URel.eq
Lemma 5.4.1, part 1.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:196
lemma
urel_of_not_disjoint
Helper for 5.4.2 that is also used in 5.4.9.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:208
lemma
equivalenceOn_urel
Lemma 5.4.2.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:235
lemma
C6_forest
Lemma 5.4.3
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:295
lemma
forest_disjoint
This one could deserve a lemma in the blueprint, as it is needed to decompose the sum of Carleson operators over disjoint subfamilies.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:313
lemma
forest_geometry
Lemma 5.4.4, verifying (2.0.32)
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:330
lemma
forest_convex
Lemma 5.4.5, verifying (2.0.33)
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:356
lemma
forest_separation
Lemma 5.4.6, verifying (2.0.36)
Note: swapped u and u' to match (2.0.36)
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:374
lemma
forest_inner
Lemma 5.4.7, verifying (2.0.37)
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:433
lemma
exists_smul_le_of_𝔘₃
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:487
lemma
mf_injOn
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:500
lemma
stackSize_𝔘₃_le_𝔐
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:524
lemma
forest_stacking
Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:538
lemma
iUnion_𝔘₄
The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n j.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:588
lemma
pairwiseDisjoint_𝔘₄
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:622
lemma
stackSize_𝔘₄_le
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:635
lemma
carlesonSum_𝔓₁_eq_sum
From the fact that the ℭ₅ k n j are disjoint, one can rewrite the whole Carleson sum over
𝔓₁ (the union of the ℭ₅ k n j) as a sum of Carleson sums over the ℭ₅ k n j.
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:692
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.