Carleson's theorem
Generated by a source-level scanner, plus a Lean run where it succeeded: see the Trust page. Trust is UNKNOWN wherever Lean did not run. Indented declarations and macro-generated declarations are not listed.
- Lean files
- 120
- Declarations
- 3082
- Contain sorry
- 6
- Axioms
- 0
Lean4 Domain Explanation Language (L4DEL): 991 annotated, 0 flagged (errors or placeholders), 2039 without an L4DEL annotation. Run lean4-explainer annotate --file <path> for templates. Lean run with Lean (version 4.34.0-rc2, x86_64-w64-windows-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release) (cache-only rendering).
3082 declarations, 6 contain sorry, 0 declared as axioms; 120 files
Folders
- Carleson/ 117 files, 3076 declarations
Files
- Carleson.lean 117 imports, no declarations
- Challenge.lean 3 declarations
- Solution.lean 3 declarations