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 521 to 540 of 781 declarations.
lemma
MeasureTheory.eLorentzNorm_eq_eLpNorm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:153
lemma
MeasureTheory.eLorentzNorm'_eq_wnorm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:199
lemma
MeasureTheory.eLorentzNorm'_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:227
lemma
MeasureTheory.eLorentzNorm'_eq'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:359
lemma
MeasureTheory.eLorentzNorm'_indicator_const
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:394
lemma
MeasureTheory.eLorentzNorm'_indicator_const'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:415
lemma
MeasureTheory.eLorentzNorm_indicator_const
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:486
lemma
MeasureTheory.MemLorentz_of_MemLorentz_ge
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Basic.lean:523
lemma
MeasureTheory.eLorentzNorm'_eq_integral_distribution_rpow
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.Defs · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/Defs.lean:42
theorem
MeasureTheory.eLorentzNorm_add_le''
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:32
lemma
MeasureTheory.eLpNorm_lorentz_helper
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:96
theorem
MeasureTheory.antitone_rpow_inv_sub_inv
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:148
lemma
MeasureTheory.eLorentzNorm'_eq_lintegral_lorentz_helper_mul
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:183
theorem
MeasureTheory.eLorentzNorm_add_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:225
theorem
MeasureTheory.eLorentzNorm_add_le_of_disjoint_support
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:333
lemma
MeasureTheory.eLpNormEssSup_nnreal_scale_constant'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LpNorm.Misc · Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean:34
lemma
MeasureTheory.eLpNorm_withDensity_scale_constant'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LpNorm.Misc · Carleson/ToMathlib/MeasureTheory/Function/LpNorm/Misc.lean:46
theorem
MeasureTheory.eLpNormEssSup_iSup
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean:69
theorem
MeasureTheory.eLpNorm_iSup'
Monotone convergence applied to eLpNorms. AEMeasurable variant.
Possibly imperfect hypotheses, particularly on p. Note that for p = ∞ the stronger
statement in eLpNormEssSup_iSup holds.
Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.Basic · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/Basic.lean:101
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.CompareExp · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean:31
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.