class PreTileStructure {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : outParam NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances 𝕜 X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam ℕ) (κ : outParam ℝ) (S : outParam ℕ) (o : outParam X) extends GridStructure X D κ S o : Type (max (u + 1) (u_2 + 1))

• Grid : Type u_2
• fintype_Grid : Fintype (GridStructure.Grid X)
• coeGrid : GridStructure.Grid X → Set X
• s : GridStructure.Grid X → ℤ
• c : GridStructure.Grid X → X
• inj : Function.Injective fun (i : GridStructure.Grid X) => (↑i, s i)
• range_s_subset : Set.range s ⊆ Set.Icc (-↑S) ↑S
• topCube : GridStructure.Grid X
• s_topCube : s topCube = ↑S
• c_topCube : c topCube = o
• subset_topCube {i : GridStructure.Grid X} : ↑i ⊆ ↑topCube
• Grid_subset_biUnion {i : GridStructure.Grid X} (k : ℤ) : k ∈ Set.Ico (-↑S) (s i) → ↑i ⊆ ⋃ j ∈ s ⁻¹' {k}, ↑j
• fundamental_dyadic' {i j : GridStructure.Grid X} : s i ≤ s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
• ball_subset_Grid {i : GridStructure.Grid X} : Metric.ball (c i) (↑D ^ s i / 4) ⊆ ↑i
• Grid_subset_ball {i : GridStructure.Grid X} : ↑i ⊆ Metric.ball (c i) (4 * ↑D ^ s i)
• small_boundary {i : GridStructure.Grid X} {t : NNReal} (ht : ↑D ^ (-↑S - s i) ≤ t) : MeasureTheory.volume.real {x : X | x ∈ ↑i ∧ EMetric.infEdist x (↑i)ᶜ ≤ ↑t * ↑D ^ s i} ≤ 2 * ↑t ^ κ * MeasureTheory.volume.real ↑i
• coeGrid_measurable {i : GridStructure.Grid X} : MeasurableSet ↑i
• 𝔓 : Type u
• fintype_𝔓 : Fintype (PreTileStructure.𝔓 𝕜 X)
• 𝓘 : PreTileStructure.𝔓 𝕜 X → GridStructure.Grid X
• surjective_𝓘 : Function.Surjective PreTileStructure.𝓘
• 𝒬 : PreTileStructure.𝔓 𝕜 X → Θ X
• range_𝒬 : Set.range 𝒬 ⊆ Set.range ⇑Q

def 𝔓 {𝕜 : Type u_1} [RCLike 𝕜] (X : Type u) {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] : Type u

Equations

• 𝔓 X = PreTileStructure.𝔓 𝕜 X

instance instFintype𝔓 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] : Fintype (𝔓 X)

Equations

• instFintype𝔓 = PreTileStructure.fintype_𝔓

def 𝓘 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] : 𝔓 X → Grid X

Equations

• 𝓘 = PreTileStructure.𝓘

theorem surjective_𝓘 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] : Function.Surjective 𝓘

instance instInhabited𝔓 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] : Inhabited (𝔓 X)

Equations

• instInhabited𝔓 = { default := ⋯.choose }

def 𝔠 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] (p : 𝔓 X) : X

Equations

• 𝔠 p = c (𝓘 p)

def 𝔰 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] (p : 𝔓 X) : ℤ

Equations

• 𝔰 p = s (𝓘 p)

class TileStructure {X : Type u} {A : outParam NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam ℕ) (κ : outParam ℝ) (S : outParam ℕ) (o : outParam X) extends PreTileStructure Q D κ S o : Type (u + 1)

A tile structure.

