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 161 to 180 of 781 declarations.
lemma
ceil_log2_le_floor_four_add_log2
Logarithmic inequality used in the proof of Lemma 5.5.2.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:293
lemma
card_𝔒
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:323
lemma
l_upper_bound
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:391
lemma
exists_𝔒_with_le_quotient
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:405
lemma
iUnion_L0'
Main part of Lemma 5.5.2.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:445
lemma
antichain_L2
Lemma 5.5.3
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:541
lemma
carlesonSum_𝔓₁_compl_eq_𝔓pos_inter
The Carleson sum over 𝔓₁ᶜ and 𝔓pos ∩ 𝔓₁ᶜ coincide at ae every point of G \ G'.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:605
lemma
carlesonSum_𝔓pos_eq_sum
The Carleson sum over 𝔓pos ∩ 𝔓₁ᶜ can be decomposed as a sum over the intersections of this
set with various ℭ k n.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:628
lemma
carlesonSum_𝔓pos_inter_ℭ_eq_add_sum
In each set ℭ k n, the Carleson sum can be decomposed as a sum over 𝔏₀ k n and over
various ℭ₁ k n j.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:650
lemma
carlesonSum_𝔓pos_inter_𝔏₀_eq_sum
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:677
lemma
carlesonSum_𝔓pos_inter_ℭ₁_eq_add_sum
In each set ℭ₁ k n j, the Carleson sum can be decomposed as a sum over ℭ₂ k n j and over
various 𝔏₁ k n j l.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:693
lemma
carlesonSum_𝔓pos_inter_ℭ₂_eq_add_sum
In each set ℭ₂ k n j, the Carleson sum can be decomposed as a sum over 𝔏₂ k n j and over
various 𝔏₃ k n j l.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:722
lemma
lintegral_enorm_carlesonSum_le_of_isAntichain_subset_ℭ
Custom version of the antichain operator theorem, in the specific form we need to handle the various terms in the previous statement.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:856
lemma
lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:947
lemma
lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:1034
lemma
C5_1_3_optimized_le_C5_1_3
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:1084
lemma
ordConnected_C
Lemma 5.3.5
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:36
lemma
ordConnected_C1
Lemma 5.3.6
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:48
lemma
ordConnected_C2
Lemma 5.3.7
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:68
lemma
ordConnected_C3
Lemma 5.3.8
Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:84
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.