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 581 to 600 of 781 declarations.
lemma
ENNReal.toReal_Iio_eq_Ico
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:286
lemma
ENNReal.toReal_Icc_eq_Icc
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:315
lemma
ENNReal.toReal_Ioo_eq_Ioo
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:332
lemma
ENNReal.toReal_Ioi_eq_Ioi
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:364
lemma
ENNReal.ofReal_Ioo_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:384
lemma
ENNReal.ofReal_Iio_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:413
lemma
ENNReal.toNNReal_Iio
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:432
lemma
ENNReal.volume_map_add_left_le_self
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:531
lemma
setLIntegral_nnreal_Ici
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:643
lemma
lintegral_nnreal_scale_constant'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:659
lemma
Set.exists_le_in_minLayer_of_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MinLayer · Carleson/ToMathlib/MinLayer.lean:94
lemma
Set.subtype_mk_minimal_iff
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MinLayer · Carleson/ToMathlib/MinLayer.lean:121
lemma
Set.minLayer_eq_setOf_height
A.minLayer n comprises exactly A's elements of height n.
Carleson.ToMathlib.MinLayer · Carleson/ToMathlib/MinLayer.lean:133
lemma
Set.iUnion_lt_minLayer_iff_bounded_series
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MinLayer · Carleson/ToMathlib/MinLayer.lean:158
lemma
Set.exists_le_in_layersAbove_of_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MinLayer · Carleson/ToMathlib/MinLayer.lean:191
lemma
ENNReal.sum_geometric_two_pow_toNNReal
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:59
lemma
MeasureTheory.lintegral_Ioc_partition
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:163
lemma
MeasureTheory.eLpNorm_two_eq_enorm_integral_mul_conj
One of the very few cases where a norm can be moved out of an integral.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:319
theorem
MeasureTheory.setIntegral_biUnion_le_sum_setIntegral
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:647
theorem
ENNReal.lintegral_Lp_smul
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:704
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.