Section 7.1 and Lemma 7.1.3 #
def
TileStructure.Forest.σ
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
(t : Forest X n)
(u : 𝔓 X)
(x : X)
:
The definition σ(u, x) given in Section 7.1.
We may assume u ∈ t whenever proving things about this definition.
Equations
- t.σ u x = Finset.image 𝔰 (Finset.filter (fun (p : 𝔓 X) => p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u ∧ x ∈ E p) Finset.univ)
Instances For
def
TileStructure.Forest.σMax
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
(t : Forest X n)
(u : 𝔓 X)
(x : X)
(hσ : (t.σ u x).Nonempty)
:
Equations
- t.σMax u x hσ = (t.σ u x).max' hσ
Instances For
def
TileStructure.Forest.σMin
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
(t : Forest X n)
(u : 𝔓 X)
(x : X)
(hσ : (t.σ u x).Nonempty)
:
Equations
- t.σMin u x hσ = (t.σ u x).min' hσ
Instances For
def
TileStructure.Forest.𝓙₀
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2
Equations
Instances For
def
TileStructure.Forest.𝓙
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓙(𝔖), defined above Lemma 7.1.2
Equations
- TileStructure.Forest.𝓙 𝔖 = {x : Grid X | Maximal (fun (x : Grid X) => x ∈ TileStructure.Forest.𝓙₀ 𝔖) x}
Instances For
def
TileStructure.Forest.𝓛₀
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2
Equations
Instances For
def
TileStructure.Forest.𝓛
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓛(𝔖), defined above Lemma 7.1.2
Equations
- TileStructure.Forest.𝓛 𝔖 = {x : Grid X | Maximal (fun (x : Grid X) => x ∈ TileStructure.Forest.𝓛₀ 𝔖) x}
Instances For
def
TileStructure.Forest.approxOnCube
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
(f : X → E')
(x : X)
:
E'
The projection operator P_𝓒 f(x), given above Lemma 7.1.3.
In lemmas the c will be pairwise disjoint on C.
Equations
- TileStructure.Forest.approxOnCube C f x = ∑ J ∈ Finset.filter (fun (p : Grid X) => p ∈ C) Finset.univ, (↑J).indicator (fun (x : X) => ⨍ (y : X) in ↑J, f y) x
Instances For
theorem
TileStructure.Forest.stronglyMeasurable_approxOnCube
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
(f : X → E')
:
theorem
TileStructure.Forest.integrable_approxOnCube
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
{f : X → E'}
:
theorem
TileStructure.Forest.approxOnCube_nonneg
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{C : Set (Grid X)}
{f : X → ℝ}
(hf : ∀ (y : X), f y ≥ 0)
{x : X}
:
approxOnCube C f x ≥ 0
theorem
TileStructure.Forest.approxOnCube_apply
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{C : Set (Grid X)}
(hC : C.PairwiseDisjoint fun (I : Grid X) => ↑I)
(f : X → E')
{x : X}
{J : Grid X}
(hJ : J ∈ C)
(xJ : x ∈ J)
:
approxOnCube C f x = ⨍ (y : X) in ↑J, f y
theorem
TileStructure.Forest.boundedCompactSupport_approxOnCube
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{𝕜 : Type u_3}
[RCLike 𝕜]
{C : Set (Grid X)}
{f : X → 𝕜}
:
theorem
TileStructure.Forest.integral_eq_lintegral_approxOnCube
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{C : Set (Grid X)}
(hC : C.PairwiseDisjoint fun (I : Grid X) => ↑I)
{J : Grid X}
(hJ : J ∈ C)
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
:
ENNReal.ofReal (∫ (y : X) in ↑J, ‖f y‖) = ∫⁻ (y : X) in ↑J, ↑‖approxOnCube C (fun (x : X) => ↑‖f x‖) y‖₊
theorem
TileStructure.Forest.approxOnCube_ofReal
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(C : Set (Grid X))
(f : X → ℝ)
(x : X)
:
approxOnCube C (fun (x : X) => ↑(f x)) x = ↑(approxOnCube C f x)
theorem
TileStructure.Forest.norm_approxOnCube_le_approxOnCube_norm
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{C : Set (Grid X)}
{f : X → E'}
{x : X}
:
‖approxOnCube C f x‖ ≤ approxOnCube C (fun (x : X) => ‖f x‖) x
def
TileStructure.Forest.cubeOf
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(i : ℤ)
(x : X)
:
Grid X
The definition I_i(x), given above Lemma 7.1.3.
The cube of scale s that contains x. There is at most 1 such cube, if it exists.
Equations
- TileStructure.Forest.cubeOf i x = Classical.epsilon fun (I : Grid X) => x ∈ I ∧ s I = i
Instances For
def
TileStructure.Forest.nontangentialMaximalFunction
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(θ : Θ X)
(f : X → ℂ)
(x : X)
:
The definition T_𝓝^θ f(x), given in (7.1.3).
For convenience, the suprema are written a bit differently than in the blueprint
(avoiding cubeOf), but this should be equivalent.
This is 0 if x doesn't lie in a cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TileStructure.Forest.boundaryOperator
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
(t : Forest X n)
(u : 𝔓 X)
(f : X → ℂ)
(x : X)
:
The operator S_{1,𝔲} f(x), given in (7.1.4).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TileStructure.Forest.MeasureTheory.Measurable.boundaryOperator
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{f : X → ℂ}
:
Measurable (t.boundaryOperator u f)
def
TileStructure.Forest.𝓑
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
:
The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3.
Instances For
def
TileStructure.Forest.c𝓑
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(z : ℕ × Grid X)
:
X
The center function for the collection of balls 𝓑.
Equations
- TileStructure.Forest.c𝓑 z = c z.2
Instances For
def
TileStructure.Forest.r𝓑
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(z : ℕ × Grid X)
:
The radius function for the collection of balls 𝓑.
Instances For
theorem
TileStructure.Forest.convex_scales
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{x : X}
(hu : u ∈ t)
:
(↑(t.σ u x)).OrdConnected
Lemma 7.1.1, freely translated.
@[irreducible]
The constant used in first_tree_pointwise.
Has value 10 * 2 ^ (104 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.first_tree_pointwise
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{x x' : X}
{f : X → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
Lemma 7.1.4
theorem
TileStructure.Forest.second_tree_pointwise
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{x x' : X}
{f : X → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
:
↑‖∑ i ∈ t.σ u x, ∫ (y : X), Ks i x y * approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f y‖₊ ≤ nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f) x'
Lemma 7.1.5
@[irreducible]
The constant used in third_tree_pointwise.
Has value 2 ^ (151 * a ^ 3) in the blueprint.
Equations
- TileStructure.Forest.C7_1_6 a = 2 ^ (151 * ↑a ^ 3)
Instances For
theorem
TileStructure.Forest.sum_p_eq_sum_I_sum_p
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
(t : Forest X n)
(u : 𝔓 X)
(x : X)
(f : X → ℤ → NNReal)
:
theorem
TileStructure.Forest.third_tree_pointwise
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{x x' : X}
{f : X → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
Lemma 7.1.6
@[irreducible]
The constant used in pointwise_tree_estimate.
Has value 2 ^ (151 * a ^ 3) in the blueprint.
Equations
Instances For
theorem
TileStructure.Forest.pointwise_tree_estimate
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{n : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{x x' : X}
{f : X → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
↑‖carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) (fun (y : X) => Complex.exp (Complex.I * -↑((𝒬 u) y)) * f y) x‖₊ ≤ ↑(C7_1_3 a) * (MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖f x‖) x' + t.boundaryOperator u (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ↑‖f x‖) x') + nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f) x'
Lemma 7.1.3.