Section 5.3 #
Note: the lemmas 5.3.1-5.3.3 are in TileStructure.
Section 5.4 and Lemma 5.1.2 #
def
𝔗₁
{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)]
(k n j : ℕ)
(u : 𝔓 X)
:
The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1).
In lemmas, we will assume u ∈ 𝔘₁ k n l
Instances For
def
URel
{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)]
(k n j : ℕ)
(u u' : 𝔓 X)
:
The relation ∼ defined below (5.4.2). It is an equivalence relation on 𝔘₂ k n j.
Instances For
theorem
URel.not_disjoint
{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)]
{k n j : ℕ}
{u u' : 𝔓 X}
(hu : u ∈ 𝔘₂ k n j)
(hu' : u' ∈ 𝔘₂ k n j)
(huu' : URel k n j u u')
:
¬Disjoint (Metric.ball (𝒬 u) 100) (Metric.ball (𝒬 u') 100)
Lemma 5.4.1, part 2.
theorem
URel.eq
{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)]
{k n j : ℕ}
{u u' : 𝔓 X}
(hu : u ∈ 𝔘₂ k n j)
(hu' : u' ∈ 𝔘₂ k n j)
(huu' : URel k n j u u')
:
Lemma 5.4.1, part 1.
theorem
urel_of_not_disjoint
{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)]
{k n j : ℕ}
{x y : 𝔓 X}
(my : y ∈ 𝔘₂ k n j)
(xye : 𝓘 x = 𝓘 y)
(nd : ¬Disjoint (Metric.ball (𝒬 x) 100) (Metric.ball (𝒬 y) 100))
:
URel k n j y x
Helper for 5.4.2 that is also used in 5.4.9.
theorem
equivalenceOn_urel
{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)]
{k n j : ℕ}
:
EquivalenceOn (URel k n j) (𝔘₂ k n j)
Lemma 5.4.2.
def
𝔘₃
{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)]
(k n j : ℕ)
:
𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j,
given above (5.4.5).
Instances For
def
𝔗₂
{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)]
(k n j : ℕ)
(u : 𝔓 X)
:
The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5).
In lemmas, we will assume u ∈ 𝔘₃ k n l
Instances For
theorem
forest_geometry
{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)]
{k n j : ℕ}
{p u : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hp : p ∈ 𝔗₂ k n j u)
:
Lemma 5.4.4, verifying (2.0.32)
theorem
forest_separation
{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)]
{k n j : ℕ}
{p u u' : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hu' : u' ∈ 𝔘₃ k n j)
(huu' : u ≠ u')
(hp : p ∈ 𝔗₂ k n j u')
(h : 𝓘 p ≤ 𝓘 u)
:
Lemma 5.4.6, verifying (2.0.36)
Note: swapped u and u' to match (2.0.36)
theorem
forest_inner
{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)]
{k n j : ℕ}
{p u : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hp : p ∈ 𝔗₂ k n j u)
:
Lemma 5.4.7, verifying (2.0.37)
theorem
forest_stacking
{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)]
{k n j : ℕ}
(x : X)
(hkn : k ≤ n)
:
Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34.