Skip to main content
therefore
Sign inSign up
Open navigation
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.

Research project101 GitHub starsApache-2.038 indexed versionsRepositoryFull 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 481 to 500 of 781 declarations.

theorem

Metric.secondCountableTopology_of_almost_dense_set_balls_nat

A pseudometric space is second countable if, for every ε > 0 and every ball B with natural number radius around a given point x₀, there is a countable set which is ε-dense in B.

Carleson.ToMathlib.CoveredByBalls · Carleson/ToMathlib/CoveredByBalls.lean:153

lemma

ENNReal.coe_biSup

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

Carleson.ToMathlib.Data.ENNReal · Carleson/ToMathlib/Data/ENNReal.lean:34

lemma

ENNReal.finsetSum_biSup

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

Carleson.ToMathlib.Data.ENNReal · Carleson/ToMathlib/Data/ENNReal.lean:59

lemma

ENNReal.enorm_sum_eq_sum_enorm

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

Carleson.ToMathlib.Data.ENNReal · Carleson/ToMathlib/Data/ENNReal.lean:91

lemma

ENNReal.biInf_enorm_sub_le

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

Carleson.ToMathlib.Data.ENNReal · Carleson/ToMathlib/Data/ENNReal.lean:143

lemma

MeasureTheory.approx_above_superset

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

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:127

lemma

MeasureTheory.distribution_pow

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

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:212

lemma

MeasureTheory.distribution_mono_left

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

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:225

lemma

MeasureTheory.distribution_add

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

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:362

theorem

MeasureTheory.eLpNorm_top_smul

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

Carleson.ToMathlib.ENorm · Carleson/ToMathlib/ENorm.lean:116

theorem

lintegral_ball_le_volume_mul_globalMaximalFunction

The integral of the norm of a function over a particular ball is smaller than the volume of the ball times the value of the globalMaximalFuntion at a point inside that ball.

Carleson.ToMathlib.HardyLittlewood · Carleson/ToMathlib/HardyLittlewood.lean:45

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.