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 461 to 480 of 781 declarations.
lemma
dens₁_le_one
This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number. -/
def dens₂ (𝔓' : Set (𝔓 X)) : ℝ≥0∞ :=
⨆ (p ∈ 𝔓') (r ≥ 4 * (D ^ 𝔰 p : ℝ)),
volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r)
lemma le_dens₂ (𝔓' : Set (𝔓 X)) {p : 𝔓 X} (hp : p ∈ 𝔓') {r : ℝ} (hr : r ≥ 4 * (D ^ 𝔰 p : ℝ)) : volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r) ≤ dens₂ 𝔓' := le_trans (le_iSup₂ (α := ℝ≥0∞) r hr) (le_iSup₂ p hp)
set_option backward.isDefEq.respectTransparency false in lemma dens₂_eq_biSup_dens₂ (𝔓' : Set (𝔓 X)) : dens₂ (𝔓') = ⨆ (p ∈ 𝔓'), dens₂ ({p}) := by simp [dens₂]
/- A rough estimate. It's also less than 2 ^ (-a)
Carleson.TileStructure · Carleson/TileStructure.lean:379
lemma
volume_E₂_le_dens₁_mul_volume
Open the record for the exact Lean statement and complete source.
Carleson.TileStructure · Carleson/TileStructure.lean:397
lemma
stackSize_le_one_of_pairwiseDisjoint
Open the record for the exact Lean statement and complete source.
Carleson.TileStructure · Carleson/TileStructure.lean:459
lemma
exists_maximal_disjoint_covering_subfamily
Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything.
Carleson.TileStructure · Carleson/TileStructure.lean:492
lemma
pairwiseDisjoint_iteratedMaximalSubfamily
Open the record for the exact Lean statement and complete source.
Carleson.TileStructure · Carleson/TileStructure.lean:550
lemma
eq_biUnion_iteratedMaximalSubfamily
Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.
Carleson.TileStructure · Carleson/TileStructure.lean:569
lemma
MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm
This implies both of the following theorems convolutionExists_of_memLp_memLp and
enorm_convolution_le_eLpNorm_mul_eLpNorm.
Carleson.ToMathlib.Analysis.Convolution · Carleson/ToMathlib/Analysis/Convolution.lean:49
theorem
fourier_comp_equivAddCircle
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Analysis.Fourier.AddCircle · Carleson/ToMathlib/Analysis/Fourier/AddCircle.lean:7
lemma
RCLike.decomposition
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Analysis.RCLike.Components · Carleson/ToMathlib/Analysis/RCLike/Components.lean:62
theorem
RCLike.induction
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Analysis.RCLike.Components · Carleson/ToMathlib/Analysis/RCLike/Components.lean:217
theorem
RCLike.aestronglyMeasurable_iff_aestronglyMeasurable_embedRCLike
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Analysis.RCLike.Misc · Carleson/ToMathlib/Analysis/RCLike/Misc.lean:19
theorem
MeasureTheory.setLIntegral_Ioo_rpow
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Analysis.SpecialFunctions.Integrals.Basic · Carleson/ToMathlib/Analysis/SpecialFunctions/Integrals/Basic.lean:14
lemma
Set.EAnnulus.oc_eq_annulus
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Annulus · Carleson/ToMathlib/Annulus.lean:340
lemma
Set.EAnnulus.cc_eq_annulus
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.Annulus · Carleson/ToMathlib/Annulus.lean:356
theorem
MeasureTheory.BoundedCompactSupport.mono
If ‖f‖ is bounded by g and g is bounded compactly supported, then so is f.
Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:270
theorem
MeasureTheory.BoundedCompactSupport.mono_norm
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:282
lemma
MeasureTheory.BoundedCompactSupport.sq_eLpNorm_le_sums
Used in Proposition 2.0.4.
Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:320
theorem
MeasureTheory.BoundedCompactSupport.prod_mul
An elementary tensor of bounded compactly supported functions is bounded compactly supported.
Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:363
lemma
BoundedCompactSupport.mul_bdd_right''
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.BoundedCompactSupport · Carleson/ToMathlib/BoundedCompactSupport.lean:471
lemma
CoveredByBalls.trans
Open the record for the exact Lean statement and complete source.
Carleson.ToMathlib.CoveredByBalls · Carleson/ToMathlib/CoveredByBalls.lean:65
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.