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 621 to 640 of 781 declarations.
lemma
ComputationsChoiceExponent.ζ_eq_top_top
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:699
lemma
ComputationsChoiceExponent.ζ_pos_iff_aux₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:770
lemma
ComputationsChoiceExponent.ζ_neg_iff_aux₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:824
lemma
ComputationsChoiceExponent.ζ_ne_zero
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:918
lemma
ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:931
lemma
ComputationsChoiceExponent.eq_exponents₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:957
lemma
ComputationsChoiceExponent.eq_exponents₂
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:984
lemma
ComputationsChoiceExponent.eq_exponents₁
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:1012
lemma
ComputationsChoiceExponent.eq_exponents₃
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:1033
lemma
ComputationsChoiceExponent.eq_exponents₇
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.InterpolatedExponents · Carleson/ToMathlib/RealInterpolation/InterpolatedExponents.lean:1075
lemma
MeasureTheory.AESubadditiveOn.biSup
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:141
lemma
MeasureTheory.AESublinearOn.biSup
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:263
lemma
MeasureTheory.AESublinearOn.biSup2
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:284
lemma
MeasureTheory.AESublinearOn.toReal
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:339
lemma
MeasureTheory.rewrite_norm_func
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:394
lemma
MeasureTheory.estimate_norm_rpow_range_operator
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:424
lemma
MeasureTheory.estimate_norm_rpow_range_operator'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:448
lemma
MeasureTheory.simplify_factor₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:515
lemma
MeasureTheory.simplify_factor₁
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:570
lemma
MeasureTheory.support_sigma_finite_from_MemLp
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:678
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.