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 721 to 740 of 781 declarations.

lemma

MeasureTheory.wnorm_const_smul_le

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

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:682

lemma

MeasureTheory.wnorm_const_smul_le'

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

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:704

lemma

MeasureTheory.eLpNorm_eq_distribution

The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without taking powers.

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:874

lemma

czOperator_bound

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

Carleson.TwoSidedCarleson.Basic · Carleson/TwoSidedCarleson/Basic.lean:18

lemma

czOperator_aestronglyMeasurable'

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

Carleson.TwoSidedCarleson.Basic · Carleson/TwoSidedCarleson/Basic.lean:55

lemma

czOperator_welldefined

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

Carleson.TwoSidedCarleson.Basic · Carleson/TwoSidedCarleson/Basic.lean:85

theorem

two_sided_metric_carleson

The constant used in two_sided_metric_carleson. Has value 2 ^ (474 * a ^ 3) / (q - 1) ^ 6 in the blueprint. -/ def C10_0_1 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := C_K a ^ 2 * C1_0_2 a q

lemma C10_0_1_pos {a : ℕ} {q : ℝ≥0} (hq : 1 < q) : 0 < C10_0_1 a q := mul_pos (pow_two_pos_of_ne_zero <| by simp_rw [ne_eq, C_K_pos.ne', not_false_eq_true]) (C1_0_2_pos hq)

variable {X : Type*} {a : ℕ} [MetricSpace X] [DoublingMeasure X (defaultA a : ℕ)] variable {τ C r R : ℝ} {q q' : ℝ≥0} variable {F G : Set X} variable {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] variable [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)]

/-! ## Theorem 10.0.1 -/

/- Theorem 10.0.1

Carleson.TwoSidedCarleson.MainTheorem · Carleson/TwoSidedCarleson/MainTheorem.lean:30

lemma

estimate_10_1_2

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

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:37

lemma

estimate_10_1_3

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

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:72

lemma

estimate_10_1_4

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

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:197

theorem

estimate_x_shift

Lemma 10.1.2

Carleson.TwoSidedCarleson.NontangentialOperator · Carleson/TwoSidedCarleson/NontangentialOperator.lean:233

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.