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 1 to 20 of 781 declarations.
lemma
dens1_antichain_dach
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:92
lemma
eLpNorm_le_M14
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:149
lemma
dach_bound
Equations (6.1.34) to (6.1.37) in Lemma 6.1.4.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:174
lemma
M14_bound
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:232
lemma
dens1_antichain_sq
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:262
lemma
dens1_antichain
Lemma 6.1.4.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:309
theorem
antichain_operator
Proposition 2.0.3.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:362
theorem
antichain_operator'
Version of the antichain operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:432
theorem
antichain_operator_le_volume
Version of the antichain operator theorem, but controlling the integral of the norm instead of
the integral of the function multiplied by another function, and with the upper bound in terms
of volume F and volume G.
Carleson.Antichain.AntichainOperator · Carleson/Antichain/AntichainOperator.lean:464
lemma
Antichain.tile_reach
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:35
lemma
Antichain.stack_density
Lemma 6.3.2.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:171
lemma
Antichain.Ep_inter_G_inter_Ip'_subset_E2
We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 ϑ N) with 𝔰 p' < 𝔰 p such that
(𝓘 p : Set X) ∩ (𝓘 p') ≠ ∅. The variable p' corresponds to 𝔭_ϑ in the blueprint.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:296
lemma
Antichain.local_antichain_density
Lemma 6.3.3.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:324
lemma
Antichain.I_p_subset_union_L
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:446
lemma
Antichain.union_L'_eq_union_I_p
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:490
lemma
Antichain.exists_larger_grid
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:561
lemma
Antichain.global_antichain_density
Lemma 6.3.4.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:899
lemma
Antichain.C2_0_6_q₆_le
A very involved bound needed for Lemma 6.1.4.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:958
lemma
Antichain.le_C6_1_6
Open the record for the exact Lean statement and complete source.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:1079
lemma
Antichain.tile_count
Lemma 6.1.6.
Carleson.Antichain.AntichainTileCount · Carleson/Antichain/AntichainTileCount.lean:1107
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.