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} (hu : u ∈ self.𝔘) : (self.𝔗 u).Nonempty
• ordConnected' {u : 𝔓 X} (hu : u ∈ self.𝔘) : (self.𝔗 u).OrdConnected
• 𝓘_ne_𝓘' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) : 𝓘 p ≠ 𝓘 u
• smul_four_le' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) : smul 4 p ≤ smul 1 u
• stackSize_le' {x : X} : stackSize self.𝔘 x ≤ 2 ^ n
• dens₁_𝔗_le' {u : 𝔓 X} (hu : u ∈ self.𝔘) : dens₁ (self.𝔗 u) ≤ 2 ^ (4 * ↑a - ↑n + 1)
• lt_dist' {u u' : 𝔓 X} (hu : u ∈ self.𝔘) (hu' : u' ∈ self.𝔘) (huu' : u ≠ u') {p : 𝔓 X} (hp : p ∈ self.𝔗 u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (defaultZ a * (n + 1)) < dist_{𝔠 p ,↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) (𝒬 u)
• ball_subset' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : 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 (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) (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 (Forest X n) fun (x : 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_mk {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 : ℕ) (𝔘 : Set (𝔓 X)) (𝔗 : 𝔓 X → Set (𝔓 X)) (a✝ : ∀ {u : 𝔓 X}, u ∈ 𝔘 → (𝔗 u).Nonempty) (b : ∀ {u : 𝔓 X}, u ∈ 𝔘 → (𝔗 u).OrdConnected) (c : ∀ {u : 𝔓 X}, u ∈ 𝔘 → ∀ {p : 𝔓 X}, p ∈ 𝔗 u → 𝓘 p ≠ 𝓘 u) (d : ∀ {u : 𝔓 X}, u ∈ 𝔘 → ∀ {p : 𝔓 X}, p ∈ 𝔗 u → smul 4 p ≤ smul 1 u) (e : ∀ {x : X}, stackSize 𝔘 x ≤ 2 ^ n) (f : ∀ {u : 𝔓 X}, u ∈ 𝔘 → dens₁ (𝔗 u) ≤ 2 ^ (4 * ↑a - ↑n + 1)) (g : ∀ {u u' : 𝔓 X}, u ∈ 𝔘 → u' ∈ 𝔘 → u ≠ u' → ∀ {p : 𝔓 X}, p ∈ 𝔗 u' → 𝓘 p ≤ 𝓘 u → 2 ^ (defaultZ a * (n + 1)) < dist_{𝔠 p ,↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) (𝒬 u)) (h : ∀ {u : 𝔓 X}, u ∈ 𝔘 → ∀ {p : 𝔓 X}, p ∈ 𝔗 u → Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)) (p : 𝔓 X) : p ∈ { 𝔘 := 𝔘, 𝔗 := 𝔗, nonempty' := a✝, ordConnected' := b, 𝓘_ne_𝓘' := c, smul_four_le' := d, stackSize_le' := e, dens₁_𝔗_le' := f, lt_dist' := g, ball_subset' := h } ↔ p ∈ 𝔘

@[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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 : 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 ,↑(defaultD a) ^ 𝔰 p / 4} (𝒬 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 : Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)

theorem TileStructure.Forest.ball_subset_of_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 : Forest X n} (hu : u ∈ t) {p : 𝔓 X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) {x : X} (hx : x ∈ 𝓘 p) : Metric.ball x (4 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)

theorem TileStructure.Forest.𝓘_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 : Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : 𝓘 p ≤ 𝓘 u

theorem TileStructure.Forest.dist_lt_four {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 : Forest X n) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) : dist_{𝔠 p ,↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) (𝒬 u) < 4

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} (hu : u ∈ self.𝔘) : (self.𝔗 u).Nonempty
• ordConnected' {u : 𝔓 X} (hu : u ∈ self.𝔘) : (self.𝔗 u).OrdConnected
• 𝓘_ne_𝓘' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) : 𝓘 p ≠ 𝓘 u
• smul_four_le' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) : smul 4 p ≤ smul 1 u
• stackSize_le' {x : X} : stackSize self.𝔘 x ≤ 2 ^ n
• dens₁_𝔗_le' {u : 𝔓 X} (hu : u ∈ self.𝔘) : dens₁ (self.𝔗 u) ≤ 2 ^ (4 * ↑a - ↑n + 1)
• lt_dist' {u u' : 𝔓 X} (hu : u ∈ self.𝔘) (hu' : u' ∈ self.𝔘) (huu' : u ≠ u') {p : 𝔓 X} (hp : p ∈ self.𝔗 u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (defaultZ a * (n + 1)) < dist_{𝔠 p ,↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) (𝒬 u)
• ball_subset' {u : 𝔓 X} (hu : u ∈ self.𝔘) {p : 𝔓 X} (hp : p ∈ self.𝔗 u) : Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p) ⊆ ↑(𝓘 u)
• pairwiseDisjoint' : self.𝔘.PairwiseDisjoint fun (u : 𝔓 X) => ↑(𝓘 u)

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 (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) (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 (Row X n) fun (x : 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 : 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 : 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 : Row X n) : t.𝔘.PairwiseDisjoint fun (u : 𝔓 X) => ↑(𝓘 u)