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))
- 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)
- 𝔓 : Type u
- fintype_𝔓 : Fintype (PreTileStructure.𝔓 𝕜 X)
- 𝓘 : PreTileStructure.𝔓 𝕜 X → GridStructure.Grid X
- surjective_𝓘 : Function.Surjective PreTileStructure.𝓘
- 𝒬 : PreTileStructure.𝔓 𝕜 X → Θ X
Instances
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]
:
Equations
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]
:
Equations
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]
:
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]
:
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
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)
:
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.
- 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)
- fintype_𝔓 : Fintype (PreTileStructure.𝔓 ℝ X)
- 𝓘 : PreTileStructure.𝔓 ℝ X → GridStructure.Grid X
- 𝒬 : PreTileStructure.𝔓 ℝ X → Θ X
- Ω : PreTileStructure.𝔓 ℝ X → Set (Θ X)
- 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
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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)
def
carlesonOn
{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)
(f : X → ℂ)
:
X → ℂ
The operator T_𝔭 defined in Proposition 2.0.2, considered on the set F.
It is the map T ∘ (1_F * ·) : f ↦ T (1_F * f), also denoted T1_F
The operator T in Proposition 2.0.2 is therefore applied to (F := Set.univ).
Equations
- One or more equations did not get rendered due to their size.
theorem
measurable_carlesonOn
{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}
{f : X → ℂ}
(measf : Measurable f)
:
Measurable (carlesonOn p f)
def
carlesonSum
{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))
(f : X → ℂ)
(x : X)
:
The operator T_ℭ f defined at the bottom of Section 7.4.
We will use this in other places of the formalization as well.
Equations
- carlesonSum ℭ f x = ∑ p ∈ {p : 𝔓 X | p ∈ ℭ}, carlesonOn p f x
theorem
measurable_carlesonSum
{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)}
{f : X → ℂ}
(measf : Measurable f)
:
Measurable (carlesonSum ℭ f)
theorem
MeasureTheory.AEStronglyMeasurable.carlesonOn
{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}
{f : X → ℂ}
(hf : AEStronglyMeasurable f volume)
:
theorem
MeasureTheory.AEStronglyMeasurable.carlesonSum
{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)}
{f : X → ℂ}
(hf : AEStronglyMeasurable f volume)
:
theorem
MeasureTheory.BoundedCompactSupport.carlesonOn
{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}
{f : X → ℂ}
(hf : BoundedCompactSupport f)
:
theorem
MeasureTheory.BoundedCompactSupport.carlesonSum
{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)}
{f : X → ℂ}
(hf : BoundedCompactSupport f)
:
theorem
sum_carlesonSum_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)]
{ι : Type u_2}
{f : X → ℂ}
{x : X}
{A : ι → Set (𝔓 X)}
{s : Finset ι}
(hs : (↑s).PairwiseDisjoint A)
:
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
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.
@[simp]
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
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✝)
:
Deduce an inclusion of tiles from an inclusion of their cubes and
non-disjointness of their Ωs.
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)]
:
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')
:
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')
:
Lemma 5.3.2 (generalizing 1 to k > 0)
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)
:
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')
:
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')
:
Lemma 5.3.3, Equation (5.3.5)
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₂.
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))
:
𝔓(𝔓') in the blueprint.
The set of all tiles whose cubes are less than the cube of some tile in the given set.
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)]
:
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))
:
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.
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))
:
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
isAntichain_iff_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)]
(𝔄 : Set (𝔓 X))
:
IsAntichain (fun (x1 x2 : TileLike X) => x1 ≤ x2) (toTileLike '' 𝔄) ↔ ∀ (p p' : 𝔓 X), p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' → Disjoint (toTileLike p).toTile (toTileLike p').toTile
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)
:
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.
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))
:
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))
:
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))
:
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 : ℕ)
:
Iterating maximalSubfamily to obtain disjoint subfamilies of A.
Equations
- iteratedMaximalSubfamily A n = maximalSubfamily (A \ ⋃ (i : ↑{i : ℕ | i < n}), let_fun 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
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)
:
Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.