class
GridStructure
(X : Type u_2)
{A : outParam NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
(D : outParam ℕ)
(κ : outParam ℝ)
(S : outParam ℕ)
(o : outParam X)
:
Type (max (u + 1) u_2)
A grid structure on X.
We prefer coeGrid : Grid → Set X over Grid : Set (Set X)
Note: the s in this paper is -s of Christ's paper.
- Grid : Type u
indexing set for a grid structure
- fintype_Grid : Fintype (GridStructure.Grid X)
- coeGrid : GridStructure.Grid X → Set X
The collection of dyadic cubes
- s : GridStructure.Grid X → ℤ
scale functions
- c : GridStructure.Grid X → X
Center functions
- inj : Function.Injective fun (i : GridStructure.Grid X) => (↑i, s i)
- topCube : GridStructure.Grid X
- subset_topCube {i : GridStructure.Grid X} : ↑i ⊆ ↑topCube
- 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)
- coeGrid_measurable {i : GridStructure.Grid X} : MeasurableSet ↑i
Instances
@[reducible, inline]
abbrev
Grid
(X : Type u)
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Type u
The indexing type of the grid structure. Elements are called (dyadic) cubes.
Note that this type has instances for both ≤ and ⊆, but they do not coincide.
Equations
- Grid X = GridStructure.Grid X
Instances For
def
s
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Equations
Instances For
def
c
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Grid X → X
Equations
Instances For
@[instance_reducible]
instance
instInhabitedGrid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Equations
- instInhabitedGrid = { default := topCube }
@[instance_reducible]
instance
instFintypeGrid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Equations
@[instance_reducible]
instance
instCoeGridSet
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Equations
- instCoeGridSet = { coe := GridStructure.coeGrid }
@[instance_reducible]
instance
instMembershipGrid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Membership X (Grid X)
@[instance_reducible]
noncomputable instance
instPartialOrderGrid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
PartialOrder (Grid X)
Equations
- instPartialOrderGrid = PartialOrder.lift (fun (i : GridStructure.Grid X) => (↑i, GridStructure.s i)) ⋯
@[simp]
theorem
Grid.mem_def
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
{x : X}
:
@[simp]
theorem
Grid.le_def
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
:
theorem
Grid.eq_iff
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
:
theorem
Grid.mem_mono
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{x : X}
:
theorem
fundamental_dyadic
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
:
theorem
le_or_disjoint
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
(h : s i ≤ s j)
:
theorem
le_or_ge_or_disjoint
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
:
theorem
le_or_ge_of_mem_of_mem
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
{c : X}
(mi : c ∈ i)
(mj : c ∈ j)
:
theorem
le_of_mem_of_mem
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
(h : s i ≤ s j)
{c : X}
(mi : c ∈ i)
(mj : c ∈ j)
:
theorem
eq_or_disjoint
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
(hs : s i = s j)
:
theorem
disjoint_of_not_le_not_le
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i j : Grid X}
(h : ¬i ≤ j)
(h' : ¬j ≤ i)
:
Disjoint ↑i ↑j
theorem
subset_of_notMem_Iic_of_not_disjoint
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
(i j : Grid X)
(h : i ∉ Set.Iic j)
(notDisjoint : ¬Disjoint ↑i ↑j)
:
↑j ⊆ ↑i
theorem
scale_mem_Icc
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
:
theorem
volume_coeGrid_pos
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
(hD : 0 < D)
:
theorem
volume_coeGrid_lt_top
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
:
theorem
Grid.inj
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
theorem
Grid.le_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
:
theorem
Grid.isTop_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
theorem
Grid.isMax_iff
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
:
def
Grid.int
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
(i : Grid X)
:
Set X
The set I ↦ Iᵒ in the blueprint.
Instances For
Equations
- Grid.«term_ᵒ» = Lean.ParserDescr.trailingNode `Grid.«term_ᵒ» 1024 1024 (Lean.ParserDescr.symbol "ᵒ")
Instances For
def
Grid.opSize
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
(i : Grid X)
:
An auxiliary measure used in the well-foundedness of Ω in Lemma tile_structure.
Instances For
theorem
Grid.int_subset
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
:
iᵒ ⊆ ↑i
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Grid.exists_unique_succ
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(i : Grid X)
(h : ¬IsMax i)
:
There exists a unique successor of each non-maximal cube.
noncomputable def
Grid.succ
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(i : Grid X)
:
Grid X
If i is not a maximal element, this is the (unique) minimal element greater than i.
This is not a SuccOrder since an element can be the successor of multiple other elements.
Equations
Instances For
theorem
Grid.exists_containing_subcube
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{i : Grid X}
(l : ℤ)
(h : l ∈ Set.Icc (-↑(defaultS X)) (s i))
{x : X}
(mx : x ∈ i)
:
theorem
Grid.induction
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(P : Grid X → Prop)
(base : ∀ (i : Grid X), IsMax i → P i)
(ind : ∀ (i : Grid X), ¬IsMax i → P i.succ → P i)
(i : Grid X)
:
P i
Maximal elements of finsets of dyadic cubes #
noncomputable def
Grid.maxCubes
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(s : Finset (Grid X))
:
Equations
- Grid.maxCubes s = {i ∈ s | ∀ j ∈ s, i ≤ j → i = j}
Instances For
theorem
Grid.maxCubes_pairwiseDisjoint
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{s : Finset (Grid X)}
:
(↑(maxCubes s)).PairwiseDisjoint fun (i : Grid X) => ↑i
theorem
Grid.dist_strictMono
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I J : Grid X}
(hpq : I < J)
{f g : Θ X}
:
Stronger version of Lemma 2.1.2.
theorem
Grid.dist_strictMono_iterate
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I J : Grid X}
{d : ℕ}
(hij : I ≤ J)
(hs : s I + ↑d = s J)
{f g : Θ X}
:
theorem
Grid.dist_strictMono_iterate'
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I J : Grid X}
{d : ℤ}
(hd : d ≥ 0)
(hij : I ≤ J)
(hs : s I + d = s J)
{f g : Θ X}
:
theorem
Grid.dist_c_le_of_subset
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ σ₂ : X → ℤ}
{F G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{J J' : Grid X}
(subset : ↑J ⊆ ↑J')
: