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 741 to 760 of 781 declarations.

lemma

radius_change

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

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

lemma

cut_out_ball

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

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

theorem

cotlar_control

Lemma 10.1.3

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

lemma

globalMaximalFunction_zero_enorm_ae_zero

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

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

theorem

cotlar_set_F₁

Part 1 of Lemma 10.1.4 about F₁.

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

theorem

cotlar_set_F₂

Part 2 of Lemma 10.1.4 about F₂.

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

theorem

cotlar_estimate

Lemma 10.1.5

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

theorem

simple_nontangential_operator

Lemma 10.1.6. The formal statement includes the measurability of the operator. See also simple_nontangential_operator_le

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

theorem

simple_nontangential_operator_le

This is the first step of the proof of Lemma 10.0.2, and should follow from 10.1.6 + monotone convergence theorem. (measurability should be proven without any restriction on r.)

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

theorem

small_annulus_right

Part of Lemma 10.1.7, reformulated.

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

theorem

small_annulus_left

Part of Lemma 10.1.7, reformulated

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

theorem

nontangential_operator_boundary

Lemma 10.1.8.

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

theorem

nontangential_from_simple

Lemma 10.0.2. The formal statement includes the measurability of the operator.

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

theorem

two_sided_metric_carleson_hasLorentzType

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

Carleson.TwoSidedCarleson.RestrictedWeakType · Carleson/TwoSidedCarleson/RestrictedWeakType.lean:49

theorem

two_sided_metric_carleson_hasStrongType

The constant used in two_sided_metric_carleson_hasStrongType. -/ lemma C_carleson_hasStrongType_pos {a : ℕ} {q : ℝ≥0} : 0 < C_carleson_hasStrongType a q := C_LorentzInterpolation_pos

/- Theorem 10.0.1, reformulation

Carleson.TwoSidedCarleson.RestrictedWeakType · Carleson/TwoSidedCarleson/RestrictedWeakType.lean:126

theorem

lebesgue_differentiation

Lemma 10.2.2.

Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:73

lemma

depth_lt_iff_not_disjoint

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

Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.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.