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 601 to 620 of 781 declarations.
lemma
Finset.prod_finset_product_filter_right
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:734
lemma
Finset.sum_range_mul_conj_sum_range
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:747
lemma
Finset.pow_sum_comm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:760
lemma
MeasureTheory.sum_sq_eLpNorm_indicator_le_of_pairwiseDisjoint
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Misc · Carleson/ToMathlib/Misc.lean:774
theorem
ciSup_eq_ciSup
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Order.ConditionallyCompleteLattice.Basic · Carleson/ToMathlib/Order/ConditionallyCompleteLattice/Basic.lean:18
lemma
ENNReal.rpow_add_of_pos
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:132
lemma
ENNReal.rpow_le_rpow_of_exponent_le_base_le
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:201
lemma
ENNReal.rpow_le_rpow_of_exponent_le_base_ge
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:229
lemma
ENNReal.rpow_le_rpow_of_exponent_le_base_ge_enorm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:247
lemma
ComputationsInterpolatedExponents.interp_exp_between
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:310
lemma
ComputationsInterpolatedExponents.preservation_positivity_inv_toReal
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:409
lemma
ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:437
lemma
ComputationsInterpolatedExponents.exp_lt_iff
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:479
lemma
ComputationsInterpolatedExponents.exp_gt_iff
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:488
lemma
ComputationsChoiceExponent.ζ_equality₂
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:556
lemma
ComputationsChoiceExponent.ζ_equality₃
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:580
lemma
ComputationsChoiceExponent.ζ_equality₄
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:611
lemma
ComputationsChoiceExponent.ζ_equality₅
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:624
lemma
ComputationsChoiceExponent.ζ_equality₇
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:654
lemma
ComputationsChoiceExponent.ζ_equality₈
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:687
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.