class
GridStructure
(X : Type u)
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
(D : outParam ℕ)
(κ : outParam ℝ)
(S : outParam ℕ)
(o : outParam X)
:
Type (u + 1)
A grid structure on X.
I expect 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 A)
- coeGrid : GridStructure.Grid X A → Set X
The collection of dyadic cubes
- s : GridStructure.Grid X A → ℤ
scale functions
- c : GridStructure.Grid X A → X
Center functions
- inj : Function.Injective fun (i : GridStructure.Grid X A) => (↑i, GridStructure.s i)
- topCube : GridStructure.Grid X A
- s_topCube : GridStructure.s topCube = ↑S
- c_topCube : GridStructure.c topCube = o
- subset_topCube : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ ↑topCube
- Grid_subset_biUnion : ∀ {i : GridStructure.Grid X A}, ∀ k ∈ Set.Ico (-↑S) (GridStructure.s i), ↑i ⊆ ⋃ j ∈ GridStructure.s ⁻¹' {k}, ↑j
- fundamental_dyadic' : ∀ {i j : GridStructure.Grid X A}, GridStructure.s i ≤ GridStructure.s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
- ball_subset_Grid : ∀ {i : GridStructure.Grid X A}, Metric.ball (GridStructure.c i) (↑D ^ GridStructure.s i / 4) ⊆ ↑i
- Grid_subset_ball : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ Metric.ball (GridStructure.c i) (4 * ↑D ^ GridStructure.s i)
- small_boundary : ∀ {i : GridStructure.Grid X A} {t : NNReal}, ↑D ^ (-↑S - GridStructure.s i) ≤ t → MeasureTheory.volume.real {x : X | x ∈ ↑i ∧ EMetric.infEdist x (↑i)ᶜ ≤ ↑t * ↑D ^ GridStructure.s i} ≤ 2 * ↑t ^ κ * MeasureTheory.volume.real ↑i
- coeGrid_measurable : ∀ {i : GridStructure.Grid X A}, MeasurableSet ↑i
Instances
theorem
GridStructure.inj
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
:
Function.Injective fun (i : GridStructure.Grid X A) => (↑i, GridStructure.s i)
theorem
GridStructure.range_s_subset
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
:
theorem
GridStructure.s_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
:
GridStructure.s topCube = ↑S
theorem
GridStructure.c_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
:
GridStructure.c topCube = o
theorem
GridStructure.subset_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
:
↑i ⊆ ↑topCube
theorem
GridStructure.Grid_subset_biUnion
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
(k : ℤ)
:
theorem
GridStructure.fundamental_dyadic'
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
{j : GridStructure.Grid X A}
:
GridStructure.s i ≤ GridStructure.s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
theorem
GridStructure.ball_subset_Grid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
:
Metric.ball (GridStructure.c i) (↑D ^ GridStructure.s i / 4) ⊆ ↑i
theorem
GridStructure.Grid_subset_ball
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
:
↑i ⊆ Metric.ball (GridStructure.c i) (4 * ↑D ^ GridStructure.s i)
theorem
GridStructure.small_boundary
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
{t : NNReal}
(ht : ↑D ^ (-↑S - GridStructure.s i) ≤ t)
:
theorem
GridStructure.coeGrid_measurable
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : outParam ℕ}
{κ : outParam ℝ}
{S : outParam ℕ}
{o : outParam X}
[self : GridStructure X D κ S o]
{i : GridStructure.Grid X A}
:
@[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 A
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
- s = GridStructure.s
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
- c = GridStructure.c
Instances For
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
instFintypeGrid
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
Equations
- instFintypeGrid = GridStructure.fintype_Grid
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
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
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 A) => (↑i, GridStructure.s i)) ⋯
theorem
fundamental_dyadic
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
{i : Grid X}
{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 : Grid X}
{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 : Grid X}
{j : Grid X}
:
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 : Grid X}
{j : Grid X}
(hs : s i = s j)
:
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}
:
@[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 : Grid X}
{j : 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]
:
Function.Injective fun (i : Grid X) => (↑i, s i)
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}
:
i ≤ topCube
theorem
Grid.isTop_topCube
{X : Type u}
{A : NNReal}
[PseudoMetricSpace X]
[MeasureTheory.DoublingMeasure X A]
{D : ℕ}
{κ : ℝ}
{S : ℕ}
{o : X}
[GridStructure X D κ S o]
:
IsTop topCube
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}
:
theorem
Grid.isMin_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}
:
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.le_of_mem_of_mem
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{i : Grid X}
{j : Grid X}
(h : s i ≤ s j)
{c : X}
(mi : c ∈ i)
(mj : c ∈ j)
:
i ≤ j
theorem
Grid.le_dyadic
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{i : Grid X}
{j : Grid X}
{k : Grid X}
(h : s i ≤ s j)
(li : k ≤ i)
(lj : k ≤ j)
:
i ≤ j
@[simp]
theorem
Grid.exists_unique_succ
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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.
def
Grid.succ
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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_supercube
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 (s i) ↑(defaultS X))
:
theorem
Grid.exists_sandwiched
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{i : Grid X}
{j : Grid X}
(h : i ≤ j)
(l : ℤ)
(hl : l ∈ Set.Icc (s i) (s j))
:
@[irreducible]
theorem
Grid.induction
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 #
def
Grid.maxCubes
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{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 = Finset.filter (fun (i : Grid X) => ∀ j ∈ s, i ≤ j → i = j) s
Instances For
theorem
Grid.exists_maximal_supercube
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{i : Grid X}
{s : Finset (Grid X)}
(hi : i ∈ s)
:
∃ j ∈ Grid.maxCubes s, i ≤ j
theorem
Grid.maxCubes_pairwiseDisjoint
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{s : Finset (Grid X)}
:
(↑(Grid.maxCubes s)).PairwiseDisjoint fun (i : Grid X) => ↑i
theorem
Grid.dist_strictMono
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I : Grid X}
{J : Grid X}
(hpq : I < J)
{f : Θ X}
{g : Θ X}
:
Stronger version of Lemma 2.1.2.
theorem
Grid.dist_mono
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I : Grid X}
{J : Grid X}
(hpq : I ≤ J)
{f : Θ X}
{g : Θ X}
:
Weaker version of Lemma 2.1.2.
theorem
Grid.dist_strictMono_iterate
{X : Type u_1}
[PseudoMetricSpace X]
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[ProofData a q K σ₁ σ₂ F G]
[GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{I : Grid X}
{J : Grid X}
{d : ℕ}
(hij : I ≤ J)
(hs : s I + ↑d = s J)
{f : Θ X}
{g : Θ X}
: