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 81 to 100 of 781 declarations.

lemma

rcarleson'_restrict

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

Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:24

lemma

distribution_carlesonOperatorReal_le

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

Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:96

lemma

C_control_approximation_effect_property

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

Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:136

lemma

control_approximation_effect

The constant used in C_control_approximation_effect. -/ def C_control_approximation_effect (δ ε p : ℝ≥0) : ℝ≥0 := min (2 * (↑δ / 2) * ((2 * Real.toNNReal π) ^ (1 - p.toReal⁻¹))⁻¹) (C_distribution_carlesonOperatorReal_le (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) p)

lemma C_control_approximation_effect_pos {δ ε p : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect δ ε p := lt_min (by positivity) (C_distribution_carlesonOperatorReal_le_pos (by positivity) (by positivity))

lemma C_control_approximation_effect_property {δ ε p : ℝ≥0} (hp : 1 ≤ p) : C_control_approximation_effect δ ε p * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) ≤ 2 * (↑δ / 2) := by calc _ _ ≤ 2 * (↑δ / 2) * ((2 * Real.toNNReal π) ^ (1 - p.toReal⁻¹))⁻¹ * (2 * ENNReal.ofReal π) ^ (1 - p.toReal⁻¹) := by gcongr norm_cast exact min_le_left _ _ _ = 2 * (↑δ / 2) := by rw [ENNReal.coe_inv (by simp [Real.pi_pos]), ENNReal.coe_rpow_of_nonneg _ (by simp only [sub_nonneg]; exact inv_le_one_of_one_le₀ hp), ENNReal.coe_mul, ENNReal.coe_ofNat, ENNReal.ofNNReal_toNNReal, ENNReal.inv_mul_cancel_right (by positivity) (ENNReal.rpow_ne_top' (by positivity) (ENNReal.mul_ne_top (by simp) (by simp)))]

lemma C_control_approximation_effect_le {δ ε p : ℝ≥0} : ENNReal.ofNNReal (C_control_approximation_effect δ ε p) ≤ (C_distribution_carlesonOperatorReal_le (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) p) := by simp only [ENNReal.coe_le_coe] exact min_le_right _ _

/- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.

Carleson.Classical.ControlApproximationEffect · Carleson/Classical/ControlApproximationEffect.lean:157

lemma

ENNReal.le_on_subset

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:22

lemma

Dirichlet_Hilbert_diff

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:69

lemma

integrable_annulus

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:125

lemma

intervalIntegrable_mul_dirichletKernel'

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:136

lemma

intervalIntegrable_mul_dirichletKernel'_max

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:148

lemma

domain_reformulation

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:170

lemma

le_CarlesonOperatorReal

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:229

lemma

partialFourierSum_bound

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

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:371

lemma

rcarleson_exceptional_set_estimate

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:22

lemma

rcarleson_exceptional_set_estimate_specific

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:50

lemma

rcarleson_exceptional_set_estimate_specific'

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:71

lemma

rcarleson_exceptional_set_estimate_specific''

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:90

theorem

C_distribution_carlesonOperatorReal_le'_property

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:115

lemma

distribution_carlesonOperatorReal_le'

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

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:129

lemma

control_approximation_effect'

The constant used in C_control_approximation_effect'. -/ def C_control_approximation_effect' (δ ε : ℝ≥0) : ℝ≥0 := min (δ / toNNReal (2 * π)) (C_distribution_carlesonOperatorReal_le' (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2))

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_pos {δ ε : ℝ≥0} (δpos : 0 < δ) (εpos : 0 < ε) : 0 < C_control_approximation_effect' δ ε := lt_min (by positivity) (C_distribution_carlesonOperatorReal_le'_pos (by positivity) (by positivity))

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_property {δ ε : ℝ≥0} : C_control_approximation_effect' δ ε * ENNReal.ofReal (2 * π) ≤ δ := by unfold C_control_approximation_effect' rw [ENNReal.coe_min, min_mul, ENNReal.coe_div (by positivity), ENNReal.ofReal, ENNReal.div_mul_cancel (by positivity) (by simp)] exact min_le_left _ _

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx lemma C_control_approximation_effect'_le {δ ε : ℝ≥0} : C_control_approximation_effect' δ ε ≤ C_distribution_carlesonOperatorReal_le' (2 * π * (↑δ / 2) / 2).toNNReal (ε / 2) := by exact min_le_right _ _

--TODO: can be removed once two_sided_metric_carleson_hasStrongType no longer depends on sorryAx /- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.

Carleson.Classical.ControlApproximationEffectContinuous · Carleson/Classical/ControlApproximationEffectContinuous.lean:177

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.