Section 7.3 and Lemma 7.3.1 #
@[irreducible]
The constant used in local_dens1_tree_bound.
Has value 2 ^ (101 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.local_dens1_tree_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}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ TileStructure.Forest.𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
:
Lemma 7.3.2.
@[irreducible]
The constant used in local_dens2_tree_bound.
Has value 2 ^ (200 * a ^ 3 + 19) in the blueprint.
Instances For
theorem
TileStructure.Forest.local_dens2_tree_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}
{J : Grid X}
(hJ : J ∈ TileStructure.Forest.𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u))
{q✝ : 𝔓 X}
(hq : q✝ ∈ (fun (x : 𝔓 X) => t.𝔗 x) u)
(hJq : ¬Disjoint ↑J ↑(𝓘 q✝))
:
Lemma 7.3.3.
theorem
TileStructure.Forest.C7_3_1_1_def
(a : ℕ)
:
TileStructure.Forest.C7_3_1_1 a = 2 ^ (155 * ↑a ^ 3)
@[irreducible]
The constant used in density_tree_bound1.
Has value 2 ^ (155 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.density_tree_bound1
{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_3_1_1 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
First part of Lemma 7.3.1.
theorem
TileStructure.Forest.C7_3_1_2_def
(a : ℕ)
:
TileStructure.Forest.C7_3_1_2 a = 2 ^ (256 * ↑a ^ 3)
@[irreducible]
The constant used in density_tree_bound2.
Has value 2 ^ (256 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.density_tree_bound2
{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)
(h4f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hg : MeasureTheory.BoundedCompactSupport g)
(hu : u ∈ t)
:
↑‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x‖₊ ≤ ↑(TileStructure.Forest.C7_3_1_2 a) * dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * dens₂ ((fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
Second part of Lemma 7.3.1.