noncomputable def czOperator {X : Type u_2} [PseudoMetricSpace X] [MeasureTheory.MeasureSpace X] (K : X → X → ℂ) (r : ℝ) (f : X → ℂ) (x : X) : ℂ

The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson

Equations

• czOperator K r f x = ∫ (y : X) in (Metric.ball x r)ᶜ, K x y * f y

theorem czOperator_bound {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsOneSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) (x : X) : ∃ (M : NNReal), ∀ᵐ (y : X) ∂MeasureTheory.volume.restrict (Metric.ball x r)ᶜ, ‖K x y * g y‖ ≤ ↑M

theorem czOperator_aestronglyMeasurable' {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} (hK : Measurable (Function.uncurry K)) {g : X → ℂ} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => czOperator K r g x) MeasureTheory.volume

theorem czOperator_aestronglyMeasurable {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsOneSidedKernel a K] {g : X → ℂ} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => czOperator K r g x) MeasureTheory.volume

theorem czOperator_aestronglyMeasurable_aux {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsOneSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) : MeasureTheory.AEStronglyMeasurable (fun (x : X) => czOperator K r g x) MeasureTheory.volume

theorem czOperator_welldefined {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsOneSidedKernel a K] {g : X → ℂ} (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) (x : X) : MeasureTheory.IntegrableOn (fun (y : X) => K x y * g y) (Metric.ball x r)ᶜ MeasureTheory.volume

theorem czOperator_sub {X : Type u_1} {a : ℕ} [MetricSpace X] [MeasureTheory.DoublingMeasure X ↑(defaultA a)] {r : ℝ} {K : X → X → ℂ} [IsOneSidedKernel a K] {f g : X → ℂ} (hf : BoundedFiniteSupport f MeasureTheory.volume) (hg : BoundedFiniteSupport g MeasureTheory.volume) (hr : 0 < r) : czOperator K r (f - g) = czOperator K r f - czOperator K r g

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

Lemma 10.1.1