Skip to main content
therefore
Sign inSign up
Open navigation
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.

Research project101 GitHub starsApache-2.038 indexed versionsRepositoryFull history on Reservoir

Head version

74ef907d6bdb

74ef907d6bdb60797b88655bc16e3032fb835fdc

Toolchain
leanprover/lean4:v4.32.0
Revision date
23 Jul 2026
Dependencies
10
Versions
38

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

Package history

Showing 341 to 360 of 781 declarations.

lemma

Grid.dist_strictMono_iterate

Open the record for the exact Lean statement and complete source.

Carleson.GridStructure · Carleson/GridStructure.lean:439

lemma

integrable_cutoff_mul

Open the record for the exact Lean statement and complete source.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:71

lemma

dist_holderApprox_le

Part of Lemma 8.0.1: Equation (8.0.1). Note that the norm ||φ||_C^τ is normalized by definition, i.e., on the ball B (z, 2 * R), it is (2 * R) ^ τ times the best Hölder constant of φ, so the Lean statement corresponds to the blueprint statement.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:179

lemma

enorm_holderApprox_sub_le

Open the record for the exact Lean statement and complete source.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:246

lemma

holderApprox_le

Part of Lemma 8.0.1: sup norm control in Equation (8.0.2). Note that it only uses the sup norm of φ, no need for a Hölder control.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:266

lemma

norm_holderApprox_sub_le

Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2). Note that it only uses the sup norm of φ, no need for a Hölder control.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:406

lemma

iLipENorm_holderApprox'

Open the record for the exact Lean statement and complete source.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:445

lemma

iLipENorm_holderApprox_le

Open the record for the exact Lean statement and complete source.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:482

theorem

holder_van_der_corput

Proposition 2.0.5.

Carleson.HolderVanDerCorput · Carleson/HolderVanDerCorput.lean:507

lemma

iLipENorm_le_add

Open the record for the exact Lean statement and complete source.

Carleson.LipschitzNorm · Carleson/LipschitzNorm.lean:46

lemma

rightContinuous_integral_annulus

Let f be integrable over an annulus with fixed radii R₁, R₂. Then fun R ↦ ∫ y in oo x R R₂, f y is right-continuous at R₁.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:102

lemma

leftContinuous_integral_annulus

Let f be integrable over an annulus with fixed radii R₁, R₂. Then fun R ↦ ∫ y in oo x R₁ R, f y is left-continuous at R₂.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:185

lemma

integrableOn_coi_inner_annulus'

The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:279

lemma

exists_rat_near_carlesonOperatorIntegrand'

Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:330

lemma

lintegral_inv_vol_le

Open the record for the exact Lean statement and complete source.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:375

lemma

edist_carlesonOperatorIntegrand_le

Open the record for the exact Lean statement and complete source.

Carleson.MetricCarleson.Basic · Carleson/MetricCarleson/Basic.lean:403

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.