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)
- 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, GridStructure.s i)
- topCube : GridStructure.Grid X
- s_topCube : GridStructure.s topCube = ↑S
- c_topCube : GridStructure.c topCube = o
- subset_topCube : ∀ {i : GridStructure.Grid X}, ↑i ⊆ ↑topCube
- Grid_subset_biUnion : ∀ {i : GridStructure.Grid X}, ∀ k ∈ Set.Ico (-↑S) (GridStructure.s i), ↑i ⊆ ⋃ j ∈ GridStructure.s ⁻¹' {k}, ↑j
- fundamental_dyadic' : ∀ {i j : GridStructure.Grid X}, GridStructure.s i ≤ GridStructure.s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
- ball_subset_Grid : ∀ {i : GridStructure.Grid X}, Metric.ball (GridStructure.c i) (↑D ^ GridStructure.s i / 4) ⊆ ↑i
- Grid_subset_ball : ∀ {i : GridStructure.Grid X}, ↑i ⊆ Metric.ball (GridStructure.c i) (4 * ↑D ^ GridStructure.s i)
- small_boundary : ∀ {i : GridStructure.Grid X} {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}, MeasurableSet ↑i
Instances
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
Equations
- s = GridStructure.s
Equations
- c = GridStructure.c
Equations
- instInhabitedGrid = { default := topCube }
Equations
- instFintypeGrid = GridStructure.fintype_Grid
Equations
- instCoeGridSet = { coe := GridStructure.coeGrid }
Equations
- instPartialOrderGrid = PartialOrder.lift (fun (i : GridStructure.Grid X) => (↑i, GridStructure.s i)) ⋯
The set I ↦ Iᵒ
in the blueprint.
Equations
- Grid.«term_ᵒ» = Lean.ParserDescr.trailingNode `Grid.«term_ᵒ» 1024 1024 (Lean.ParserDescr.symbol "ᵒ")
An auxiliary measure used in the well-foundedness of Ω
in Lemma tile_structure
.
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.
There exists a unique successor of each non-maximal cube.
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.
Maximal elements of finsets of dyadic cubes #
Equations
- Grid.maxCubes s = Finset.filter (fun (i : Grid X) => ∀ j ∈ s, i ≤ j → i = j) s
Stronger version of Lemma 2.1.2.