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 701 to 720 of 781 declarations.
lemma
MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:556
lemma
MeasureTheory.distribution_comp_eq_distribution_comp_rearrangement
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:573
lemma
MeasureTheory.lintegral_comp_rearrangement'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:602
lemma
MeasureTheory.sSup_rearrangement
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:732
lemma
MeasureTheory.setLIntegral_enorm_le_lintegral_rearrangement
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:815
lemma
MeasureTheory.setLIntegral_enorm_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:829
lemma
MeasureTheory.lintegral_rearrangement_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:874
lemma
MeasureTheory.Antitone.lintegral_withDensity_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:994
lemma
ContinuousWithinAt.measure_lt_ne_zero
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Topology.ContinuousOn · Carleson/ToMathlib/Topology/ContinuousOn.lean:21
lemma
eLpNormEssSup_nnreal_eq_iSup_nnreal
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Topology.ContinuousOn · Carleson/ToMathlib/Topology/ContinuousOn.lean:62
theorem
MeasureTheory.wnorm'_eq_iSup_rpow_mul_rearrangement
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:56
theorem
MeasureTheory.wnorm_indicator_const
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:192
lemma
MeasureTheory.wnorm_iSup_of_monotone
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:267
theorem
MeasureTheory.MemWLp.ae_ne_top
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:301
lemma
MeasureTheory.distribution_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:352
lemma
MeasureTheory.wnorm'_le_eLpNorm'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:365
lemma
MeasureTheory.distribution_lt_top
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:379
lemma
MeasureTheory.aestronglyMeasurable_ennreal_toReal_iff
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:470
lemma
MeasureTheory.hasWeakType_toReal_iff
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:485
lemma
MeasureTheory.hasWeakType_iSup_of_monotone
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:496
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.