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 781 to 781 of 781 declarations.
lemma
estimate_czOperator
Lemma 10.0.3, blueprint form.
Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:1704
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.