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.

noncomputable def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂ

The Nᵗʰ partial Fourier sum of f : ℝ → ℂ for N : ℕ.

Equations

• partialFourierSum N f x = ∑ n ∈ Finset.Icc (-↑N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x

def Real.vol {X : Type u_1} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (x y : X) : ℝ

The "volume function" V. Preferably use vol instead.

Equations

• Real.vol x y = MeasureTheory.volume.real (Metric.ball x (dist x y))

def Set.Annulus.oo {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ℝ) : Set X

Equations

• Set.Annulus.oo x r R = {y : X | dist x y ∈ Set.Ioo r R}

def Set.EAnnulus.oo {X : Type u_1} [PseudoMetricSpace X] (x : X) (r R : ENNReal) : Set X

Equations

• Set.EAnnulus.oo x r R = {y : X | edist x y ∈ Set.Ioo r R}

noncomputable def iLipENorm {𝕜 : Type u_3} {X : Type u_4} [NormedField 𝕜] [PseudoMetricSpace X] (φ : X → 𝕜) (x₀ : X) (R : ℝ) : ENNReal

The inhomogeneous Lipschitz norm on a ball.

Equations

• iLipENorm φ x₀ R = (⨆ x ∈ Metric.ball x₀ R, ‖φ x‖ₑ) + ENNReal.ofReal R * ⨆ x ∈ Metric.ball x₀ R, ⨆ y ∈ Metric.ball x₀ R, ⨆ (_ : x ≠ y), ‖φ x - φ y‖ₑ / edist x y

noncomputable def localOscillation {𝕜 : Type u_3} {X : Type u_4} [RCLike 𝕜] [PseudoMetricSpace X] (E : Set X) (f g : C(X, 𝕜)) : ENNReal

The local oscillation of two functions w.r.t. a set E. This is d_E in the blueprint.

Equations

• localOscillation E f g = ⨆ z ∈ E ×ˢ E, ENNReal.ofReal ‖f z.1 - g z.1 - f z.2 + g z.2‖

structure BoundedFiniteSupport {X : Type u_3} {E : Type u_4} [MeasurableSpace X] [TopologicalSpace E] [ENorm E] [Zero E] (f : X → E) (μ : MeasureTheory.Measure X := by volume_tac) : Prop

Bounded measurable function $g$ on $X$ supported on a set of finite measure

• memLp_top : MeasureTheory.MemLp f ⊤ μ
• measure_support_lt : μ (Function.support f) < ⊤

def MeasureTheory.HasBoundedStrongType {ε₁ : Type u_3} {ε₂ : Type u_4} [ENorm ε₁] [ENorm ε₂] [TopologicalSpace ε₁] [TopologicalSpace ε₂] [Zero ε₁] {α : Type u_5} {α' : Type u_6} {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → ε₁) → α' → ε₂) (p p' : ENNReal) (μ : Measure α) (ν : Measure α') (c : ENNReal) : Prop

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.

Equations

• One or more equations did not get rendered due to their size.

class MeasureTheory.Measure.IsDoubling {X : Type u_3} [MeasurableSpace X] [PseudoMetricSpace X] (μ : Measure X) (A : outParam NNReal) : Prop

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.

• measure_ball_two_le_same (x : X) (r : ℝ) : μ (Metric.ball x (2 * r)) ≤ ↑A * μ (Metric.ball x r)

class MeasureTheory.DoublingMeasure (X : Type u_3) (A : outParam NNReal) [PseudoMetricSpace X] extends CompleteSpace X, LocallyCompactSpace X, MeasureTheory.MeasureSpace X, BorelSpace X, MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume, MeasureTheory.volume.IsDoubling A, NeZero MeasureTheory.volume : Type u_3

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.

• complete {f : Filter X} : Cauchy f → ∃ (x : X), f ≤ nhds x
• local_compact_nhds (x : X) (n : Set X) : n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
• MeasurableSet' : Set X → Prop
• measurableSet_empty : MeasurableSet' self.toMeasurableSpace ∅
• measurableSet_compl (s : Set X) : MeasurableSet' self.toMeasurableSpace s → MeasurableSet' self.toMeasurableSpace sᶜ
• measurableSet_iUnion (f : ℕ → Set X) : (∀ (i : ℕ), MeasurableSet' self.toMeasurableSpace (f i)) → MeasurableSet' self.toMeasurableSpace (⋃ (i : ℕ), f i)
• volume : Measure X
• measurable_eq : self.toMeasurableSpace = borel X
• finiteAtNhds (x : X) : volume.FiniteAtFilter (nhds x)
• measure_ball_two_le_same (x : X) (r : ℝ) : volume (Metric.ball x (2 * r)) ≤ ↑A * volume (Metric.ball x r)
• out : MeasureTheory.volume ≠ 0

class FunctionDistances (𝕜 : outParam (Type u_1)) (X : Type u) [NormedField 𝕜] [TopologicalSpace X] : Type (max (u + 1) u_1)

A class stating that continuous functions have distances associated to every ball. We use a separate type to conveniently index these functions.

• Θ : Type u

  A type of continuous functions from X to 𝕜.

• coeΘ : Θ X → C(X, 𝕜)

  The coercion map from Θ to C(X, 𝕜).

• coeΘ_injective {f g : Θ X} (h : ∀ (x : X), (coeΘ f) x = (coeΘ g) x) : f = g

  Injectivity of the coercion map from Θ to C(X, 𝕜).

• metric (_x : X) (_r : ℝ) : PseudoMetricSpace (Θ X)

  For each _x : X and _r : ℝ, a PseudoMetricSpace Θ.

@[instance_reducible]

instance instCoeΘContinuousMap {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [d : FunctionDistances 𝕜 X] : Coe (Θ X) C(X, 𝕜)

Equations

• instCoeΘContinuousMap = { coe := coeΘ }

@[instance_reducible]

instance instFunLikeΘ {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [d : FunctionDistances 𝕜 X] : FunLike (Θ X) X 𝕜

Equations

• instFunLikeΘ = { coe := fun (f : Θ X) => ⇑(coeΘ f), coe_injective := ⋯ }

def WithFunctionDistance {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [d : FunctionDistances 𝕜 X] (x : X) (r : ℝ) : Type u_2

Class used to endow Θ X with a pseudometric space structure.

Equations

• WithFunctionDistance x r = Θ X

@[instance_reducible]

instance instPseudoMetricSpaceWithFunctionDistance {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [PseudoMetricSpace X] [d : FunctionDistances 𝕜 X] {x : X} {r : ℝ} : PseudoMetricSpace (WithFunctionDistance x r)

Equations

• instPseudoMetricSpaceWithFunctionDistance = FunctionDistances.metric x r

def «termDist_{_,_}» : Lean.ParserDescr

The real-valued distance function on WithFunctionDistance x r.

Equations

• One or more equations did not get rendered due to their size.

def «termEdist_{_,_}» : Lean.ParserDescr

The ℝ≥0∞-valued distance function on WithFunctionDistance x r. Preferred over nndist.

Equations

• One or more equations did not get rendered due to their size.

class inductive CoveredByBalls {X : Type u_2} [PseudoMetricSpace X] (s : Set X) (n : ℕ) (r : ℝ) : Prop

s can be covered by at most N balls with radius r.

• mk {X : Type u_2} [PseudoMetricSpace X] {s : Set X} {n : ℕ} {r : ℝ} (balls : Finset X) (card_balls : balls.card ≤ n) (union_balls : s ⊆ ⋃ x ∈ balls, Metric.ball x r) : CoveredByBalls s n r

theorem coveredByBalls_iff {X : Type u_2} [PseudoMetricSpace X] (s : Set X) (n : ℕ) (r : ℝ) : CoveredByBalls s n r ↔ ∃ (balls : Finset X), balls.card ≤ n ∧ s ⊆ ⋃ x ∈ balls, Metric.ball x r

def BallsCoverBalls (X : Type u_2) [PseudoMetricSpace X] (r r' : ℝ) (n : ℕ) : Prop

Balls of radius r in X are covered by n balls of radius r'

Equations

• BallsCoverBalls X r r' n = ∀ (x : X), CoveredByBalls (Metric.ball x r) n r'

def AllBallsCoverBalls (X : Type u_2) [PseudoMetricSpace X] (a : ℝ) (n : ℕ) : Prop

For all r, balls of radius r in X are covered by n balls of radius a * r

Equations

• AllBallsCoverBalls X a n = ∀ (r : ℝ), BallsCoverBalls X (a * r) r n

class CompatibleFunctions (𝕜 : outParam (Type u_3)) (X : Type u) (A : outParam ℕ) [RCLike 𝕜] [PseudoMetricSpace X] extends FunctionDistances 𝕜 X : Type (max (u + 1) u_3)

A set Θ of (continuous) functions is compatible. A will usually be 2 ^ a.

• Θ : Type u
• coeΘ : Θ X → C(X, 𝕜)
• coeΘ_injective {f g : Θ X} (h : ∀ (x : X), (coeΘ f) x = (coeΘ g) x) : f = g
• metric (_x : X) (_r : ℝ) : PseudoMetricSpace (Θ X)
• eq_zero : ∃ (o : X), ∀ (f : Θ X), (coeΘ f) o = 0
• localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ X} : localOscillation (Metric.ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x, r} f g)

  The distance is bounded below by the local oscillation. (1.1.4)

• cdist_mono {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ X} (h : Metric.ball x₁ r₁ ⊆ Metric.ball x₂ r₂) : dist_{x₁, r₁} f g ≤ dist_{x₂, r₂} f g

  The distance is monotone in the ball. (1.1.6)

• cdist_le {x₁ x₂ : X} {r : ℝ} {f g : Θ X} (h : dist x₁ x₂ < 2 * r) : dist_{x₂, 2 * r} f g ≤ ↑A * dist_{x₁, r} f g

  The distance of a ball with large radius is bounded above. (1.1.5)

• le_cdist {x₁ x₂ : X} {r : ℝ} {f g : Θ X} (h1 : Metric.ball x₁ r ⊆ Metric.ball x₂ (↑A * r)) : 2 * dist_{x₁, r} f g ≤ dist_{x₂, ↑A * r} f g

  The distance of a ball with large radius is bounded below. (1.1.7)

• allBallsCoverBalls {x : X} {r : ℝ} : AllBallsCoverBalls (WithFunctionDistance x r) 2 A

  Every ball of radius 2R can be covered by A balls of radius R. (1.1.8)

class IsCancellative (X : Type u_2) {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop

Θ is τ-cancellative. τ will usually be 1 / a

• enorm_integral_exp_le' {x : X} {r : ℝ} {φ : X → ℂ} (hr : 0 < r) (h1 : iLipENorm φ x r ≠ ⊤) (h2 : Function.support φ ⊆ Metric.ball x r) {f g : Θ X} : ‖∫ (x : X), Complex.exp (Complex.I * (↑(f x) - ↑(g x))) * φ x‖ₑ ≤ ↑A * MeasureTheory.volume (Metric.ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (-τ)

noncomputable def upperRadius {X : Type u_2} [PseudoMetricSpace X] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ENNReal

R_Q(θ, x) defined in (1.1.17).

Equations

• upperRadius Q θ x = ⨆ (r : ℝ), ⨆ (_ : dist_{x, r} θ (Q x) < 1), ENNReal.ofReal r

noncomputable def linearizedNontangentialOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The linearized maximally truncated nontangential Calderon–Zygmund operator T_Q^θ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def nontangentialOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The maximally truncated nontangential Calderon–Zygmund operator T_*.

Equations

• nontangentialOperator K f x = ⨆ (R₂ : ℝ), ⨆ R₁ ∈ Set.Ioo 0 R₂, ⨆ x' ∈ Metric.ball x R₁, ‖∫ (y : X) in Set.Annulus.oo x' R₁ R₂, K x' y * f y‖ₑ

noncomputable def carlesonOperatorIntegrand {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (K : X → X → ℂ) (θ : Θ X) (R₁ R₂ : ℝ) (f : X → ℂ) (x : X) : ℂ

The integrand in the (linearized) Carleson operator. This is G in Lemma 3.0.1.

Equations

• carlesonOperatorIntegrand K θ R₁ R₂ f x = ∫ (y : X) in Set.Annulus.oo x R₁ R₂, K x y * f y * Complex.exp (Complex.I * ↑(θ y))

noncomputable def linearizedCarlesonOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (Q : X → Θ X) (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The linearized generalized Carleson operator T_Q, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.

Equations

• linearizedCarlesonOperator Q K f x = ⨆ (R₁ : ℝ), ⨆ (R₂ : ℝ), ⨆ (_ : 0 < R₁), ⨆ (_ : R₁ < R₂), ‖carlesonOperatorIntegrand K (Q x) R₁ R₂ f x‖ₑ

noncomputable def carlesonOperator {X : Type u_2} {A : ℕ} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X ↑A] [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ENNReal

The generalized Carleson operator T, taking values in ℝ≥0∞. Use ENNReal.toReal to get the corresponding real number.

Equations

• carlesonOperator K f x = ⨆ (θ : Θ X), linearizedCarlesonOperator (fun (x : X) => θ) K f x

@[reducible, inline]

abbrev defaultA (a : ℕ) : ℕ

This is usually the value of the argument A in DoublingMeasure and CompatibleFunctions

Equations

• defaultA a = 2 ^ a

noncomputable def defaultτ (a : ℕ) : ℝ

defaultτ is the inverse of a.

Equations

• defaultτ a = (↑a)⁻¹

noncomputable def C_K (a : ℝ) : NNReal

The constant used twice in the definition of the Calderon-Zygmund kernel.

Equations

• C_K a = 2 ^ a ^ 3

class IsOneSidedKernel {X : Type u_1} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (a : outParam ℕ) (K : X → X → ℂ) : Prop

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.

• measurable_K : Measurable (Function.uncurry K)
• norm_K_le_vol_inv (x y : X) : ‖K x y‖ ≤ ↑(C_K ↑a) / Real.vol x y
• norm_K_sub_le {x y y' : X} (h : 2 * dist y y' ≤ dist x y) : ‖K x y - K x y'‖ ≤ (dist y y' / dist x y) ^ (↑a)⁻¹ * (↑(C_K ↑a) / Real.vol x y)

class KernelProofData {X : Type u_1} (a : outParam ℕ) (K : outParam (X → X → ℂ)) [PseudoMetricSpace X] : Type (u_1 + 1)

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.

• d : MeasureTheory.DoublingMeasure X ↑(defaultA a)
• four_le_a : 4 ≤ a
• cf : CompatibleFunctions ℝ X (defaultA a)
• hcz : IsOneSidedKernel a K

theorem 𝕔_def : 𝕔 = 100

@[irreducible]

def 𝕔 : ℕ

The main constant in the blueprint, driving all the construction, is D = 2 ^ (100 * a ^ 2). It turns out that the proof is robust, and works for other values of 100, giving better constants in the end. We will formalize it using a parameter 𝕔 (that we fix equal to 100 to follow the blueprint) and having D = 2 ^ (𝕔 * a ^ 2). We register two lemmas seven_le_c and c_le_100 and will never unfold 𝕔 from this point on.

Equations

• 𝕔 = 100

noncomputable def C1_0_2 (a : ℕ) (q : NNReal) : NNReal

The constant used in MetricSpaceCarleson and LinearizedMetricCarleson. Has value 2 ^ (443 * a ^ 3) / (q - 1) ^ 6 in the blueprint.

Equations

• C1_0_2 a q = 2 ^ ((3 * 𝕔 + 18 + 5 * (𝕔 / 4)) * a ^ 3) / (q - 1) ^ 6

def C_Ts (a : ℕ) : NNReal

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.

Equations

• C_Ts a = 2 ^ a ^ 3

def ClassicalCarleson : Prop

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.

Equations

• One or more equations did not get rendered due to their size.

def MetricSpaceCarleson : Prop

Theorem 1.1.1. For the proof, see metric_carleson in the file Carleson.MetricCarleson.Main.

Equations

• One or more equations did not get rendered due to their size.

def LinearizedMetricCarleson : Prop

Theorem 1.1.2. For the proof, see linearized_metric_carleson in the file Carleson.MetricCarleson.Linearized.

Equations

• One or more equations did not get rendered due to their size.