Section 10.1 and Lemma 10.0.2

def simpleNontangentialOperator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] (K : X → X → ℂ) (r : ℝ) (g : X → ℂ) (x : X) : ENNReal

The operator T_*^r g(x), defined in (10.1.31), as part of Lemma 10.1.6.

Equations

• simpleNontangentialOperator K r g x = ⨆ (R : ℝ), ⨆ (_ : R > r), ⨆ x' ∈ Metric.ball x R, ‖czOperator K R g x'‖ₑ

theorem Real.two_mul_lt_two_pow (x : ℝ) (hx : 2 ≤ x) : 2 * x ≤ 2 ^ x

theorem geom_estimate_constant_le_two : (4 * (1 - 2 ^ (-1 / 4)))⁻¹ ≤ 2

theorem real_geometric_series_estimate {x : ℝ} (hx : 4 ≤ x) : ∑' (n : ℕ), 2 ^ (-↑n / x) ≤ 2 ^ x

theorem geometric_series_estimate {x : ℝ} (hx : 4 ≤ x) : ∑' (n : ℕ), 2 ^ (-↑n / x) ≤ 2 ^ x

Lemma 10.1.1

@[irreducible]

def C10_1_2 (a : ℕ) : NNReal

The constant used in estimate_x_shift.

Equations

• C10_1_2 a = 2 ^ (a ^ 3 + 2 * a + 1)

theorem C10_1_2_def (a : ℕ) : C10_1_2 a = 2 ^ (a ^ 3 + 2 * a + 1)

theorem estimate_x_shift {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) (hr : 0 < r) (hx : dist x x' ≤ r) : ↑(nndist (czOperator K r g x) (czOperator K r g x')) ≤ ↑(C10_1_2 a) * globalMaximalFunction MeasureTheory.volume 1 g x

Lemma 10.1.2

theorem C10_1_3_def (a : ℕ) : C10_1_3 a = 2 ^ (a ^ 3 + 4 * a + 1)

@[irreducible]

def C10_1_3 (a : ℕ) : NNReal

The constant used in cotlar_control.

Equations

• C10_1_3 a = 2 ^ (a ^ 3 + 4 * a + 1)