• Grid : Type u
• fintype_Grid : Fintype (GridStructure.Grid X)
• coeGrid : GridStructure.Grid X → Set X
• s : GridStructure.Grid X → ℤ
• c : GridStructure.Grid X → X
• inj : Function.Injective fun (i : GridStructure.Grid X) => (↑i, s i)
• range_s_subset : Set.range s ⊆ Set.Icc (-↑S) ↑S
• topCube : GridStructure.Grid X
• s_topCube : s topCube = ↑S
• c_topCube : c topCube = o
• subset_topCube {i : GridStructure.Grid X} : ↑i ⊆ ↑topCube
• Grid_subset_biUnion {i : GridStructure.Grid X} (k : ℤ) : k ∈ Set.Ico (-↑S) (s i) → ↑i ⊆ ⋃ j ∈ s ⁻¹' {k}, ↑j
• fundamental_dyadic' {i j : GridStructure.Grid X} : s i ≤ s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
• ball_subset_Grid {i : GridStructure.Grid X} : Metric.ball (c i) (↑D ^ s i / 4) ⊆ ↑i
• Grid_subset_ball {i : GridStructure.Grid X} : ↑i ⊆ Metric.ball (c i) (4 * ↑D ^ s i)
• small_boundary {i : GridStructure.Grid X} {t : NNReal} (ht : ↑D ^ (-↑S - s i) ≤ t) : MeasureTheory.volume.real {x : X | x ∈ ↑i ∧ EMetric.infEdist x (↑i)ᶜ ≤ ↑t * ↑D ^ s i} ≤ 2 * ↑t ^ κ * MeasureTheory.volume.real ↑i
• coeGrid_measurable {i : GridStructure.Grid X} : MeasurableSet ↑i
• 𝔓 : Type u
• fintype_𝔓 : Fintype (PreTileStructure.𝔓 ℝ X)
• 𝓘 : PreTileStructure.𝔓 ℝ X → GridStructure.Grid X
• surjective_𝓘 : Function.Surjective PreTileStructure.𝓘
• 𝒬 : PreTileStructure.𝔓 ℝ X → Θ X
• range_𝒬 : Set.range 𝒬 ⊆ Set.range ⇑Q
• Ω : PreTileStructure.𝔓 ℝ X → Set (Θ X)
• biUnion_Ω {i : GridStructure.Grid X} : Set.range ⇑Q ⊆ ⋃ p ∈ PreTileStructure.𝓘 ⁻¹' {i}, Ω p
• disjoint_Ω {p p' : PreTileStructure.𝔓 ℝ X} (h : p ≠ p') (hp : PreTileStructure.𝓘 p = PreTileStructure.𝓘 p') : Disjoint (Ω p) (Ω p')
• relative_fundamental_dyadic {p p' : PreTileStructure.𝔓 ℝ X} (h : PreTileStructure.𝓘 p ≤ PreTileStructure.𝓘 p') : Disjoint (Ω p) (Ω p') ∨ Ω p' ⊆ Ω p
• cball_subset {p : 𝔓 X} : ball_{𝔠 p, ↑D ^ 𝔰 p / 4} (𝒬 p) 5⁻¹ ⊆ Ω p
• subset_cball {p : 𝔓 X} : Ω p ⊆ ball_{𝔠 p, ↑D ^ 𝔰 p / 4} (𝒬 p) 1

def «termDist_(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «termNndist_(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «termEdist_(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def «termBall_(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem 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)] {f g : Θ X} (p : 𝔓 X) : dist_{c (𝓘 p), ↑(defaultD a) ^ s (𝓘 p) / 4} f g = dist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} f g

@[simp]

theorem nndist_𝓘 {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)] {f g : Θ X} (p : 𝔓 X) : nndist_{c (𝓘 p), ↑(defaultD a) ^ s (𝓘 p) / 4} f g = nndist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} f g

@[simp]

theorem ball_𝓘 {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)] {f : Θ X} (p : 𝔓 X) {r : ℝ} : ball_{c (𝓘 p), ↑(defaultD a) ^ s (𝓘 p) / 4} f r = ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} f r

@[simp]

theorem cball_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)] {p : 𝔓 X} : ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) 5⁻¹ ⊆ Ω p

@[simp]

theorem subset_cball {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)] {p : 𝔓 X} : Ω p ⊆ ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) 1

theorem ball_eq_of_grid_eq {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)] {p q✝ : 𝔓 X} {ϑ : Θ X} {r : ℝ} (h : 𝓘 p = 𝓘 q✝) : ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} ϑ r = ball_{𝔠 q✝, ↑(defaultD a) ^ 𝔰 q✝ / 4} ϑ r

