theorem
TileStructure.Forest.eLpNorm_MB_le
{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 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.BoundedCompactSupport f)
:
MeasureTheory.eLpNorm (fun (x : X) => MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x) 2 MeasureTheory.volume ≤ ↑(CMB (↑(defaultA a)) 2) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume
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.
Equations
- TileStructure.Forest.C7_2_2 a = 2 ^ (103 * ↑a ^ 3)
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) => nontangentialMaximalFunction θ f x) 2 MeasureTheory.volume ≤ ↑(C7_2_2 a) * 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.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 : Forest X n}
{u : 𝔓 X}
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(hu : u ∈ t)
:
MeasureTheory.eLpNorm (t.boundaryOperator u f) 2 MeasureTheory.volume ≤ ↑(C7_2_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume
Lemma 7.2.3.
@[irreducible]
The constant used in tree_projection_estimate.
Originally had value 2 ^ (104 * a ^ 3) in the blueprint, but that seems to be a mistake.
Equations
- TileStructure.Forest.C7_2_1 a = 2 ^ (152 * ↑a ^ 3)
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 : 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‖₊ ≤ ↑(C7_2_1 a) * MeasureTheory.eLpNorm (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖f x‖) 2
MeasureTheory.volume * MeasureTheory.eLpNorm (approxOnCube (𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖g x‖) 2 MeasureTheory.volume
Lemma 7.2.1.