theorem
integrableOn_K_mul_f
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{f : X → ℂ}
{x' : X}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
{r : ENNReal}
(hr : 0 < r)
:
MeasureTheory.IntegrableOn (fun (y : X) => K x' y * f y) (Set.EAnnulus.ci x' r) MeasureTheory.volume
theorem
TileStructure.Forest.eLpNorm_MB_le
{X : Type u_2}
{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_4}
[RCLike 𝕜]
{f : X → 𝕜}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
:
MeasureTheory.eLpNorm (maximalFunction MeasureTheory.volume 𝓑 c𝓑 r𝓑 1 f) 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 ^ (102 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.nontangential_operator_bound
{X : Type u_2}
{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 MeasureTheory.volume)
(θ : Θ X)
:
Lemma 7.2.2.
noncomputable def
TileStructure.Forest.kissing
{X : Type u_2}
{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
Instances For
theorem
TileStructure.Forest.volume_le_of_kissing
{X : Type u_2}
{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 ∈ kissing I)
:
MeasureTheory.volume (Metric.ball (c I) (33 * ↑(defaultD a) ^ s I)) ≤ 2 ^ (9 * a) * MeasureTheory.volume (Metric.ball (c J) (↑(defaultD a) ^ s J / 4))
theorem
TileStructure.Forest.pairwiseDisjoint_of_kissing
{X : Type u_2}
{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}
:
(↑(kissing I)).PairwiseDisjoint fun (i : Grid X) => Metric.ball (c i) (↑(defaultD a) ^ s i / 4)
theorem
TileStructure.Forest.e728_push_toReal
{X : Type u_2}
{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 → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume)
:
(t.boundaryOperator u f x).toReal = ∑ I : Grid X, (↑I).indicator (fun (x : X) => ∑ J ∈ t.𝓙' u (c I) (s I), (ijIntegral f I J).toReal) x
theorem
TileStructure.Forest.e728_rearrange
{X : Type u_2}
{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 MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
:
∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal = ∑ I : Grid X,
(↑(MeasureTheory.volume (Metric.ball (c I) (16 * ↑(defaultD a) ^ s I)))⁻¹.toReal * ∫ (x : X) in ↑I, (starRingEnd ℂ) (g x)) * ↑(∑ J ∈ t.𝓙' u (c I) (s I), (↑(defaultD a) ^ ((↑(s J) - ↑(s I)) / ↑a) * ∫⁻ (y : X) in ↑J, ‖f y‖ₑ).toReal)
theorem
TileStructure.Forest.e728
{X : Type u_2}
{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 MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
:
‖∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal‖ₑ ≤ ∑ J ∈ (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)).toFinset,
∫⁻ (y : X) in ↑J, ‖f y‖ₑ * maximalFunction MeasureTheory.volume 𝓑 c𝓑 r𝓑 1 g y * ∑ I : Grid X,
if ↑J ⊆ Metric.ball (c I) (16 * ↑(defaultD a) ^ s I) ∧ s J ≤ s I then ↑(defaultD a) ^ ((↑(s J) - ↑(s I)) / ↑a)
else 0
Equation (7.2.8) in the proof of Lemma 7.2.3.
theorem
TileStructure.Forest.boundary_geometric_series
{X : Type u_2}
{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)]
{J : Grid X}
:
Bound for the inner sum in Equation (7.2.8).
@[irreducible]
can be improved to 2 ^ (10 * a + 5 / 2)
Equations
- TileStructure.Forest.C7_2_3 a = 2 ^ (12 * ↑a)
Instances For
theorem
TileStructure.Forest.boundary_operator_bound_aux
{X : Type u_2}
{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 MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
:
‖∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal‖ₑ ≤ ↑(C7_2_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
theorem
TileStructure.Forest.boundary_operator_bound
{X : Type u_2}
{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 MeasureTheory.volume)
:
Lemma 7.2.3.
@[irreducible]
The constant used in tree_projection_estimate.
Has value 2 ^ (130 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.tree_projection_estimate
{X : Type u_2}
{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 MeasureTheory.volume)
(hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume)
(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.