theorem cball_disjoint {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)] {p p' : 𝔓 X} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') : Disjoint (ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) 5⁻¹) (ball_{𝔠 p', ↑(defaultD a) ^ 𝔰 p' / 4} (𝒬 p') 5⁻¹)

theorem volume_xDsp_bound {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)] {p : 𝔓 X} {x : X} (hx : x ∈ 𝓘 p) : MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (3 * a) ≤ MeasureTheory.volume (Metric.ball x (↑(defaultD a) ^ 𝔰 p))

A bound used in both nontrivial cases of Lemma 7.5.5.

theorem volume_xDsp_bound_4 {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)] {p : 𝔓 X} {x : X} (hx : x ∈ 𝓘 p) : MeasureTheory.volume (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (4 * a) ≤ MeasureTheory.volume (Metric.ball x (↑(defaultD a) ^ 𝔰 p))

A bound used in Lemma 7.6.2.

def E {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)] (p : 𝔓 X) : Set X

The set E defined in Proposition 2.0.2.

Equations

• E p = {x : X | x ∈ 𝓘 p ∧ Q x ∈ Ω p ∧ 𝔰 p ∈ Set.Icc (σ₁ x) (σ₂ x)}

theorem E_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)] {p : 𝔓 X} : E p ⊆ ↑(𝓘 p)

theorem Q_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)] {p : 𝔓 X} {x : X} (hp : x ∈ E p) : Q x ∈ Ω p

theorem disjoint_E {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)] {p p' : 𝔓 X} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') : Disjoint (E p) (E p')

theorem measurableSet_E {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)] {p : 𝔓 X} : MeasurableSet (E p)

theorem volume_E_lt_top {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)] {p : 𝔓 X} : MeasureTheory.volume (E p) < ⊤

def TileLike (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)] : Type u_1

Equations

• TileLike X = (Grid X × (Set (Θ X))ᵒᵈ)

def TileLike.fst {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 : TileLike X) : Grid X

Equations

• x.fst = x.1

def TileLike.snd {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 : TileLike X) : Set (Θ X)

Equations

• x.snd = x.2

@[simp]

theorem TileLike.fst_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)] (x : Grid X) (y : Set (Θ X)) : fst (x, y) = x

@[simp]

theorem TileLike.snd_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)] (x : Grid X) (y : Set (Θ X)) : snd (x, y) = y

instance instPartialOrderTileLike {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)] : PartialOrder (TileLike X)

Equations

• instPartialOrderTileLike = id inferInstance

theorem TileLike.le_def {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 y : TileLike X) : x ≤ y ↔ x.fst ≤ y.fst ∧ y.snd ⊆ x.snd

def toTileLike {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)] (p : 𝔓 X) : TileLike X

Equations

• toTileLike p = (𝓘 p, Ω p)

@[simp]

theorem toTileLike_fst {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)] (p : 𝔓 X) : (toTileLike p).fst = 𝓘 p

@[simp]

theorem toTileLike_snd {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)] (p : 𝔓 X) : (toTileLike p).snd = Ω p

def smul {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)] (l : ℝ) (p : 𝔓 X) : TileLike X

This is not defined as such in the blueprint, but λp ≲ λ'p' can be written using smul l p ≤ smul l' p'. Beware: smul 1 p is very different from toTileLike p.

Equations

• smul l p = (𝓘 p, ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) l)

@[simp]

theorem smul_fst {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)] (l : ℝ) (p : 𝔓 X) : (smul l p).fst = 𝓘 p

@[simp]

theorem smul_snd {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)] (l : ℝ) (p : 𝔓 X) : (smul l p).snd = ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) l

theorem smul_mono_left {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)] {l l' : ℝ} {p : 𝔓 X} (h : l ≤ l') : smul l' p ≤ smul l p

theorem smul_le_toTileLike {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)] {p : 𝔓 X} : smul 1 p ≤ toTileLike p

theorem toTileLike_le_smul {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)] {p : 𝔓 X} : toTileLike p ≤ smul 5⁻¹ p

theorem 𝒬_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)] {p : 𝔓 X} : 𝒬 p ∈ Ω p

theorem 𝒬_inj {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)] {p p' : 𝔓 X} (h : 𝒬 p = 𝒬 p') (h𝓘 : 𝓘 p = 𝓘 p') : p = p'

theorem toTileLike_injective {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)] : Function.Injective fun (p : 𝔓 X) => toTileLike p

instance instPartialOrder𝔓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)] : PartialOrder (𝔓 X)

Equations

• instPartialOrder𝔓Real = PartialOrder.lift toTileLike ⋯

theorem 𝔓.le_def {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)] {p q✝ : 𝔓 X} : p ≤ q✝ ↔ toTileLike p ≤ toTileLike q✝

theorem 𝔓.le_def' {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)] {p q✝ : 𝔓 X} : p ≤ q✝ ↔ 𝓘 p ≤ 𝓘 q✝ ∧ Ω q✝ ⊆ Ω p

theorem tile_le_of_cube_le_and_not_disjoint {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)] {p q✝ : 𝔓 X} (hi : 𝓘 p ≤ 𝓘 q✝) {x : Θ X} (mxp : x ∈ Ω p) (mxq : x ∈ Ω q✝) : p ≤ q✝

Deduce an inclusion of tiles from an inclusion of their cubes and non-disjointness of their Ωs.

theorem dist_𝒬_lt_one_of_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)] {p q✝ : 𝔓 X} (h : p ≤ q✝) : dist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 q✝) (𝒬 p) < 1

theorem dist_𝒬_lt_one_of_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)] {p q✝ : 𝔓 X} (h : p ≤ q✝) : dist_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) (𝒬 q✝) < 1

theorem 𝓘_strictMono {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)] : StrictMono 𝓘

theorem smul_mono {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)] {p p' : 𝔓 X} {m m' n n' : ℝ} (hp : smul n p ≤ smul m p') (hm : m' ≤ m) (hn : n ≤ n') : smul n' p ≤ smul m' p'

Lemma 5.3.1

theorem smul_C2_1_2 {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)] {p p' : 𝔓 X} (m : ℝ) {n k : ℝ} (hk : 0 < k) (hp : 𝓘 p ≠ 𝓘 p') (hl : smul n p ≤ smul k p') : smul (n + C2_1_2 a * m) p ≤ smul m p'

Lemma 5.3.2 (generalizing 1 to k > 0)

theorem dist_LTSeries {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 : ℕ} {u : Set (𝔓 X)} {s : LTSeries ↑u} (hs : s.length = n) {f g : Θ X} : dist_{𝔠 ↑(RelSeries.head s), ↑(defaultD a) ^ 𝔰 ↑(RelSeries.head s) / 4} f g ≤ C2_1_2 a ^ n * dist_{𝔠 ↑(RelSeries.last s), ↑(defaultD a) ^ 𝔰 ↑(RelSeries.last s) / 4} f g

def C5_3_3 (a : ℕ) : ℝ

The constraint on λ in the first part of Lemma 5.3.3.

Equations

• C5_3_3 a = (1 - C2_1_2 a)⁻¹

theorem C5_3_3_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] : C5_3_3 a ≤ 11 / 10

theorem wiggle_order_11_10 {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)] {p p' : 𝔓 X} {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) : smul n p ≤ smul n p'

Lemma 5.3.3, Equation (5.3.3)

theorem wiggle_order_100 {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)] {p p' : 𝔓 X} (hp : smul 10 p ≤ smul 1 p') (hn : 𝓘 p ≠ 𝓘 p') : smul 100 p ≤ smul 100 p'

Lemma 5.3.3, Equation (5.3.4)

theorem wiggle_order_500 {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)] {p p' : 𝔓 X} (hp : smul 2 p ≤ smul 1 p') (hn : 𝓘 p ≠ 𝓘 p') : smul 4 p ≤ smul 500 p'

Lemma 5.3.3, Equation (5.3.5)

def C5_3_2 (a : ℕ) : ℝ

Equations

• C5_3_2 a = 2 ^ (-95 * ↑a)

def TileLike.toTile {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)] (t : TileLike X) : Set (X × Θ X)

Equations

• t.toTile = ↑t.fst ×ˢ t.snd

def TileLike.toSet {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)] (t : TileLike X) : Set X

From a TileLike, we can construct a set. This is used in the definitions E₁ and E₂.

Equations

• t.toSet = ↑t.fst ∩ G ∩ ⇑Q ⁻¹' t.snd

def E₁ {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)] (p : 𝔓 X) : Set X

Equations

• E₁ p = (toTileLike p).toSet

def E₂ {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)] (l : ℝ) (p : 𝔓 X) : Set X

Equations

• E₂ l p = (smul l p).toSet

theorem E₁_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)] (p : 𝔓 X) : E₁ p ⊆ ↑(𝓘 p)

theorem E₂_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)] (l : ℝ) (p : 𝔓 X) : E₂ l p ⊆ ↑(𝓘 p)

theorem E₂_mono {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)] {p : 𝔓 X} : Monotone fun (l : ℝ) => E₂ l p

def lowerCubes {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)] (𝔓' : Set (𝔓 X)) : Set (𝔓 X)

𝔓(𝔓') in the blueprint. The set of all tiles whose cubes are less than the cube of some tile in the given set.

Equations

• lowerCubes 𝔓' = {p : 𝔓 X | ∃ p' ∈ 𝔓', 𝓘 p ≤ 𝓘 p'}

theorem mem_lowerCubes {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)] {p : 𝔓 X} {𝔓' : Set (𝔓 X)} : p ∈ lowerCubes 𝔓' ↔ ∃ p' ∈ 𝔓', 𝓘 p ≤ 𝓘 p'

theorem lowerCubes_mono {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)] : Monotone lowerCubes

theorem subset_lowerCubes {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)] {𝔓' : Set (𝔓 X)} : 𝔓' ⊆ lowerCubes 𝔓'

def dens₁ {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)] (𝔓' : Set (𝔓 X)) : ENNReal

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number.

Equations

• One or more equations did not get rendered due to their size.

theorem dens₁_mono {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)] {𝔓₁ 𝔓₂ : Set (𝔓 X)} (h : 𝔓₁ ⊆ 𝔓₂) : dens₁ 𝔓₁ ≤ dens₁ 𝔓₂

def dens₂ {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)] (𝔓' : Set (𝔓 X)) : ENNReal

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number.

Equations

• dens₂ 𝔓' = ⨆ p ∈ 𝔓', ⨆ (r : ℝ), ⨆ (_ : r ≥ 4 * ↑(defaultD a) ^ 𝔰 p), MeasureTheory.volume (F ∩ Metric.ball (𝔠 p) r) / MeasureTheory.volume (Metric.ball (𝔠 p) r)

theorem le_dens₂ {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)] (𝔓' : Set (𝔓 X)) {p : 𝔓 X} (hp : p ∈ 𝔓') {r : ℝ} (hr : r ≥ 4 * ↑(defaultD a) ^ 𝔰 p) : MeasureTheory.volume (F ∩ Metric.ball (𝔠 p) r) / MeasureTheory.volume (Metric.ball (𝔠 p) r) ≤ dens₂ 𝔓'

theorem dens₂_eq_biSup_dens₂ {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)] (𝔓' : Set (𝔓 X)) : dens₂ 𝔓' = ⨆ p ∈ 𝔓', dens₂ {p}

theorem dens₁_le_one {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)] {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≤ 1

theorem volume_E₂_le_dens₁_mul_volume {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)] {p p' : 𝔓 X} {𝔓' : Set (𝔓 X)} (mp : p ∈ lowerCubes 𝔓') (mp' : p' ∈ 𝔓') {l : NNReal} (hl : 2 ≤ l) (sp : smul (↑l) p' ≤ smul (↑l) p) : MeasureTheory.volume (E₂ (↑l) p) ≤ ↑l ^ a * dens₁ 𝔓' * MeasureTheory.volume ↑(𝓘 p)

Stack sizes

def stackSize {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)] (C : Set (𝔓 X)) (x : X) : ℕ

The number of tiles p in s whose underlying cube 𝓘 p contains x.

