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 761 to 780 of 781 declarations.
lemma
depth_lt_top_iff_ne_univ
A point has finite depth in O iff O is not the whole space.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:186
lemma
depth_bound_1
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:210
lemma
depth_bound_2
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:246
lemma
depth_bound_3
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:262
lemma
ball_covering_bounded_intersection
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:280
lemma
ball_covering'
Lemma 10.2.4, but following the blueprint exactly (with a countable set of centres rather than
functions from ℕ).
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:318
lemma
ball_covering_finite
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:360
theorem
ball_covering
Lemma 10.2.4.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:428
lemma
czBall_subset_czPartition
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:573
lemma
czPartition_pairwiseDisjoint
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:594
lemma
iUnion_czPartition
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:617
lemma
tsum_czRemainder'
Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases).
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:737
lemma
aemeasurable_czApproximation
Part of Lemma 10.2.5 (both cases).
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:752
lemma
enorm_czApproximation_le_infinite
Equation (10.2.17) specialized to the general case.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:844
lemma
eLpNorm_czRemainder'_le
Part of Lemma 10.2.5, equation (10.2.21) (general case).
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:953
lemma
eLpNorm_czRemainder_le
Part of Lemma 10.2.5, equation (10.2.21) (finite case).
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:994
lemma
estimate_good
Lemma 10.2.6
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:1092
lemma
czOperatorBound_inner_le
Open the record for the exact Lean statement and complete source.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:1511
lemma
distribution_czOperatorBound
Lemma 10.2.8
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:1594
lemma
estimate_bad
Lemma 10.2.9
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:1649
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.