theorem
exists_scale_add_le_of_mem_minLayer
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{A : Set (𝔓 X)}
{p : 𝔓 X}
{n : ℕ}
(hp : p ∈ A.minLayer n)
:
theorem
exists_le_add_scale_of_mem_maxLayer
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{A : Set (𝔓 X)}
{p : 𝔓 X}
{n : ℕ}
(hp : p ∈ A.maxLayer n)
:
theorem
exists_scale_add_le_of_mem_layersAbove
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{A : Set (𝔓 X)}
{p : 𝔓 X}
{n : ℕ}
(hp : p ∈ A.layersAbove n)
:
theorem
exists_le_add_scale_of_mem_layersBelow
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{A : Set (𝔓 X)}
{p : 𝔓 X}
{n : ℕ}
(hp : p ∈ A.layersBelow n)
: