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 641 to 660 of 781 declarations.
lemma
MeasureTheory.combine_estimates₀
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:710
lemma
MeasureTheory.combine_estimates₁
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:857
lemma
MeasureTheory.simplify_factor_aux₄
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:908
lemma
MeasureTheory.exists_hasStrongType_real_interpolation_aux₀
The trivial case for the estimate in the real interpolation theorem
when the L^p norm of f vanishes.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:969
lemma
MeasureTheory.exists_hasStrongType_real_interpolation_aux₁
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1020
lemma
MeasureTheory.exists_hasStrongType_real_interpolation_aux₂
The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots,
for the case q₀ < q₁.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1099
lemma
MeasureTheory.exists_hasStrongType_real_interpolation_aux₃
The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁,
before taking roots.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1228
lemma
MeasureTheory.exists_hasStrongType_real_interpolation_aux₄
The main estimate for the real interpolation theorem, before taking roots, combining
the cases p₀ ≠ p₁ and p₀ = p₁.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1254
lemma
MeasureTheory.C_realInterpolation_ENNReal_ne_top
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1312
lemma
MeasureTheory.C_realInterpolation_ENNReal_pos
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1339
lemma
MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1394
theorem
MeasureTheory.exists_hasStrongType_real_interpolation
Marcinkiewicz real interpolation theorem
Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1436
lemma
MeasureTheory.truncCut_sup
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:56
lemma
MeasureTheory.representationLp
Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:84
lemma
MeasureTheory.lintegral_lintegral_pow_swap
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:271
lemma
MeasureTheory.AEStronglyMeasurable.trunc_ton_norm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:357
lemma
MeasureTheory.AEStronglyMeasurable.trunc_ton
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:372
lemma
MeasureTheory.AEStronglyMeasurable.truncCompl_ton
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:386
lemma
MeasureTheory.AEStronglyMeasurable.truncCompl_ton_norm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:400
lemma
MeasureTheory.restrict_to_support_trnc
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:440
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.