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 541 to 560 of 781 declarations.
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_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:73
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
Carleson.ToMathlib.MeasureTheory.Function.LpSeminorm.CompareExp · Carleson/ToMathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean:97
lemma
MeasureTheory.SimpleFunc.Antitone.support_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc · Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean:218
theorem
MeasureTheory.SimpleFunc.iSup_approx_apply'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc · Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean:434
lemma
MeasureTheory.SimpleFunc.iSup_nnapprox_apply
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc · Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean:490
lemma
MeasureTheory.Antitone.antitone_eapprox
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc · Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean:549
lemma
enorm_integral_norm_eq_integral_enorm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap · Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean:26
theorem
Function.Periodic.setIntegral_Ioc_add_eq
If f is a periodic function with period T, then its integral over [t, t + T] does not
depend on t.
Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:24
theorem
Function.Periodic.setLIntegral_Ioc_add_eq
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:33
theorem
Function.Periodic.aestronglyMeasurable
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:60
lemma
AddCircle.volume_preimage_equivIoc
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:114
theorem
MeasureTheory.eLpNorm_eq_eLpNorm_liftIoc
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.IntervalIntegral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean:130
theorem
MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul
The layer cake formula / Cavalieri's principle / tail probability formula:
Let f be a non-negative measurable function on a measure space. Let G be an
increasing absolutely continuous function on the positive real line, vanishing at the origin,
with derivative G' = g. Then the integral of the composition G ∘ f can be written as
the integral over the positive real line of the "tail measures" μ {ω | f(ω) > t} of f
weighted by g.
Roughly speaking, the statement is: ∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) > t}.
See MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul for a version with sets of the form
{ω | f(ω) ≥ t} instead.
Carleson.ToMathlib.MeasureTheory.Integral.Layercake · Carleson/ToMathlib/MeasureTheory/Integral/Layercake.lean:376
theorem
MeasureTheory.lintegral_comp_eq_lintegral_distribution_mul'
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.MeasureTheory.Integral.Layercake · Carleson/ToMathlib/MeasureTheory/Integral/Layercake.lean:479
theorem
ENNReal.Lp_add_le_sum
Minkowski inequality for finite sums of ENNReal-valued functions.
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:20
theorem
ENNReal.lintegral_prod_norm_pow_le'
A version of Hölder with multiple arguments, allowing ∞ as an exponent.
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:38
theorem
ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm
Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:79
theorem
ENNReal.sq_lintegral_mul_le_mul_lintegral_sq
Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared).
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:94
theorem
ENNReal.eLpNorm_convolution_le_of_norm_le_mul
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is
bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where
1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges
of f and g; see eLpNorm_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:444
theorem
ENNReal.eLpNorm_convolution_le_of_norm_le_mul'
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is
bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where
1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges
of f and g; see eLpNorm_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.
Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:460
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.