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.

Research project101 GitHub starsApache-2.038 indexed versionsRepository Full history on Reservoir

Head version

74ef907d6bdb

74ef907d6bdb60797b88655bc16e3032fb835fdc

Toolchain: leanprover/lean4:v4.32.0
Revision date: 23 Jul 2026
Dependencies: 10
Versions: 38

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

Package history

Showing 561 to 580 of 781 declarations.

theorem

ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul

Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms on that interval, 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_Ioc_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

Carleson.ToMathlib.MeasureTheory.Integral.MeanInequalities · Carleson/ToMathlib/MeasureTheory/Integral/MeanInequalities.lean:527

theorem

lintegral_antitone_mul_le

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Integral.Misc · Carleson/ToMathlib/MeasureTheory/Integral/Misc.lean:13

lemma

AddCircle.map_subtypeVal_map_equivIoc_volume

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:65

theorem

MeasureTheory.map_coe_addCircle_volume_eq

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:101

theorem

AddCircle.liftIco_convolution_liftIco

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:136

theorem

AddCircle.eLpNorm_liftIoc

The norm of the lift of a function f is equal to the norm of f on that period.

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:163

lemma

MeasureTheory.aeMeasurable_withDensity_inv

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.AEMeasurable · Carleson/ToMathlib/MeasureTheory/Measure/AEMeasurable.lean:13

theorem

MeasureTheory.aemeasurable_Ici_of_forall_Icc

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.AEMeasurable · Carleson/ToMathlib/MeasureTheory/Measure/AEMeasurable.lean:34

lemma

MeasureTheory.eq_zero_of_isDoubling_zero

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:43

lemma

MeasureTheory.eq_zero_of_isDoubling_lt_one

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:58

lemma

MeasureTheory.measure_ball_le_same

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:98

lemma

MeasureTheory.isOpenPosMeasure_of_isDoubling

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:126

lemma

MeasureTheory.IsDoubling.measure_ball_lt_top

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:184

lemma

MeasureTheory.IsDoubling.allBallsCoverBalls

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:199

lemma

MeasureTheory.one_le_A

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:313

lemma

MeasureTheory.measureReal_ball_le_same

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:353

lemma

MeasureTheory.measureReal_ball_le_same'

Version of measureReal_ball_le_same without ceiling function.

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:368

lemma

ENNReal.map_toReal_eq_map_toReal_comap_ofReal'

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:49

lemma

Measure.Subtype.sigmaFinite

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:107

theorem

NNReal.smul_map_volume_mul_left

Open the record for the exact Lean statement and complete source.

Carleson.ToMathlib.MeasureTheory.Measure.NNReal · Carleson/ToMathlib/MeasureTheory/Measure/NNReal.lean:149

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.