Lemmas 7.4.4 #
@[irreducible]
The constant used in correlation_separated_trees.
Has value 2 ^ (550 * a ^ 3 - 3 * n) in the blueprint.
Instances For
theorem
TileStructure.Forest.correlation_separated_trees_of_subset
{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₁ u₂ : 𝔓 X}
{f₁ f₂ g₁ g₂ : X → ℂ}
(hu₁ : u₁ ∈ t)
(hu₂ : u₂ ∈ t)
(hu : u₁ ≠ u₂)
(h2u : 𝓘 u₁ ≤ 𝓘 u₂)
(hf₁ : Bornology.IsBounded (Set.range f₁))
(h2f₁ : HasCompactSupport f₁)
(hf₂ : Bornology.IsBounded (Set.range f₂))
(h2f₂ : HasCompactSupport f₂)
:
↑‖∫ (x : X),
adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd ℂ) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₂) g₂ x)‖₊ ≤ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal)
2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₂ g₂) x).toReal) 2
MeasureTheory.volume
theorem
TileStructure.Forest.correlation_separated_trees
{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₁ u₂ : 𝔓 X}
{f₁ f₂ g₁ g₂ : X → ℂ}
(hu₁ : u₁ ∈ t)
(hu₂ : u₂ ∈ t)
(hu : u₁ ≠ u₂)
(hf₁ : Bornology.IsBounded (Set.range f₁))
(h2f₁ : HasCompactSupport f₁)
(hf₂ : Bornology.IsBounded (Set.range f₂))
(h2f₂ : HasCompactSupport f₂)
:
↑‖∫ (x : X),
adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd ℂ) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₂) g₂ x)‖₊ ≤ ↑(C7_4_4 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal)
2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(𝓘 u₁) ∩ ↑(𝓘 u₂)).indicator (t.adjointBoundaryOperator u₂ g₂) x).toReal) 2
MeasureTheory.volume
Lemma 7.4.4.
Section 7.7 #
def
TileStructure.Forest.rowDecomp
{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)
(j : ℕ)
:
Row X n
The row-decomposition of a tree, defined in the proof of Lemma 7.7.1. The indexing is off-by-one compared to the blueprint.
Equations
- t.rowDecomp j = sorry
Instances For
@[irreducible]
The constant used in indicator_row_bound.
Has value 2 ^ (257 * a ^ 3 - n / 2) in the blueprint.
Instances For
theorem
TileStructure.Forest.row_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 j : ℕ}
{t : Forest X n}
{f : X → ℂ}
(hj : j < 2 ^ n)
(hf : MeasureTheory.BoundedCompactSupport f)
:
MeasureTheory.eLpNorm
(∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ,
adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f)
2 MeasureTheory.volume ≤ ↑(C7_7_2_1 a n) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume
Part of Lemma 7.7.2.
theorem
TileStructure.Forest.indicator_row_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 j : ℕ}
{t : Forest X n}
{u : 𝔓 X}
{f : X → ℂ}
(hj : j < 2 ^ n)
(hf : MeasureTheory.BoundedCompactSupport f)
:
MeasureTheory.eLpNorm
((∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ, F.indicator)
(adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f))
2 MeasureTheory.volume ≤ ↑(C7_7_2_2 a n) * dens₂ (⋃ u ∈ t, (fun (x : 𝔓 X) => t.𝔗 x) u) ^ 2⁻¹ * MeasureTheory.eLpNorm f 2 MeasureTheory.volume
Part of Lemma 7.7.2.
@[irreducible]
The constant used in row_correlation.
Has value 2 ^ (862 * a ^ 3 - 3 * n) in the blueprint.
Instances For
theorem
TileStructure.Forest.row_correlation
{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 j j' : ℕ}
{t : Forest X n}
{f₁ f₂ : X → ℂ}
(hjj' : j < j')
(hj' : j' < 2 ^ n)
(hf₁ : Bornology.IsBounded (Set.range f₁))
(h2f₁ : HasCompactSupport f₁)
(hf₂ : Bornology.IsBounded (Set.range f₂))
(h2f₂ : HasCompactSupport f₂)
:
↑‖∫ (x : X),
(∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j) Finset.univ,
adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₁ x) * ∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ t.rowDecomp j') Finset.univ,
adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f₂ x‖₊ ≤ ↑(C7_7_3 a n) * MeasureTheory.eLpNorm f₁ 2 MeasureTheory.volume * MeasureTheory.eLpNorm f₂ 2 MeasureTheory.volume
Lemma 7.7.3.
def
TileStructure.Forest.rowSupport
{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)
(j : ℕ)
:
Set X
The definition of Eⱼ defined above Lemma 7.7.4.
Instances For
Proposition 2.0.4 #
theorem
forest_operator
{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 : ℕ}
(𝔉 : TileStructure.Forest X n)
{f g : X → ℂ}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hg : Measurable g)
(h2g : Bornology.IsBounded (Function.support g))
:
↑‖∫ (x : X),
(starRingEnd ℂ) (g x) * ∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f x‖₊ ≤ ↑(C2_0_4 (↑a) q n) * dens₂ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume
theorem
forest_operator'
{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 : ℕ}
(𝔉 : TileStructure.Forest X n)
{f : X → ℂ}
{A : Set X}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hA : MeasurableSet A)
(h'A : Bornology.IsBounded A)
:
∫⁻ (x : X) in A,
↑‖∑ u ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ 𝔉) Finset.univ, carlesonSum ((fun (x : 𝔓 X) => 𝔉.𝔗 x) u) f x‖₊ ≤ ↑(C2_0_4 (↑a) q n) * dens₂ (⋃ u ∈ 𝔉, (fun (x : 𝔓 X) => 𝔉.𝔗 x) u) ^ (q⁻¹ - 2⁻¹) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.volume A ^ (1 / 2)
Version of the forest operator theorem, but controlling the integral of the norm instead of the integral of the function multiplied by another function.
theorem
forest_operator_le_volume
{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 : ℕ}
(𝔉 : TileStructure.Forest X n)
{f : X → ℂ}
{A : Set X}
(hf : Measurable f)
(h2f : ∀ (x : X), ‖f x‖ ≤ F.indicator 1 x)
(hA : MeasurableSet A)
(h'A : Bornology.IsBounded A)
:
Version of the forest operator theorem, but controlling the integral of the norm instead of
the integral of the function multiplied by another function, and with the upper bound in terms
of volume F and volume G.