`Carleson/Defs.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

36 declarations, 0 contain sorry, 0 declared as axioms

Key definitions and setup for the Carleson project

This file contains the statements of the main theorems from the Carleson formalization project: Theorem 1.0.1 (classical Carleson), Theorem 1.1.1 (metric space Carleson) and Theorem 1.1.2 (linearised metric Carleson), as well as the definitions required to state these results.

These are intentionally put in a very low-level file to enable running the comparator tool.

Main definitions and results

MeasureTheory.DoublingMeasure: A metric space with a measure with some nice propreties, including a doubling condition. This is called a "doubling metric measure space" in the blueprint.
FunctionDistances: class stating that continuous functions have distances associated to every ball.
IsOneSidedKernel K states that K is a one-sided Calderon-Zygmund kernel.
KernelProofData: Data common through most of chapters 2-7. These contain the minimal axioms for kernel-summand's proof.
MeasureTheory.DoublingMeasure: A metric space with a measure with some nice propreties, including a doubling condition. This is called a "doubling metric measure space" in the blueprint.
FunctionDistances: class stating that continuous functions have distances associated to every ball.
IsOneSidedKernel K states that K is a one-sided Calderon-Zygmund kernel.
KernelProofData: Data common through most of chapters 2-7. These contain the minimal axioms for kernel-summand's proof.
ClassicalCarleson: statement of Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions (Theorem 1.0.1 in the blueprint).
MetricSpaceCarleson: statement of Theorem 1.1.1 from the blueprint.
LinearizedMetricCarleson: statement of Theorem 1.1.2 from the blueprint.

Imports (1)

Mathlib.Analysis.Fourier.AddCircle

Imported by 8 files

def partialFourierSum Partial Fourier sum line 43 source
Source documentation
The Nᵗʰ partial Fourier sum of f : ℝ → ℂ for N : ℕ.
L4DEL explanation
The N-th partial sum adds the Fourier modes of f with frequency from -N to N, using coefficients taken over one period [0, 2*pi].
1. Sum over integers n from -N to N of the Fourier coefficient of f at n times the n-th exponential character evaluated at x.
See also: ClassicalCarleson
Sources and attribution: Pinned Lean source (8972acdfd953)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex
Proof uses: Finset.sum, Int, Finset.Icc, Neg.neg, HMul.hMul, fourierCoeffOn, OfNat.ofNat, Real.pi, Real.two_pi_pos, ContinuousMap, AddCircle, AddSubgroup.zmultiples, fourier
38 instances, coercions and auxiliary constants left out.
```
def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂ := ∑ n ∈ Finset.Icc (-(N : ℤ)) N,
…
```
def Real.vol The "volume function" V line 52 source
Source documentation
The "volume function" V. Preferably use vol instead.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, Real
Proof uses: MeasureTheory.Measure.real, MeasureTheory.MeasureSpace.volume, Metric.ball, Dist.dist
2 instances, coercions and auxiliary constants left out.
```
protected def Real.vol [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ :=
…
```
def Set.Annulus.oo line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioo, Dist.dist
3 instances, coercions and auxiliary constants left out.
def Set.EAnnulus.oo line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, ENNReal, Set
Proof uses: Set.ofPred, Membership.mem, Set.Ioo, EDist.edist
8 instances, coercions and auxiliary constants left out.
def iLipENorm The inhomogeneous Lipschitz norm on a ball line 60 source
Source documentation
The inhomogeneous Lipschitz norm on a ball.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedField, PseudoMetricSpace, Real, ENNReal
Proof uses: HAdd.hAdd, iSup, Membership.mem, Set, Metric.ball, ENorm.enorm, HMul.hMul, ENNReal.ofReal, Ne, HDiv.hDiv, HSub.hSub, EDist.edist
41 instances, coercions and auxiliary constants left out.
```
def iLipENorm {𝕜 X : Type*} [NormedField 𝕜] [PseudoMetricSpace X]
  (φ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ≥0∞ :=
…
```
def localOscillation The local oscillation of two functions w.r.t line 67 source
Source documentation
The local oscillation of two functions w.r.t. a set E. This is d_E in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, PseudoMetricSpace, Set, ContinuousMap, ENNReal
Proof uses: iSup, Prod, Membership.mem, SProd.sprod, ENNReal.ofReal, Norm.norm, HAdd.hAdd, HSub.hSub, Prod.fst, Prod.snd
42 instances, coercions and auxiliary constants left out.
```
def localOscillation (E : Set X) (f g : C(X, 𝕜)) : ℝ≥0∞ :=
…
```
Mentions: E, g
structure BoundedFiniteSupport Bounded measurable function $g$ on $X$ supported on a set of finite measure line 74 source
Source documentation
Bounded measurable function $g$ on $X$ supported on a set of finite measure

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, TopologicalSpace, ENorm, Zero, autoParam, MeasureTheory.Measure
1 instances, coercions and auxiliary constants left out.
```
structure BoundedFiniteSupport (f : X → E) (μ : Measure X := by volume_tac) : Prop where
…
```
Mentions: E
def MeasureTheory.HasBoundedStrongType A weaker version of HasStrongType line 80 source
Source documentation
A weaker version of HasStrongType. This is the same as HasStrongType if T is continuous w.r.t. the L^2 norm, but weaker in general.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ENorm, TopologicalSpace, Zero, MeasurableSpace, ENNReal, MeasureTheory.Measure
Proof uses: BoundedFiniteSupport, And, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul
6 instances, coercions and auxiliary constants left out.
```
def MeasureTheory.HasBoundedStrongType
    {ε₁ ε₂ : Type*} [ENorm ε₁] [ENorm ε₂] [TopologicalSpace ε₁] [TopologicalSpace ε₂] [Zero ε₁]
    {α α' : Type*} {_x : MeasurableSpace α} {_x' : MeasurableSpace α'}
    (T : (α → ε₁) → (α' → ε₂))
    (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0∞) : Prop :=
…
```
Mentions: α', T, c
class MeasureTheory.Measure.IsDoubling A doubling measure is a measure on a metric space with the condition that doubling the radius of a ball only increases the volume by a constant factor, independent of the ball line 90 source
Source documentation
A doubling measure is a measure on a metric space with the condition that doubling the radius of a ball only increases the volume by a constant factor, independent of the ball.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, PseudoMetricSpace, MeasureTheory.Measure, outParam, NNReal
```
class MeasureTheory.Measure.IsDoubling {X : Type*} [MeasurableSpace X] [PseudoMetricSpace X]
    (μ : Measure X) (A : outParam ℝ≥0) : Prop where
…
```
Mentions: A
class MeasureTheory.DoublingMeasure A metric space with a measure with some nice properties, including a doubling condition line 98 source
Source documentation
A metric space with a measure with some nice properties, including a doubling condition. This is called a "doubling metric measure space" in the blueprint. A will usually be 2 ^ a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, NNReal, PseudoMetricSpace
```
class MeasureTheory.DoublingMeasure (X : Type*) (A : outParam ℝ≥0) [PseudoMetricSpace X] extends
    CompleteSpace X, LocallyCompactSpace X,
    MeasureSpace X, BorelSpace X,
    IsLocallyFiniteMeasure (volume : Measure X),
    Measure.IsDoubling (volume : Measure X) A, NeZero (volume : Measure X) where
…
```
Mentions: A, MeasureTheory.Measure.IsDoubling
class FunctionDistances A class stating that continuous functions have distances associated to every ball line 113 source
Source documentation
A class stating that continuous functions have distances associated to every ball. We use a separate type to conveniently index these functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, NormedField, TopologicalSpace
```
class FunctionDistances (𝕜 : outParam Type*) (X : Type u) [NormedField 𝕜] [TopologicalSpace X] where
…
```
instance (instance at line 129) line 129 source
instance (instance at line 130) line 130 source
def WithFunctionDistance Class used to endow Θ X with a pseudometric space structure line 137 source
Source documentation
Class used to endow Θ X with a pseudometric space structure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RCLike, PseudoMetricSpace, FunctionDistances, Real
Proof uses: FunctionDistances.Θ
8 instances, coercions and auxiliary constants left out.
```
def WithFunctionDistance (x : X) (r : ℝ) := Θ X
```
instance (instance at line 139) line 139 source
class inductive CoveredByBalls s can be covered by at most N balls with radius r line 153 source
Source documentation
s can be covered by at most N balls with radius r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Set, Nat, Real
```
class inductive CoveredByBalls (s : Set X) (n : ℕ) (r : ℝ) : Prop where
…
```
Mentions: s
def BallsCoverBalls Balls of radius r in X are covered by n balls of radius r' line 160 source
Source documentation
Balls of radius r in X are covered by n balls of radius r'

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Nat
Proof uses: CoveredByBalls, Metric.ball
```
def BallsCoverBalls (r r' : ℝ) (n : ℕ) : Prop := ∀ x : X, CoveredByBalls (ball x r) n r'
…
```
Mentions: CoveredByBalls
def AllBallsCoverBalls For all r, balls of radius r in X are covered by n balls of radius a * r line 164 source
Source documentation
For all r, balls of radius r in X are covered by n balls of radius a * r

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Real, Nat
Proof uses: BallsCoverBalls, HMul.hMul
2 instances, coercions and auxiliary constants left out.
```
def AllBallsCoverBalls (a : ℝ) (n : ℕ) : Prop := ∀ r : ℝ, BallsCoverBalls X (a * r) r n
```
Mentions: BallsCoverBalls
class CompatibleFunctions A set Θ of (continuous) functions is compatible line 167 source
Source documentation
A set Θ of (continuous) functions is compatible. A will usually be 2 ^ a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, Nat, RCLike, PseudoMetricSpace
```
class CompatibleFunctions (𝕜 : outParam Type*) (X : Type u) (A : outParam ℕ)
  [RCLike 𝕜] [PseudoMetricSpace X] extends FunctionDistances 𝕜 X where
…
```
Mentions: A, FunctionDistances
class IsCancellative Θ is τ-cancellative line 191 source
Source documentation
Θ is τ-cancellative. τ will usually be 1 / a

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, Real, CompatibleFunctions
7 instances, coercions and auxiliary constants left out.
```
class IsCancellative (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop where
…
```
Mentions: CompatibleFunctions, A
def upperRadius R_Q(θ, x) defined in (1.1.17) line 200 source
Source documentation
R_Q(θ, x) defined in (1.1.17).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, FunctionDistances, Real, FunctionDistances.Θ, ENNReal
Proof uses: iSup, LT.lt, Dist.dist, WithFunctionDistance, OfNat.ofNat, ENNReal.ofReal
19 instances, coercions and auxiliary constants left out.
```
def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ≥0∞ :=
…
```
Mentions: FunctionDistances
def linearizedNontangentialOperator The linearized maximally truncated nontangential Calderon–Zygmund operator T_Q^θ line 204 source
Source documentation
The linearized maximally truncated nontangential Calderon–Zygmund operator T_Q^θ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, FunctionDistances.Θ, Complex, ENNReal
Proof uses: iSup, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.EAnnulus.oo, ENNReal.ofReal, Min.min, upperRadius, HMul.hMul
49 instances, coercions and auxiliary constants left out.
```
def linearizedNontangentialOperator [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X)
    (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: FunctionDistances, K
def nontangentialOperator The maximally truncated nontangential Calderon–Zygmund operator T_* line 211 source
Source documentation
The maximally truncated nontangential Calderon–Zygmund operator T_*.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, Complex, ENNReal
Proof uses: iSup, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul
44 instances, coercions and auxiliary constants left out.
```
def nontangentialOperator (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: K
def carlesonOperatorIntegrand The integrand in the (linearized) Carleson operator line 216 source
Source documentation
The integrand in the (linearized) Carleson operator. This is G in Lemma 3.0.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, Complex, FunctionDistances.Θ
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I
30 instances, coercions and auxiliary constants left out.
```
def carlesonOperatorIntegrand [FunctionDistances ℝ X] (K : X → X → ℂ)
    (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: FunctionDistances, K
def linearizedCarlesonOperator The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞ line 222 source
Source documentation
The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, FunctionDistances.Θ, Complex, ENNReal
Proof uses: iSup, LT.lt, OfNat.ofNat, ENorm.enorm, carlesonOperatorIntegrand
38 instances, coercions and auxiliary constants left out.
```
def linearizedCarlesonOperator [FunctionDistances ℝ X] (Q : X → Θ X) (K : X → X → ℂ)
    (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: FunctionDistances, K
def carlesonOperator The generalized Carleson operator line 228 source
Source documentation
The generalized Carleson operator T, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.
L4DEL explanation
It takes, at each point, the largest truncated oscillatory integral of K times f against a phase, over all phases and all inner/outer truncation radii.
1. For a fixed phase theta, the linearized operator takes the supremum over radii 0 < R1 < R2 of the norm of the integral of K x y * f y * exp(i theta y) over the annulus R1 < dist(x,y) < R2.
2. carlesonOperator is the supremum of this over all phases theta in the space of phases; values lie in the extended nonnegative reals.
Prerequisites: linearizedCarlesonOperator, carlesonOperatorIntegrand
See also: MetricSpaceCarleson
Sources and attribution: Pinned Lean source (8972acdfd953)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, PseudoMetricSpace, MeasureTheory.DoublingMeasure, NNReal, FunctionDistances, Real, Complex, ENNReal
Proof uses: iSup, FunctionDistances.Θ, linearizedCarlesonOperator
25 instances, coercions and auxiliary constants left out.

phase space: the space Theta X of functions used as oscillation phases in the Carleson operator; it carries a compatible family of metrics on balls
```
def carlesonOperator [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
…
```
Mentions: FunctionDistances, K
abbrev defaultA This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions line 235 source
Source documentation
This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions

standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
@[simp] abbrev defaultA (a : ℕ) : ℕ := 2 ^ a
```
def defaultτ defaultτ is the inverse of a line 237 source
Source documentation
defaultτ is the inverse of a.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Inv.inv
3 instances, coercions and auxiliary constants left out.
```
@[simp] def defaultτ (a : ℕ) : ℝ := a⁻¹
…
```
def C_K The constant used twice in the definition of the Calderon-Zygmund kernel line 245 source
Source documentation
The constant used twice in the definition of the Calderon-Zygmund kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, Nat
13 instances, coercions and auxiliary constants left out.
```
@[simp] def C_K (a : ℝ) : ℝ≥0 := 2 ^ a ^ 3
```
class IsOneSidedKernel K is a one-sided Calderon-Zygmund kernel line 250 source
Source documentation
K is a one-sided Calderon-Zygmund kernel. In the formalization K x y is defined everywhere, even for x = y. The assumptions on K show that K x x = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, outParam, Nat, Complex
```
class IsOneSidedKernel (a : outParam ℕ) (K : X → X → ℂ) : Prop where
…
```
Mentions: K
class KernelProofData Standing assumptions for the kernel chapters line 261 source
Source documentation
Data common through most of chapters 2 through 7. These contain the minimal axioms for kernel-summand's proof. This is used in Chapter 3 when we don't have all other fields from ProofData.
L4DEL explanation
This class packages everything the early chapters need: a doubling measure, a parameter a with 4 at most a, compatible function distances, and a one-sided Calderon-Zygmund kernel K.
1. The fields are d (a doubling measure with doubling constant 2^a), four_le_a, cf (compatible functions), and hcz (K is a one-sided Calderon-Zygmund kernel).
2. The docstring notes these are the minimal axioms for the kernel-summand argument and are used before the full ProofData is available.
See also: MetricSpaceCarleson
Sources and attribution: Pinned Lean source (8972acdfd953)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, Nat, Complex, PseudoMetricSpace

doubling measure: a measure on a metric space for which the measure of a ball of radius 2r is bounded by a fixed constant times the measure of the ball of radius r
```
class KernelProofData {X : Type*} (a : outParam ℕ) (K : outParam (X → X → ℂ))
    [PseudoMetricSpace X] where
…
```
Mentions: K
def C1_0_2 The constant used in MetricSpaceCarleson and LinearizedMetricCarleson line 285 source
Source documentation
The constant used in MetricSpaceCarleson and LinearizedMetricCarleson. Has value 2 ^ (443 * a ^ 3) / (q - 1) ^ 6 in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
def C1_0_2 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((3 * 𝕔 + 18 + 5 * (𝕔 / 4)) * a ^ 3) / (q - 1) ^ 6
…
```
def C_Ts A constant used on the boundedness of T_Q^θ and T_* line 292 source
Source documentation
A constant used on the boundedness of T_Q^θ and T_*. We generally assume HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·) 2 2 volume volume (C_Ts a) throughout this formalization.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HPow.hPow, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
def C_Ts (a : ℕ) : ℝ≥0 := 2 ^ a ^ 3
…
```
def ClassicalCarleson Carleson's theorem (statement) line 298 source
Source documentation
Theorem 1.0.1: Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. For the proof, see classical_carleson in the file Carleson.Classical.ClassicalCarleson.
L4DEL explanation
For every continuous 2*pi-periodic complex function f, the partial Fourier sums of f converge to f at almost every point.
1. This is only a Prop (a definition of the statement); the proofs are separate theorems.
2. The quantifier is over f from the reals to the complex numbers that is continuous and periodic with period 2*pi, and the conclusion is almost-everywhere convergence along N going to infinity.
Prerequisites: partialFourierSum
See also: classical_carleson, classical_carleson_from_carleson_hunt_real
Sources and attribution: Pinned Lean source (8972acdfd953)
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Real, Complex, Continuous, Function.Periodic, HMul.hMul, OfNat.ofNat, Real.pi, Filter.Eventually, Filter.Tendsto, Nat, partialFourierSum, Filter.atTop, nhds, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume
19 instances, coercions and auxiliary constants left out.

a.e.: almost everywhere: outside a set of Lebesgue measure zero
```
def ClassicalCarleson : Prop :=
…
```
def MetricSpaceCarleson Metric space Carleson theorem (statement) line 304 source
Source documentation
Theorem 1.1.1. For the proof, see metric_carleson in the file Carleson.MetricCarleson.Main.
L4DEL explanation
In a doubling metric measure space with a Calderon-Zygmund kernel whose truncated nontangential operator is L2-bounded, the Carleson operator obeys a restricted weak-type estimate integrated over G against F.
1. Hypotheses: KernelProofData, an exponent q in (1,2] with conjugate q', measurable sets F and G, a measurable f with norm at most the indicator of F, and an L2 bound for the nontangential operator with constant C_Ts a.
2. Conclusion: the integral of carlesonOperator K f over G is at most C1_0_2 a q * vol(G)^(1/q') * vol(F)^(1/q).
3. This is a Prop; the proof is metric_carleson in MetricCarleson/Main.lean.
Prerequisites: KernelProofData, carlesonOperator, nontangentialOperator, C1_0_2
See also: metric_carleson, LinearizedMetricCarleson
Sources and attribution: Pinned Lean source (8972acdfd953)
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, IsCancellative, defaultA, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Real, Norm.norm, Set.indicator, MeasureTheory.HasBoundedStrongType and 12 more
58 instances, coercions and auxiliary constants left out.
```
def MetricSpaceCarleson : Prop :=
…
```
def LinearizedMetricCarleson Theorem 1.1.2 line 314 source
Source documentation
Theorem 1.1.2. For the proof, see linearized_metric_carleson in the file Carleson.MetricCarleson.Linearized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Norm.norm and 14 more
61 instances, coercions and auxiliary constants left out.
```
def LinearizedMetricCarleson : Prop :=
…
```