Equations

• stackSize C x = ∑ p : 𝔓 X with p ∈ C, (↑(𝓘 p)).indicator 1 x

theorem stackSize_setOf_add_stackSize_setOf_not {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)] {C : Set (𝔓 X)} {x : X} {P : 𝔓 X → Prop} : stackSize {p : 𝔓 X | p ∈ C ∧ P p} x + stackSize {p : 𝔓 X | p ∈ C ∧ ¬P p} x = stackSize C x

theorem stackSize_inter_add_stackSize_sdiff {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)] {C C' : Set (𝔓 X)} {x : X} : stackSize (C ∩ C') x + stackSize (C \ C') x = stackSize C x

theorem stackSize_sdiff_eq {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)] {C C' : Set (𝔓 X)} (x : X) : stackSize (C \ C') x = stackSize C x - stackSize (C ∩ C') x

theorem stackSize_congr {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)] {C : Set (𝔓 X)} {x x' : X} (h : ∀ p ∈ C, x ∈ ↑(𝓘 p) ↔ x' ∈ ↑(𝓘 p)) : stackSize C x = stackSize C x'

theorem stackSize_mono {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)] {C C' : Set (𝔓 X)} {x : X} (h : C ⊆ C') : stackSize C x ≤ stackSize C' x

theorem stackSize_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)] (C : Set (𝔓 X)) (x : X) : ↑(stackSize C x) = ∑ p : 𝔓 X with p ∈ C, (↑(𝓘 p)).indicator 1 x

theorem stackSize_measurable {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)] {C : Set (𝔓 X)} : Measurable fun (x : X) => ↑(stackSize C x)

theorem stackSize_le_one_of_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)] {C : Set (𝔓 X)} {x : X} (h : C.PairwiseDisjoint fun (p : 𝔓 X) => ↑(𝓘 p)) : stackSize C x ≤ 1

theorem eq_empty_of_forall_stackSize_zero {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)] (s : Set (𝔓 X)) : (∀ (x : X), stackSize s x = 0) → s = ∅

Decomposing a set of tiles into disjoint subfamilies

theorem exists_maximal_disjoint_covering_subfamily {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)] (A : Set (𝔓 X)) : ∃ (B : Set (𝔓 X)), (B.PairwiseDisjoint fun (p : 𝔓 X) => ↑(𝓘 p)) ∧ B ⊆ A ∧ ∀ a_1 ∈ A, ∃ b ∈ B, ↑(𝓘 a_1) ⊆ ↑(𝓘 b)

Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything.

def maximalSubfamily {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)] (A : Set (𝔓 X)) : Set (𝔓 X)

A disjoint subfamily of A covering everything.

Equations

• maximalSubfamily A = ⋯.choose

@[irreducible]

def iteratedMaximalSubfamily {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)] (A : Set (𝔓 X)) (n : ℕ) : Set (𝔓 X)

Iterating maximalSubfamily to obtain disjoint subfamilies of A.

Equations

• iteratedMaximalSubfamily A n = maximalSubfamily (A \ ⋃ (i : ↑{i : ℕ | i < n}), have this := ⋯; iteratedMaximalSubfamily A ↑i)

theorem pairwiseDisjoint_iteratedMaximalSubfamily_image {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)] (A : Set (𝔓 X)) (n : ℕ) : (iteratedMaximalSubfamily A n).PairwiseDisjoint fun (p : 𝔓 X) => ↑(𝓘 p)

theorem iteratedMaximalSubfamily_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)] (A : Set (𝔓 X)) (n : ℕ) : iteratedMaximalSubfamily A n ⊆ A

theorem pairwiseDisjoint_iteratedMaximalSubfamily {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)] (A : Set (𝔓 X)) : Set.univ.PairwiseDisjoint (iteratedMaximalSubfamily A)

theorem eq_biUnion_iteratedMaximalSubfamily {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)] (A : Set (𝔓 X)) {N : ℕ} (hN : ∀ (x : X), stackSize A x ≤ N) : A = ⋃ (n : ℕ), ⋃ (_ : n < N), iteratedMaximalSubfamily A n

Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.