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.
Equations
- TileStructure.Forest.C7_3_2 a = 2 ^ (101 * ↑a ^ 3)
Instances For
theorem
TileStructure.Forest.local_dens1_tree_bound_exists
{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}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hp₂ : ∃ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u, ¬Disjoint (↑L) (E p) ∧ 𝔰 p ≤ s L)
:
Part 1 of Lemma 7.3.2.
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 : Forest X n}
{u : 𝔓 X}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((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, but that appears to be an error.
Equations
- TileStructure.Forest.C7_3_3 a = 2 ^ (201 * ↑a ^ 3)
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 : Forest X n}
{u : 𝔓 X}
{J : Grid X}
(hu : u ∈ t)
(hJ : J ∈ 𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u))
:
MeasureTheory.volume (F ∩ ↑J) ≤ ↑(C7_3_3 a) * dens₂ ((fun (x : 𝔓 X) => t.𝔗 x) u) * MeasureTheory.volume ↑J
Lemma 7.3.3.
@[irreducible]
The constant used in density_tree_bound1.
Has value 2 ^ (155 * a ^ 3) in the blueprint, but that was based on an incorrect
version of Lemma 7.2.1.
Equations
- TileStructure.Forest.C7_3_1_1 a = 2 ^ (202.5 * ↑a ^ 3)
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 : Forest X n}
{u : 𝔓 X}
{f g : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(hg : MeasureTheory.BoundedCompactSupport g)
(h2g : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
(hu : u ∈ t)
:
↑‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x‖₊ ≤ ↑(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.
@[irreducible]
The constant used in density_tree_bound2.
Has value 2 ^ (256 * a ^ 3) in the blueprint, but that was based on an incorrect
version of Lemma 7.2.1.
Equations
- TileStructure.Forest.C7_3_1_2 a = 2 ^ (303 * ↑a ^ 3)
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 : Forest X n}
{u : 𝔓 X}
{f g : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hg : MeasureTheory.BoundedCompactSupport g)
(h2g : ∀ (x : X), ‖g x‖ ≤ G.indicator 1 x)
(hu : u ∈ t)
:
‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x‖ₑ ≤ ↑(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.