Section 7.6 and Lemma 7.4.6 #
def
TileStructure.Forest.πβ
{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)
:
The definition π' at the start of Section 7.6.
We use a different notation to distinguish it from the π' used in Section 7.5
Equations
Instances For
theorem
TileStructure.Forest.union_πβ
{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}
(huβ : uβ β t)
:
Part of Lemma 7.6.1.
theorem
TileStructure.Forest.pairwiseDisjoint_πβ
{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}
(huβ : uβ β t)
:
(t.πβ uβ).PairwiseDisjoint fun (I : Grid X) => βI
Part of Lemma 7.6.1.
@[irreducible]
The constant used in thin_scale_impact. This is denoted sβ in the proof of Lemma 7.6.3.
Has value Z * n / (202 * a ^ 3) - 2 in the blueprint.
Instances For
theorem
TileStructure.Forest.C7_6_3_pos
{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 : β}
[ProofData a q K Οβ Οβ F G]
(h : 1 β€ n)
:
0 < TileStructure.Forest.C7_6_3 a n
theorem
TileStructure.Forest.thin_scale_impact
{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β uβ p : π X}
{J : Grid X}
(huβ : uβ β t)
(huβ : uβ β t)
(hu : uβ β uβ)
(h2u : π uβ β€ π uβ)
(hp : p β (fun (x : π X) => t.π x) uβ \ t.πβ uβ uβ)
(hJ : J β t.πβ uβ)
(h : Β¬Disjoint (Metric.ball (π p) (8 * β(defaultD a) ^ π° p)) (Metric.ball (c J) (8 * β(defaultD a) ^ s J)))
:
β(π° p) β€ β(s J) - TileStructure.Forest.C7_6_3 a n
Lemma 7.6.3.
theorem
TileStructure.Forest.square_function_count
{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 β t.πβ uβ)
(s' : β€)
:
β¨β» (x : X) in βJ,
(β
I β
Finset.filter
(fun (I : Grid X) =>
s I = s J - s' β§ Disjoint βI β(π uβ) β§ Β¬Disjoint (βJ) (Metric.ball (c I) (8 * β(defaultD a) ^ s I)))
Finset.univ,
(Metric.ball (c I) (8 * β(defaultD a) ^ s I)).indicator 1 x) ^ 2 βMeasureTheory.volume β€ β(TileStructure.Forest.C7_6_4 a s')
Lemma 7.6.4.
@[irreducible]
The constant used in bound_for_tree_projection.
Has value 2 ^ (118 * a ^ 3 - 100 / (202 * a) * Z * n * ΞΊ) in the blueprint.
Instances For
theorem
TileStructure.Forest.bound_for_tree_projection
{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β uβ : π X}
{f : X β β}
(huβ : uβ β t)
(huβ : uβ β t)
(hu : uβ β uβ)
(h2u : π uβ β€ π uβ)
(hf : Bornology.IsBounded (Set.range f))
(h2f : HasCompactSupport f)
(h3f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
:
MeasureTheory.eLpNorm
(TileStructure.Forest.approxOnCube (t.πβ uβ) fun (x : X) =>
βTileStructure.Forest.adjointCarlesonSum ((fun (x : π X) => t.π x) uβ \ t.πβ uβ uβ) f xβ)
2 MeasureTheory.volume β€ β(TileStructure.Forest.C7_6_2 a n) * MeasureTheory.eLpNorm
((β(π uβ)).indicator fun (x : X) =>
(MB MeasureTheory.volume TileStructure.Forest.π TileStructure.Forest.cπ TileStructure.Forest.rπ
(fun (x : X) => βf xβ) x).toReal)
2 MeasureTheory.volume
Lemma 7.6.2. Todo: add needed hypothesis to LaTeX
@[irreducible]
The constant used in correlation_near_tree_parts.
Has value 2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3)) in the blueprint.
Instances For
theorem
TileStructure.Forest.correlation_near_tree_parts
{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β 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),
TileStructure.Forest.adjointCarlesonSum ((fun (x : π X) => t.π x) uβ) gβ x * (starRingEnd β) (TileStructure.Forest.adjointCarlesonSum ((fun (x : π X) => t.π x) uβ \ t.πβ uβ uβ) gβ x)ββ β€ β(TileStructure.Forest.C7_4_6 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((β(π uβ)).indicator (t.adjointBoundaryOperator uβ gβ) x).toReal) 2
MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((β(π uβ)).indicator (t.adjointBoundaryOperator uβ gβ) x).toReal) 2
MeasureTheory.volume
Lemma 7.4.6