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 21 to 40 of 781 declarations.
lemma
tile_disjointness
Lemma 6.1.1.
Carleson.Antichain.Basic · Carleson/Antichain/Basic.lean:80
lemma
norm_Ks_le'
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.Basic · Carleson/Antichain/Basic.lean:126
lemma
maximal_bound_antichain
Lemma 6.1.2.
Carleson.Antichain.Basic · Carleson/Antichain/Basic.lean:153
lemma
Lemma6_1_3.eLpNorm_𝓜_le_eLpNorm_𝓜p_mul
A maximal function bound via an application of H"older's inequality
Carleson.Antichain.Basic · Carleson/Antichain/Basic.lean:286
lemma
dens2_antichain
Lemma 6.1.3 (inequality 6.1.11).
Carleson.Antichain.Basic · Carleson/Antichain/Basic.lean:424
lemma
Tile.correlation_kernel_bound
Second part of Lemma 6.2.1 (eq. 6.2.3).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:131
lemma
Tile.range_support
Lemma 6.2.2.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:168
lemma
Tile.uncertainty'
Lemma 6.2.3 (dist version).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:195
lemma
Tile.uncertainty
Lemma 6.2.3 (edist version).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:293
lemma
Tile.I12_le'
Inequality (6.2.28).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:330
lemma
Tile.I12_le
Inequality (6.2.29).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:384
lemma
Tile.volume_coeGrid_le
Inequality (6.2.32).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:414
lemma
Tile.bound_6_2_29
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:431
lemma
Tile.boundedCompactSupport_star_Ks_mul_g
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:464
lemma
Tile.bound_6_2_26
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:618
lemma
Tile.correlation_le_of_nonempty_inter
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:638
lemma
Tile.correlation_le_of_empty_inter
If (6.2.23) does not hold, the LHS is zero and the result follows trivially.
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:658
lemma
Tile.correlation_zero_of_ne_subset
Part 2 of Lemma 6.1.5 (claim 6.1.44).
Carleson.Antichain.TileCorrelation · Carleson/Antichain/TileCorrelation.lean:690
lemma
calculation_3
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:85
lemma
calculation_4
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:105
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.