Section 10.1 and Lemma 10.0.2

noncomputable 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), above Lemma 10.1.6.

Equations

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

@[irreducible]

def C10_1_2 (a : ℕ) : NNReal

The constant used in estimate_x_shift.

Equations

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

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

theorem estimate_10_1_2 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {x : X} [IsTwoSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) : ∫⁻ (y : X) in (Metric.ball x r)ᶜ ∩ Metric.ball x (2 * r), ‖K x y * g y‖ₑ ≤ 2 ^ (a ^ 3 + a) * globalMaximalFunction MeasureTheory.volume 1 g x

theorem estimate_10_1_3 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] (ha : 4 ≤ a) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) (hx : dist x x' ≤ r) : ‖∫ (y : X) in (Metric.ball x (2 * r))ᶜ, K x y * g y - K x' y * g y‖ₑ ≤ 2 ^ (a ^ 3 + 2 * a) * globalMaximalFunction MeasureTheory.volume 1 g x

theorem estimate_10_1_4 {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) (hx : dist x x' ≤ r) : ∫⁻ (y : X) in (Metric.ball x' r)ᶜ ∩ Metric.ball x (2 * r), ‖K x' y * g y‖ₑ ≤ 2 ^ (a ^ 3 + 2 * a) * globalMaximalFunction MeasureTheory.volume 1 g x

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] (ha : 4 ≤ a) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) (hx : dist x x' ≤ r) : edist (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 radius_change {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x x' : X} [IsTwoSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : r ∈ Set.Ioc 0 R) (hx : dist x x' ≤ R / 4) : ‖czOperator K r ((Metric.ball x (R / 2))ᶜ.indicator g) x' - czOperator K R ((Metric.ball x (R / 2))ᶜ.indicator g) x'‖ₑ ≤ 2 ^ (a ^ 3 + 4 * a) * globalMaximalFunction MeasureTheory.volume 1 g x

theorem cut_out_ball {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r R : ℝ} {K : X → X → ℂ} {x x' : X} {g : X → ℂ} (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'

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] (ha : 4 ≤ a) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (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 globalMaximalFunction_zero_enorm_ae_zero {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {R : ℝ} {x : X} (hR : 0 < R) {f : X → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hMzero : globalMaximalFunction MeasureTheory.volume 1 f x = 0) : ∀ᵐ (x' : X) ∂MeasureTheory.volume.restrict (Metric.ball x R), ‖f x'‖ₑ = 0

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] (hr : 0 < r) (hR : r ≤ R) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) : (MeasureTheory.volume.restrict (Metric.ball x (R / 4))) {x' : X | 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] (ha : 4 ≤ a) (hr : 0 < r) (hR : r ≤ R) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) : (MeasureTheory.volume.restrict (Metric.ball x (R / 4))) {x' : X | ↑(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 + 3)

@[irreducible]

def C10_1_5 (a : ℕ) : NNReal

The constant used in cotlar_estimate.

Equations

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

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] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (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 lowerSemicontinuous_simpleNontangentialOperator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {g : X → ℂ} : LowerSemicontinuous (simpleNontangentialOperator K r g)

Part of Lemma 10.1.6.

theorem aestronglyMeasurable_simpleNontangentialOperator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} {g : X → ℂ} : MeasureTheory.AEStronglyMeasurable (simpleNontangentialOperator K r g) MeasureTheory.volume

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. It is not tight and can be improved by some a + constant.

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] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) (hr : 0 < r) : MeasureTheory.HasBoundedStrongType (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] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) (hr : 0 ≤ r) : MeasureTheory.HasBoundedStrongType (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] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) : ContinuousWithinAt (fun (R₂ : ℝ) => ∫ (y : X) in Set.Annulus.oo x R₁ R₂, K x y * g y) (Set.Ioo R₁ R₂) R₁

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] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) {R₁ R₂ : ℝ} (hR₁ : 0 ≤ R₁) : ContinuousWithinAt (fun (R : ℝ) => ∫ (y : X) in Set.Annulus.oo x R R₂, K x y * g y) (Set.Ioo R₁ R₂) R₂

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] {f : X → ℂ} (hf : BoundedFiniteSupport f MeasureTheory.volume) : nontangentialOperator K f x = ⨆ (R₂ : ℝ), ⨆ R₁ ∈ Set.Ioo 0 R₂, ⨆ x' ∈ Metric.ball x R₁, ‖∫ (y : X) in Metric.ball x' R₂ \ Metric.ball x' R₁, K x' y * f y‖ₑ

Lemma 10.1.8.

theorem lowerSemicontinuous_nontangentialOperator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} {g : X → ℂ} : LowerSemicontinuous (nontangentialOperator K g)

Part of Lemma 10.1.6.

theorem aestronglyMeasurable_nontangentialOperator {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {K : X → X → ℂ} {g : X → ℂ} : MeasureTheory.AEStronglyMeasurable (nontangentialOperator K g) MeasureTheory.volume

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] (ha : 4 ≤ a) (hT : ∀ r > 0, MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a)) : MeasureTheory.HasBoundedStrongType (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.