theorem cotlar_control {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) (hr : r ∈ Set.Ioc 0 R) (hx : dist x x' ≤ R / 4) : ‖czOperator K R g x‖ₑ ≤ ‖czOperator K r ((Metric.ball x (R / 2))ᶜ.indicator g) x'‖ₑ + ↑(C10_1_3 a) * globalMaximalFunction MeasureTheory.volume 1 g x

Lemma 10.1.3

theorem C10_1_4_def (a : ℕ) : C10_1_4 a = 2 ^ (a ^ 3 + 20 * a + 2)

@[irreducible]

def C10_1_4 (a : ℕ) : NNReal

The constant used in cotlar_set_F₂.

Equations

• C10_1_4 a = 2 ^ (a ^ 3 + 20 * a + 2)

theorem cotlar_set_F₁ {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) : MeasureTheory.volume {x' : X | x' ∈ Metric.ball x (R / 4) ∧ 4 * globalMaximalFunction MeasureTheory.volume 1 (czOperator K r g) x < ‖czOperator K r g x'‖ₑ} ≤ MeasureTheory.volume (Metric.ball x (R / 4)) / 4

Part 1 of Lemma 10.1.4 about F₁.

theorem cotlar_set_F₂ {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) : MeasureTheory.volume {x' : X | x' ∈ Metric.ball x (R / 4) ∧ ↑(C10_1_4 a) * globalMaximalFunction MeasureTheory.volume 1 g x < ‖czOperator K r ((Metric.ball x (R / 2)).indicator g) x'‖ₑ} ≤ MeasureTheory.volume (Metric.ball x (R / 4)) / 4

Part 2 of Lemma 10.1.4 about F₂.

theorem C10_1_5_def (a : ℕ) : C10_1_5 a = 2 ^ (a ^ 3 + 20 * a + 2)

@[irreducible]

def C10_1_5 (a : ℕ) : NNReal

The constant used in cotlar_estimate.

Equations

• C10_1_5 a = 2 ^ (a ^ 3 + 20 * a + 2)

theorem cotlar_estimate {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) (hr : r ∈ Set.Ioc 0 R) : ‖czOperator K R g x‖ₑ ≤ 4 * globalMaximalFunction MeasureTheory.volume 1 (czOperator K r g) x + ↑(C10_1_5 a) * globalMaximalFunction MeasureTheory.volume 1 g x

Lemma 10.1.5

theorem C10_1_6_def (a : ℕ) : C10_1_6 a = 2 ^ (a ^ 3 + 24 * a + 6)

@[irreducible]

def C10_1_6 (a : ℕ) : NNReal

The constant used in simple_nontangential_operator.

Equations

• C10_1_6 a = 2 ^ (a ^ 3 + 24 * a + 6)

theorem simple_nontangential_operator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) (hr : 0 < r) : MeasureTheory.HasStrongType (simpleNontangentialOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C10_1_6 a)

Lemma 10.1.6. The formal statement includes the measurability of the operator. See also simple_nontangential_operator_le

theorem simple_nontangential_operator_le {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) (hr : 0 ≤ r) : MeasureTheory.HasStrongType (simpleNontangentialOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C10_1_6 a)

This is the first step of the proof of Lemma 10.0.2, and should follow from 10.1.6 + monotone convergence theorem. (measurability should be proven without any restriction on r.)

theorem small_annulus_right {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} {x' : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {f : X → ℂ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (h2f : MeasureTheory.volume (Function.support f) < ⊤) {R₁ : ℝ} : Continuous fun (R₂ : ℝ) => ∫ (y : X) in {y : X | dist x' y ∈ Set.Ioo R₁ R₂}, K x' y * f y

Part of Lemma 10.1.7, reformulated.

theorem small_annulus_left {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} {x' : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {f : X → ℂ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (h2f : MeasureTheory.volume (Function.support f) < ⊤) {R₂ : ℝ} : Continuous fun (R₁ : ℝ) => ∫ (y : X) in {y : X | dist x' y ∈ Set.Ioo R₁ R₂}, K x' y * f y

Part of Lemma 10.1.7, reformulated

theorem nontangential_operator_boundary {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) {f : X → ℂ} (hmf : Measurable f) (hf : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume < ⊤) (h2f : MeasureTheory.volume (Function.support f) < ⊤) : nontangentialOperator K f x = ⨆ (R₁ : ℝ), ⨆ (R₂ : ℝ), ⨆ (_ : R₁ < R₂), ⨆ (x' : X), ⨆ (_ : dist x x' ≤ R₁), ‖∫ (y : X) in Metric.ball x' R₂ \ Metric.ball x' R₁, K x' y * f y‖ₑ

Lemma 10.1.8.

theorem C10_0_2_def (a : ℕ) : C10_0_2 a = 2 ^ (3 * a ^ 3)

@[irreducible]

def C10_0_2 (a : ℕ) : NNReal

The constant used in nontangential_from_simple.

Equations

• C10_0_2 a = 2 ^ (3 * a ^ 3)

theorem nontangential_from_simple {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} [IsTwoSidedKernel a K] [CompatibleFunctions ℝ X (defaultA a)] [IsCancellative X (defaultτ a)] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume (C_Ts ↑a)) {g : X → ℂ} (hmg : Measurable g) (hg : MeasureTheory.eLpNorm g ⊤ MeasureTheory.volume < ⊤) (h2g : MeasureTheory.volume (Function.support g) < ⊤) : MeasureTheory.HasStrongType (nontangentialOperator K) 2 2 MeasureTheory.volume MeasureTheory.volume (C10_0_2 a)

Lemma 10.0.2. The formal statement includes the measurability of the operator.