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 41 to 60 of 781 declarations.
lemma
calculation_5
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:139
lemma
calculation_12
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:194
lemma
calculation_14
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:235
lemma
near_1_geometric_bound
A bound on the sum of a geometric series whose ratio is close to 1.
Carleson.Calculations · Carleson/Calculations.lean:282
lemma
calculation_convexity_bound
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:295
lemma
calculation_150
Open the record for the exact Lean statement and complete source.
Carleson.Calculations · Carleson/Calculations.lean:329
lemma
close_smooth_approx_periodic
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:20
lemma
close_smooth_approx_periodic_Lp
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:41
lemma
summable_of_le_on_nonzero
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:106
lemma
fourierCoeffOn_bound
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:132
lemma
periodic_deriv
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:153
lemma
fourierCoeffOn_ContDiff_two_bound
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:170
lemma
int_sum_nat
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:204
lemma
fourierConv_ofTwiceDifferentiable
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Approximation · Carleson/Classical/Approximation.lean:239
theorem
fourierCoeff_eq_fourierCoeff_of_aeeq
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:17
theorem
partialFourierSum'_comp_equivAddCircle
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:32
lemma
partialFourierSum_eq_partialFourierSum'
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:53
lemma
partialFourierSum'_eq_partialFourierSum_apply
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:79
lemma
partialFourierSum'_eq_partialFourierSumLp
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:104
lemma
partialFourierSum_aeeq_partialFourierSumLp
Open the record for the exact Lean statement and complete source.
Carleson.Classical.Basic · Carleson/Classical/Basic.lean:114
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.