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 121 to 140 of 781 declarations.
lemma
norm_dirichletApproxAux_le
Open the record for the exact Lean statement and complete source.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:585
lemma
norm_sub_indicator_k
Open the record for the exact Lean statement and complete source.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:598
lemma
dist_dirichletApprox_le
Lemma 11.3.5, part 4.
The kernel dirichletApprox approximates well the kernel of the Hilbert transform, on [-π, π],
up to an error which is uniformly bounded in L^1 (as it is bounded by a constant multiple
of niceKernel).
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:647
lemma
norm_czOperator_le_add
As the kernel of the Hilbert transform is well approximated by dirichletApprox, up to an
error controlled by 12 * niceKernel r, we may bound czOperator K in terms of these. As the
approximation only works in the interval [-π, π], this statement is only true for a
point x in [2, 3] and a function supported in [1, 4], as this means all values of the
approximation that will show up will be in [-2, 2] ⊆ [-π, π].
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:693
lemma
eLpNorm_czOperator_restrict_two_three_of_support_subset
The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]),
uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is
bounded by the sum of two operators which are both bounded: one is the convolution
with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has
a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.
In this version, we assume that the function is supported in [1, 4], but we will drop this
assumption just after this lemma, in eLpNorm_czOperator_restrict_two_three.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:769
lemma
eLpNorm_czOperator_restrict_two_three
The operator czOperator K r is bounded from L^2 [1, 4] to L^2 [2, 3],
uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is
bounded by the sum of two operators which are both bounded: one is the convolution
with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has
a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:847
lemma
eLpNorm_czOperator_restrict
The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1],
uniformly in r and a. This follows from the same fact from L^2 [1, 4] to L^2 [2, 3]
proved using Fourier series, and translation invariance.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:879
lemma
eLpNorm_czOperator_sq
Open the record for the exact Lean statement and complete source.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:907
lemma
eLpNorm_czOperator
Open the record for the exact Lean statement and complete source.
Carleson.Classical.HilbertStrongType · Carleson/Classical/HilbertStrongType.lean:955
lemma
partialFourierSumL2_norm
Open the record for the exact Lean statement and complete source.
Carleson.Classical.SpectralProjectionBound · Carleson/Classical/SpectralProjectionBound.lean:27
lemma
intervalIntegrable_continuous_mul_lipschitzOnWith
Open the record for the exact Lean statement and complete source.
Carleson.Classical.VanDerCorput · Carleson/Classical/VanDerCorput.lean:23
lemma
van_der_Corput
Open the record for the exact Lean statement and complete source.
Carleson.Classical.VanDerCorput · Carleson/Classical/VanDerCorput.lean:54
lemma
disjoint_TilesAt_of_ne
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:27
lemma
dens1_le_dens'
Lemma 5.3.11
Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:95
lemma
pairwiseDisjoint_ℭ₁'
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:146
lemma
setA_subset_iUnion_𝓒
Open the record for the exact Lean statement and complete source.
Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:309
lemma
third_exception_rearrangement
A rearrangement for Lemma 5.2.9 that does not require the tile structure.
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:24
lemma
first_exception'
Lemma 5.2.1
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:66
lemma
dense_cover
Lemma 5.2.2
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:137
lemma
pairwiseDisjoint_E1
Lemma 5.2.3
Carleson.Discrete.ExceptionalSet · Carleson/Discrete/ExceptionalSet.lean:167
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.