class
IsTwoSidedKernel
{X : Type u_1}
[PseudoMetricSpace X]
[MeasureTheory.MeasureSpace X]
(a : outParam ℕ)
(K : X → X → ℂ)
extends IsOneSidedKernel a K :
K is a two-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.
Instances
Section 10.2 and Lemma 10.0.3 #
Question:
theorem
maximal_theorem
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
:
Lemma 10.2.1, formulated differently.
The blueprint version is basically this after unfolding HasBoundedWeakType, wnorm and wnorm'.
theorem
lebesgue_differentiation
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
:
∀ᵐ (x : X), ∃ (c : ℕ → X) (r : ℕ → ℝ),
Filter.Tendsto (fun (i : ℕ) => ⨍ (y : X) in Metric.ball (c i) (r i), f y) Filter.atTop (nhds (f x)) ∧ Filter.Tendsto r Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) ∧ ∀ (i : ℕ), x ∈ Metric.ball (c i) (r i)
Lemma 10.2.2.
Lemma 10.2.3 is in Mathlib: Pairwise.countable_of_isOpen_disjoint.
A point's depth in an open set O is positive iff it lies in O.
theorem
depth_eq_zero_iff_notMem
{X : Type u_1}
[MetricSpace X]
{O : Set X}
{x : X}
(hO : IsOpen O)
:
A "triangle inequality" for depths.
theorem
depth_bound_1
{X : Type u_1}
[MetricSpace X]
{O : Set X}
{x y : X}
(hO : O ≠ Set.univ)
(h : ¬Disjoint (Metric.ball x ((depth O x).toReal / 6)) (Metric.ball y ((depth O y).toReal / 6)))
:
theorem
ball_covering_bounded_intersection
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{O : Set X}
(hO : IsOpen O ∧ O ≠ Set.univ)
{U : Set X}
(countU : U.Countable)
(pdU : U.PairwiseDisjoint fun (c : X) => Metric.ball c ((depth O c).toReal / 6))
{x : X}
(mx : x ∈ O)
:
theorem
ball_covering'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{O : Set X}
(hO : IsOpen O ∧ O ≠ Set.univ)
:
Lemma 10.2.4, but following the blueprint exactly (with a countable set of centres rather than
functions from ℕ).
theorem
ball_covering_finite
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
{O : Set X}
(hO : IsOpen O ∧ O ≠ Set.univ)
{U : Set X}
{r' : X → ℝ}
(fU : U.Finite)
(pdU : U.PairwiseDisjoint fun (c : X) => Metric.ball c (r' c))
(U₃ : ⋃ c ∈ U, Metric.ball c (3 * r' c) = O)
(U₇ : ∀ c ∈ U, ¬Disjoint (Metric.ball c (7 * r' c)) Oᶜ)
(Ubi : ∀ x ∈ O, {c : X | c ∈ U ∧ x ∈ Metric.ball c (3 * r' c)}.encard ≤ ↑(2 ^ (6 * a)))
:
theorem
ball_covering
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{O : Set X}
(hO : IsOpen O ∧ O ≠ Set.univ)
:
Lemma 10.2.4.
Lemma 10.2.5 #
Lemma 10.2.5 has an annoying case distinction between the case E_α ≠ X (general case) and
E_α = X (finite case). It isn't easy to get rid of this case distinction.
In the formalization we state most properties of Lemma 10.2.5 twice, once for each case (in some cases the condition is vacuous in the finite case, and then we omit it)
We could have tried harder to uniformize the cases, but in the finite case there is really only set
B*_j, and in the general case it is convenient to index B*_j by the natural numbers.
def
GeneralCase
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
(f : X → ℂ)
(α : ENNReal)
:
The property specifying whether we are in the "general case".
Equations
- GeneralCase f α = ∃ (x : X), α ≥ globalMaximalFunction MeasureTheory.volume 1 f x
Instances For
theorem
volume_lt_of_not_GeneralCase
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(h : ¬GeneralCase f α)
(hα : 0 < α)
:
In the finite case, the volume of X is finite.
theorem
isOpen_MB_preimage_Ioi
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
:
def
czCenter
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
X
The center of B_j in the proof of Lemma 10.2.5 (general case).
Instances For
def
czRadius
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
The radius of B_j in the proof of Lemma 10.2.5 (general case).
Instances For
@[reducible, inline]
abbrev
czBall
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
Set X
The ball B_j in the proof of Lemma 10.2.5 (general case).
Equations
- czBall hX i = Metric.ball (czCenter hX i) (czRadius hX i)
Instances For
@[reducible, inline]
abbrev
czBall6
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
Set X
The ball B_j' introduced below Lemma 10.2.5 (general case).
Instances For
@[reducible, inline]
abbrev
czBall3
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
Set X
The ball B_j* in Lemma 10.2.5 (general case).
Instances For
@[reducible, inline]
abbrev
czBall7
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
Set X
The ball B_j** in the proof of Lemma 10.2.5 (general case).
Instances For
theorem
czBall_pairwiseDisjoint
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
:
Set.univ.PairwiseDisjoint fun (i : ℕ) => Metric.ball (czCenter hX i) (czRadius hX i)
theorem
iUnion_czBall3
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
:
theorem
not_disjoint_czBall7
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{i : ℕ}
(hi : 0 < czRadius hX i)
:
¬Disjoint (czBall7 hX i) (globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α)ᶜ
theorem
mem_czBall3_finite
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{y : X}
:
@[irreducible]
def
czPartition
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
:
Set X
Q_i in the proof of Lemma 10.2.5 (general case).
Equations
Instances For
theorem
czBall_subset_czPartition
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{i : ℕ}
:
theorem
czPartition_subset_czBall3
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{i : ℕ}
:
theorem
czPartition_pairwiseDisjoint
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
:
Set.univ.PairwiseDisjoint fun (i : ℕ) => czPartition hX i
theorem
czPartition_pairwiseDisjoint'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{x : X}
{i j : ℕ}
(hi : x ∈ czPartition hX i)
(hj : x ∈ czPartition hX j)
:
theorem
iUnion_czPartition
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
:
def
czApproximation
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
(f : X → ℂ)
(α : ENNReal)
(x : X)
:
The function g in Lemma 10.2.5. (both cases)
Equations
- czApproximation f α x = if hX : GeneralCase f α then if hx : ∃ (j : ℕ), x ∈ czPartition hX j then ⨍ (y : X) in czPartition hX hx.choose, f y else f x else ⨍ (y : X), f y
Instances For
theorem
czApproximation_def_of_mem
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{x : X}
{i : ℕ}
(hx : x ∈ czPartition hX i)
:
theorem
czApproximation_def_of_notMem
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{x : X}
(hX : GeneralCase f α)
(hx : x ∉ globalMaximalFunction MeasureTheory.volume 1 f ⁻¹' Set.Ioi α)
:
theorem
czApproximation_def_of_volume_lt
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{x : X}
(hX : ¬GeneralCase f α)
:
def
czRemainder'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(i : ℕ)
(x : X)
:
The function b_i in Lemma 10.2.5 (general case).
Equations
- czRemainder' hX i x = (czPartition hX i).indicator (f - czApproximation f α) x
Instances For
def
czRemainder
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
(f : X → ℂ)
(α : ENNReal)
(x : X)
:
The function b = ∑ⱼ bⱼ introduced below Lemma 10.2.5.
In the finite case, we also use this as the function b = b₁ in Lemma 10.2.5.
We choose a more convenient definition, but prove in tsum_czRemainder' that this is the same.
Equations
- czRemainder f α x = f x - czApproximation f α x
Instances For
theorem
tsum_czRemainder'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f α)
(x : X)
:
Part of Lemma 10.2.5, this is essentially (10.2.16) (both cases).
theorem
aemeasurable_czApproximation
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : AEMeasurable f MeasureTheory.volume}
:
Part of Lemma 10.2.5 (both cases).
theorem
AEMeasurable.czRemainder'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : AEMeasurable f MeasureTheory.volume}
(hX : GeneralCase f α)
(i : ℕ)
:
theorem
BoundedFiniteSupport.czApproximation
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hα : 0 < α)
(hf : BoundedFiniteSupport f MeasureTheory.volume)
:
Part of Lemma 10.2.5 (both cases).
theorem
BoundedFiniteSupport.czRemainder
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hα : 0 < α)
{hf : BoundedFiniteSupport f MeasureTheory.volume}
:
theorem
BoundedFiniteSupport.czRemainder'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hα : 0 < α)
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : GeneralCase f α)
(i : ℕ)
:
theorem
AEMeasurable.czRemainder
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hα : 0 < α)
{hf : BoundedFiniteSupport f MeasureTheory.volume}
:
theorem
czApproximation_add_czRemainder
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{x : X}
:
Part of Lemma 10.2.5, equation (10.2.16) (both cases).
This is true by definition, the work lies in tsum_czRemainder'
theorem
enorm_czApproximation_le_infinite
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : GeneralCase f α)
:
Equation (10.2.17) specialized to the general case.
theorem
enorm_czApproximation_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hα : ⨍⁻ (x : X), ‖f x‖ₑ ≤ α)
:
Part of Lemma 10.2.5, equation (10.2.17) (both cases).
theorem
eLpNorm_czApproximation_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hα : 0 < α)
:
Part of Lemma 10.2.5, equation (10.2.18) (both cases).
theorem
support_czRemainder'_subset
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{i : ℕ}
:
Part of Lemma 10.2.5, equation (10.2.19) (general case).
theorem
integral_czRemainder'
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hX : GeneralCase f α}
{i : ℕ}
:
Part of Lemma 10.2.5, equation (10.2.20) (general case).
theorem
integral_czRemainder
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : ¬GeneralCase f α)
(hα : 0 < α)
:
Part of Lemma 10.2.5, equation (10.2.20) (finite case).
theorem
eLpNorm_czRemainder'_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
{hX : GeneralCase f α}
{i : ℕ}
:
MeasureTheory.eLpNorm (czRemainder' hX i) 1 MeasureTheory.volume ≤ 2 ^ (2 * a + 1) * α * MeasureTheory.volume (czBall3 hX i)
Part of Lemma 10.2.5, equation (10.2.21) (general case).
theorem
eLpNorm_czRemainder_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : ¬GeneralCase f α)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ < α)
:
MeasureTheory.eLpNorm (czRemainder f α) 1 MeasureTheory.volume ≤ 2 ^ (2 * a + 1) * α * MeasureTheory.volume Set.univ
Part of Lemma 10.2.5, equation (10.2.21) (finite case).
theorem
tsum_volume_czBall3_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hX : GeneralCase f α)
(hα : 0 < α)
:
∑' (i : ℕ), MeasureTheory.volume (czBall3 hX i) ≤ 2 ^ (6 * a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Part of Lemma 10.2.5, equation (10.2.22) (general case).
theorem
volume_univ_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hX : ¬GeneralCase f α)
(hα : 0 < α)
:
Part of Lemma 10.2.5, equation (10.2.22) (finite case).
theorem
tsum_eLpNorm_czRemainder'_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : GeneralCase f α)
:
∑' (i : ℕ), MeasureTheory.eLpNorm (czRemainder' hX i) 1 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Part of Lemma 10.2.5, equation (10.2.23) (general case).
theorem
tsum_eLpNorm_czRemainder_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
{hf : BoundedFiniteSupport f MeasureTheory.volume}
(hX : ¬GeneralCase f α)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ < α)
:
Part of Lemma 10.2.5, equation (10.2.23) (finite case).
theorem
estimate_good
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{r : ℝ}
{K : X → X → ℂ}
[IsTwoSidedKernel a K]
{f : X → ℂ}
{α : ENNReal}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α)
(hT : MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
:
MeasureTheory.distribution (czOperator K r (czApproximation f (α'✝ a α))) (α / 2) MeasureTheory.volume ≤ ↑(C10_2_6 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Lemma 10.2.6
def
czOperatorBound
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(hX : GeneralCase f (α'✝ a α))
(x : X)
:
The function F defined in Lemma 10.2.7.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
estimate_bad_partial
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{r : ℝ}
{K : X → X → ℂ}
{x : X}
[IsTwoSidedKernel a K]
{f : X → ℂ}
{α : ENNReal}
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hr : 0 < r)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α)
(hx : x ∈ (Ω f (α'✝ a α))ᶜ)
(hX : GeneralCase f (α'✝¹ a α))
:
Lemma 10.2.7.
Note that hx implies hX, but we keep the superfluous hypothesis to shorten the statement.
theorem
czOperatorBound_inner_le
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(ha : 4 ≤ a)
(hX : GeneralCase f (α'✝ a α))
{i : ℕ}
:
theorem
distribution_czOperatorBound
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{f : X → ℂ}
{α : ENNReal}
(ha : 4 ≤ a)
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α)
(hX : GeneralCase f (α'✝ a α))
:
MeasureTheory.volume ((Ω f (α'✝¹ a α))ᶜ ∩ czOperatorBound hX ⁻¹' Set.Ioi (α / 8)) ≤ ↑(C10_2_8 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Lemma 10.2.8
theorem
estimate_bad
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{r : ℝ}
{K : X → X → ℂ}
[IsTwoSidedKernel a K]
{f : X → ℂ}
{α : ENNReal}
(ha : 4 ≤ a)
(hr : 0 < r)
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hα : ⨍⁻ (x : X), ‖f x‖ₑ / ↑(c10_0_3 a) < α)
:
MeasureTheory.distribution (czOperator K r (czRemainder f (α'✝ a α))) (α / 2) MeasureTheory.volume ≤ ↑(C10_2_9 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Lemma 10.2.9
theorem
estimate_czOperator
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{r : ℝ}
{K : X → X → ℂ}
[IsTwoSidedKernel a K]
{f : X → ℂ}
{α : ENNReal}
(ha : 4 ≤ a)
(hr : 0 < r)
(hf : BoundedFiniteSupport f MeasureTheory.volume)
(hT : MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
:
MeasureTheory.distribution (czOperator K r f) α MeasureTheory.volume ≤ ↑(C10_0_3 a) / α * MeasureTheory.eLpNorm f 1 MeasureTheory.volume
Lemma 10.0.3, blueprint form.
theorem
czOperator_weak_1_1
{X : Type u_1}
{a : ℕ}
[MetricSpace X]
[MeasureTheory.DoublingMeasure X ↑(defaultA a)]
{r : ℝ}
{K : X → X → ℂ}
[IsTwoSidedKernel a K]
(ha : 4 ≤ a)
(hr : 0 < r)
(hT : MeasureTheory.HasBoundedStrongType (czOperator K r) 2 2 MeasureTheory.volume MeasureTheory.volume ↑(C_Ts a))
:
Lemma 10.0.3, formulated differently. The blueprint version is basically this after
unfolding HasBoundedWeakType, wnorm and wnorm'.