structure TileStructure.Forest (X : Type u_1) [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (n : ℕ) : Type u_1

An n-forest

• 𝔘 : Set (𝔓 X)
• 𝔗 : 𝔓 X → Set (𝔓 X)

  The value of 𝔗 u only matters when u ∈ 𝔘.

• nonempty' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → (self.𝔗 u).Nonempty
• ordConnected' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → (self.𝔗 u).OrdConnected
• 𝓘_ne_𝓘' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → 𝓘 p ≠ 𝓘 u
• smul_four_le' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → smul 4 p ≤ smul 1 u
• stackSize_le' : ∀ {x : X}, stackSize self.𝔘 x ≤ 2 ^ n
• dens₁_𝔗_le' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → dens₁ (self.𝔗 u) ≤ 2 ^ (4 * ↑a - ↑n + 1)
• lt_dist' : ∀ {u u' : 𝔓 X}, u ∈ self.𝔘 → u' ∈ self.𝔘 → u ≠ u' → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u' → 𝓘 p ≤ 𝓘 u → 2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)
• ball_subset' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)

instance TileStructure.Forest.instCoeHeadSet𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : CoeHead (TileStructure.Forest X n) (Set (𝔓 X))

Equations

• TileStructure.Forest.instCoeHeadSet𝔓Real = { coe := TileStructure.Forest.𝔘 }

instance TileStructure.Forest.instMembership𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : Membership (𝔓 X) (TileStructure.Forest X n)

Equations

• TileStructure.Forest.instMembership𝔓Real = { mem := fun (t : TileStructure.Forest X n) (x : 𝔓 X) => x ∈ t.𝔘 }

instance TileStructure.Forest.instCoeFunForall𝔓RealSet {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : CoeFun (TileStructure.Forest X n) fun (x : TileStructure.Forest X n) => 𝔓 X → Set (𝔓 X)

Equations

• TileStructure.Forest.instCoeFunForall𝔓RealSet = { coe := fun (t : TileStructure.Forest X n) (x : 𝔓 X) => t.𝔗 x }

@[simp]

theorem TileStructure.Forest.mem_𝔘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) : u ∈ t.𝔘 ↔ u ∈ t

@[simp]

theorem TileStructure.Forest.mem_𝔗 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) : p ∈ t.𝔗 u ↔ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u

theorem TileStructure.Forest.nonempty {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) : ((fun (x : 𝔓 X) => t.𝔗 x) u).Nonempty

theorem TileStructure.Forest.ordConnected {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) : ((fun (x : 𝔓 X) => t.𝔗 x) u).OrdConnected

theorem TileStructure.Forest.𝓘_ne_𝓘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : 𝓘 p ≠ 𝓘 u

theorem TileStructure.Forest.smul_four_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : smul 4 p ≤ smul 1 u

theorem TileStructure.Forest.stackSize_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {x : X} {n : ℕ} (t : TileStructure.Forest X n) : stackSize t.𝔘 x ≤ 2 ^ n

theorem TileStructure.Forest.dens₁_𝔗_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) : dens₁ ((fun (x : 𝔓 X) => t.𝔗 x) u) ≤ 2 ^ (4 * ↑a - ↑n + 1)

theorem TileStructure.Forest.lt_dist {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u u' : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u ≠ u') {p : 𝔓 X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)

theorem TileStructure.Forest.ball_subset {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {n : ℕ} (t : TileStructure.Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)

structure TileStructure.Row (X : Type u_1) [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (n : ℕ) extends TileStructure.Forest X n : Type u_1

An n-row

• 𝔘 : Set (𝔓 X)
• 𝔗 : 𝔓 X → Set (𝔓 X)
• nonempty' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → (self.𝔗 u).Nonempty
• ordConnected' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → (self.𝔗 u).OrdConnected
• 𝓘_ne_𝓘' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → 𝓘 p ≠ 𝓘 u
• smul_four_le' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → smul 4 p ≤ smul 1 u
• stackSize_le' : ∀ {x : X}, stackSize self.𝔘 x ≤ 2 ^ n
• dens₁_𝔗_le' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → dens₁ (self.𝔗 u) ≤ 2 ^ (4 * ↑a - ↑n + 1)
• lt_dist' : ∀ {u u' : 𝔓 X}, u ∈ self.𝔘 → u' ∈ self.𝔘 → u ≠ u' → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u' → 𝓘 p ≤ 𝓘 u → 2 ^ (defaultZ a * (n + 1)) < dist (𝒬 p) (𝒬 u)
• ball_subset' : ∀ {u : 𝔓 X}, u ∈ self.𝔘 → ∀ {p : 𝔓 X}, p ∈ self.𝔗 u → Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)
• pairwiseDisjoint' : self.𝔘.PairwiseDisjoint self.𝔗

instance TileStructure.Row.instCoeHeadSet𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : CoeHead (TileStructure.Row X n) (Set (𝔓 X))

Equations

• TileStructure.Row.instCoeHeadSet𝔓Real = { coe := fun (t : TileStructure.Row X n) => t.𝔘 }

instance TileStructure.Row.instMembership𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : Membership (𝔓 X) (TileStructure.Row X n)

Equations

• TileStructure.Row.instMembership𝔓Real = { mem := fun (t : TileStructure.Row X n) (x : 𝔓 X) => x ∈ t.𝔘 }

instance TileStructure.Row.instCoeFunForall𝔓RealSet {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} : CoeFun (TileStructure.Row X n) fun (x : TileStructure.Row X n) => 𝔓 X → Set (𝔓 X)

Equations

• TileStructure.Row.instCoeFunForall𝔓RealSet = { coe := fun (t : TileStructure.Row X n) (x : 𝔓 X) => t.𝔗 x }

@[simp]

theorem TileStructure.Row.mem_𝔘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u : 𝔓 X} {n : ℕ} (t : TileStructure.Row X n) : u ∈ t.𝔘 ↔ u ∈ t

@[simp]

theorem TileStructure.Row.mem_𝔗 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {n : ℕ} (t : TileStructure.Row X n) : p ∈ t.𝔗 u ↔ p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u

theorem TileStructure.Row.pairwiseDisjoint {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {n : ℕ} (t : TileStructure.Row X n) : t.𝔘.PairwiseDisjoint fun (x : 𝔓 X) => t.𝔗 x