Documentation

Carleson.GridStructure

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. I expect we prefer coeGrid : GridSet X over Grid : Set (Set X) Note: the s in this paper is -s of Christ's paper.

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] :

    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
    Instances For
    def s {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : } {κ : } {S : } {o : X} [GridStructure X D κ S o] :
    Grid X
    Equations
    • s = GridStructure.s
    def c {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : } {κ : } {S : } {o : X} [GridStructure X D κ S o] :
    Grid XX
    Equations
    • c = GridStructure.c
    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] :
    Coe (Grid X) (Set X)
    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] :
    Equations
    • instMembershipGrid = { mem := fun (i : Grid X) (x : X) => x i }
    instance instPartialOrderGrid {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : } {κ : } {S : } {o : X} [GridStructure X D κ S o] :
    Equations
    @[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} :
    x i x i
    @[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} :
    i j i j s i s j
    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} :
    s i s ji j Disjoint i j
    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) :
    i j Disjoint i 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} :
    i j j i Disjoint i j
    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) :
    i j j i
    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) :
    i 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) :
    i = j Disjoint i j
    theorem subset_of_nmem_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 : iSet.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} :
    s i Set.Icc (-S) S
    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) :
    0 < MeasureTheory.volume i
    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} :
    MeasureTheory.volume i <
    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} :
    IsMax i i = topCube
    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.

    Equations
    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.

    Equations
    • i.opSize = (S - s i).toNat
    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.
    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 Grid.c_mem_Grid {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {i : Grid X} :
    c i i
    theorem Grid.nonempty {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (i : Grid X) :
    (↑i).Nonempty
    theorem Grid.le_dyadic {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {i j k : Grid X} (h : s i s j) (li : k i) (lj : k j) :
    i j
    @[simp]
    theorem Grid.lt_def {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} :
    i < j i j s i < s j
    theorem Grid.isMin_iff {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {i : Grid X} :
    IsMin i s i = -(defaultS X)
    theorem Grid.exists_unique_succ {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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) :
    ∃! j : Grid X, j Finset.univ i < j ∀ (j' : Grid X), i < j'j j'

    There exists a unique successor of each non-maximal cube.

    def Grid.succ {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (i : 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
    theorem Grid.succ_spec {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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) :
    i < i.succ ∀ (j : Grid X), i < ji.succ j
    theorem Grid.succ_unique {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} (h : ¬IsMax i) :
    i < j(∀ (j' : Grid X), i < j'j j')i.succ = j
    theorem Grid.le_succ {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {i : Grid X} :
    i i.succ
    theorem Grid.max_of_le_succ {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {i : Grid X} :
    i.succ iIsMax i
    theorem Grid.succ_le_of_lt {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} (h : i < j) :
    i.succ j
    theorem Grid.exists_containing_subcube {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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) :
    ∃ (j : Grid X), s j = l x j
    theorem Grid.exists_supercube {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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 (s i) (defaultS X)) :
    ∃ (j : Grid X), s j = l i j
    theorem Grid.exists_sandwiched {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} (h : i j) (l : ) (hl : l Set.Icc (s i) (s j)) :
    ∃ (k : Grid X), s k = l i k k j
    theorem Grid.scale_succ {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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) :
    s i.succ = s i + 1
    theorem Grid.opSize_succ_lt {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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) :
    i.succ.opSize < i.opSize
    @[irreducible]
    theorem Grid.induction {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] [GridStructure X (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (P : Grid XProp) (base : ∀ (i : Grid X), IsMax iP i) (ind : ∀ (i : Grid X), ¬IsMax iP i.succP i) (i : Grid X) :
    P i
    theorem Grid.succ_def {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} (h : ¬IsMax i) :
    i.succ = j i j s j = s i + 1

    Maximal elements of finsets of dyadic cubes #

    def Grid.maxCubes {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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
    theorem Grid.exists_maximal_supercube {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F 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) :
    jGrid.maxCubes s, i j
    theorem Grid.maxCubes_pairwiseDisjoint {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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)} :
    (↑(Grid.maxCubes s)).PairwiseDisjoint fun (i : Grid X) => i
    def C2_1_2 (a : ) :

    The constant appearing in Lemma 2.1.2, 2 ^ {-95a}.

    Equations
    theorem C2_1_2_le_inv_512 (X : Type u_1) [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] :
    C2_1_2 a 1 / 512
    theorem C2_1_2_le_one (X : Type u_1) [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] :
    theorem C2_1_2_lt_one (X : Type u_1) [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : X} {F G : Set X} [ProofData a q K σ₁ σ₂ F G] :
    C2_1_2 a < 1
    theorem Grid.dist_strictMono {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} :
    dist f g C2_1_2 a * dist f g

    Stronger version of Lemma 2.1.2.

    theorem Grid.dist_mono {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} :
    dist f g dist f g

    Weaker version of Lemma 2.1.2.

    theorem Grid.dist_strictMono_iterate {X : Type u_1} [PseudoMetricSpace X] {a : } {q : } {K : XX} {σ₁ σ₂ : 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} :
    dist f g C2_1_2 a ^ d * dist f g