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 361 to 380 of 781 declarations.
lemma
continuous_carlesonOperatorIntegrand
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:454
lemma
enorm_carlesonOperatorIntegrand_le
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:474
theorem
carlesonOperatorIntegrand_measurable
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:491
theorem
linearizedCarlesonOperator_measurable
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:514
theorem
enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:583
theorem
linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:605
lemma
tendsto_carlesonOperatorIntegrand_of_dominated_convergence
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:629
lemma
linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:662
lemma
monotone_lcoConvergent
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Linearized · Carleson/MetricCarleson/Linearized.lean:22
lemma
iSup_lcoConvergent
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Linearized · Carleson/MetricCarleson/Linearized.lean:35
lemma
measurable_lcoConvergent
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Linearized · Carleson/MetricCarleson/Linearized.lean:71
theorem
linearized_metric_carleson
Theorem 1.1.2
Carleson.MetricCarleson.Linearized · Carleson/MetricCarleson/Linearized.lean:109
lemma
carlesonOperator_eq_biSup_Θ'_J102
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:25
lemma
biSup_Θ'_eq_biSup_enumΘ'
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:83
lemma
enumΘ'ArgMax_eq_iff
The characterising property of enumΘ'ArgMax.
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:110
lemma
lowerSemicontinuous_LNT
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:159
lemma
BST_LNT_of_BST_NT
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:170
theorem
metric_carleson
Theorem 1.1.1
Carleson.MetricCarleson.Main · Carleson/MetricCarleson/Main.lean:203
lemma
measurable_T_lin
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:34
theorem
finitary_carleson_step
Open the record for the exact Lean statement and complete source.
Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:81
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.