Section 7.2 and Lemma 7.2.1 #
@[irreducible]
The constant used in nontangential_operator_bound.
Has value 2 ^ (103 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.nontangential_operator_bound
{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)]
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(θ : Θ X)
:
MeasureTheory.eLpNorm (fun (x : X) => (TileStructure.Forest.nontangentialMaximalFunction θ f x).toReal) 2
MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume
Lemma 7.2.2.
def
TileStructure.Forest.kissing
{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 : Grid X)
:
The set of cubes in Lemma 7.2.4.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TileStructure.Forest.subset_of_kissing
{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 J : Grid X}
(h : J ∈ TileStructure.Forest.kissing I)
:
theorem
TileStructure.Forest.volume_le_of_kissing
{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 J : Grid X}
(h : J ∈ TileStructure.Forest.kissing I)
:
theorem
TileStructure.Forest.pairwiseDisjoint_of_kissing
{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 : Grid X}
:
(↑(TileStructure.Forest.kissing I)).PairwiseDisjoint fun (i : Grid X) => Metric.ball (c i) (↑(defaultD a) ^ s i / 4)
theorem
TileStructure.Forest.boundary_overlap
{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 : Grid X)
:
(TileStructure.Forest.kissing I).card ≤ 2 ^ (9 * a)
Lemma 7.2.4.
theorem
TileStructure.Forest.boundary_operator_bound
{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 : TileStructure.Forest X n}
{u : 𝔓 X}
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(hu : u ∈ t)
:
MeasureTheory.eLpNorm (fun (x : X) => (t.boundaryOperator u f x).toReal) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume
Lemma 7.2.3.
@[irreducible]
The constant used in nontangential_operator_bound.
Has value 2 ^ (104 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.tree_projection_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 : TileStructure.Forest X n}
{u : 𝔓 X}
{f g : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(hg : MeasureTheory.BoundedCompactSupport g)
(hu : u ∈ t)
:
↑‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x‖₊ ≤ ↑(TileStructure.Forest.C7_2_1 a) * MeasureTheory.eLpNorm
(TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖f x‖) 2
MeasureTheory.volume * MeasureTheory.eLpNorm
(TileStructure.Forest.approxOnCube (TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖g x‖) 2
MeasureTheory.volume
Lemma 7.2.1.