Documentation

Carleson.Discrete.Defs

source
def aux𝓒 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) :
Set (Grid X)
Equations
Instances For
    source
    def 𝓒 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) :
    Set (Grid X)

    The partition 𝓒(G, k) of Grid X by volume, given in (5.1.1) and (5.1.2). Note: the G is fixed with properties in ProofData.

    Equations
    Instances For
      source
      def TilesAt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) :
      Set (𝔓 X)

      The definition 𝔓(k) given in (5.1.3).

      Equations
      Instances For
        source
        theorem disjoint_TilesAt_of_ne {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {m : β„•} {n : β„•} (h : m β‰  n) :
        Disjoint (TilesAt m) (TilesAt n)
        source
        theorem pairwiseDisjoint_TilesAt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
        Set.univ.PairwiseDisjoint TilesAt
        source
        def aux𝔐 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) :
        Set (𝔓 X)
        Equations
        Instances For
          source
          def 𝔐 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) :
          Set (𝔓 X)

          The definition 𝔐(k, n) given in (5.1.4) and (5.1.5).

          Equations
          Instances For
            source
            def dens' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (P' : Set (𝔓 X)) :
            ENNReal

            The definition dens'_k(𝔓') given in (5.1.6).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem dens'_iSup {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {P : Set (𝔓 X)} :
              dens' k P = ⨆ p ∈ P, dens' k {p}
              source
              def auxβ„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) :
              Set (𝔓 X)
              Equations
              Instances For
                source
                def β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) :
                Set (𝔓 X)

                The partition β„­(k, n) of 𝔓(k) by density, given in (5.1.7).

                Equations
                Instances For
                  source
                  theorem β„­_subset_TilesAt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} :
                  β„­ k n βŠ† TilesAt k
                  source
                  theorem disjoint_β„­_of_ne {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {m : β„•} {n : β„•} (h : m β‰  n) :
                  Disjoint (β„­ k m) (β„­ k n)
                  source
                  theorem pairwiseDisjoint_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                  Set.univ.PairwiseDisjoint fun (kn : β„• Γ— β„•) => β„­ kn.1 kn.2
                  source
                  def 𝔅 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (p : 𝔓 X) :
                  Set (𝔓 X)

                  The subset 𝔅(p) of 𝔐(k, n), given in (5.1.8).

                  Equations
                  Instances For
                    source
                    def preℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                    Set (𝔓 X)
                    Equations
                    Instances For
                      source
                      def ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                      Set (𝔓 X)

                      The subset ℭ₁(k, n, j) of β„­(k, n), given in (5.1.9). Together with 𝔏₀(k, n) this forms a partition.

                      Equations
                      Instances For
                        source
                        theorem ℭ₁_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                        ℭ₁ k n j βŠ† β„­ k n
                        source
                        theorem disjoint_ℭ₁_of_ne {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {l : β„•} (h : j β‰  l) :
                        Disjoint (ℭ₁ k n j) (ℭ₁ k n l)
                        source
                        theorem pairwiseDisjoint_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} :
                        Set.univ.PairwiseDisjoint (ℭ₁ k n)
                        source
                        theorem card_𝔅_of_mem_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {p : 𝔓 X} (hp : p ∈ ℭ₁ k n j) :
                        (𝔅 k n p).toFinset.card ∈ Set.Ico (2 ^ j) (2 ^ (j + 1))
                        source
                        def 𝔏₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) :
                        Set (𝔓 X)

                        The subset 𝔏₀(k, n) of β„­(k, n), given in (5.1.10). Not to be confused with 𝔏₀(k, n, j) which is called 𝔏₀' in Lean.

                        Equations
                        Instances For
                          source
                          def 𝔏₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) (l : β„•) :
                          Set (𝔓 X)

                          𝔏₁(k, n, j, l) consists of the minimal elements in ℭ₁(k, n, j) not in 𝔏₁(k, n, j, l') for some l' < l. Defined near (5.1.11).

                          Equations
                          Instances For
                            source
                            def β„­β‚‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                            Set (𝔓 X)

                            The subset β„­β‚‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.13).

                            Equations
                            Instances For
                              source
                              theorem β„­β‚‚_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                              β„­β‚‚ k n j βŠ† ℭ₁ k n j
                              source
                              def π”˜β‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                              Set (𝔓 X)

                              The subset π”˜β‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.14).

                              Equations
                              Instances For
                                source
                                theorem π”˜β‚_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                π”˜β‚ k n j βŠ† ℭ₁ k n j
                                source
                                def 𝔏₂ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                                Set (𝔓 X)

                                The subset 𝔏₂(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.15).

                                Equations
                                Instances For
                                  source
                                  theorem 𝔏₂_subset_β„­β‚‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                  𝔏₂ k n j βŠ† β„­β‚‚ k n j
                                  source
                                  def ℭ₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                                  Set (𝔓 X)

                                  The subset ℭ₃(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.16).

                                  Equations
                                  Instances For
                                    source
                                    theorem ℭ₃_def {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {p : 𝔓 X} :
                                    p ∈ ℭ₃ k n j ↔ p ∈ β„­β‚‚ k n j ∧ βˆƒ u ∈ π”˜β‚ k n j, π“˜ p β‰  π“˜ u ∧ smul 2 p ≀ smul 1 u
                                    source
                                    theorem ℭ₃_subset_β„­β‚‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                    ℭ₃ k n j βŠ† β„­β‚‚ k n j
                                    source
                                    def 𝔏₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) (l : β„•) :
                                    Set (𝔓 X)

                                    𝔏₃(k, n, j, l) consists of the maximal elements in ℭ₃(k, n, j) not in 𝔏₃(k, n, j, l') for some l' < l. Defined near (5.1.17).

                                    Equations
                                    Instances For
                                      source
                                      def β„­β‚„ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                                      Set (𝔓 X)

                                      The subset β„­β‚„(k, n, j) of ℭ₃(k, n, j), given in (5.1.19).

                                      Equations
                                      Instances For
                                        source
                                        theorem β„­β‚„_subset_ℭ₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                        β„­β‚„ k n j βŠ† ℭ₃ k n j
                                        source
                                        def 𝓛 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (n : β„•) (u : 𝔓 X) :
                                        Set (Grid X)

                                        The subset 𝓛(u) of Grid X, given near (5.1.20). Note: It seems to also depend on n.

                                        Equations
                                        Instances For
                                          source
                                          def 𝔏₄ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                                          Set (𝔓 X)

                                          The subset 𝔏₄(k, n, j) of β„­β‚„(k, n, j), given near (5.1.22). Todo: we may need to change the definition to say that p is at most the least upper bound of 𝓛 n u in Grid X.

                                          Equations
                                          Instances For
                                            source
                                            theorem 𝔏₄_subset_β„­β‚„ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                            𝔏₄ k n j βŠ† β„­β‚„ k n j
                                            source
                                            def β„­β‚… {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (k : β„•) (n : β„•) (j : β„•) :
                                            Set (𝔓 X)

                                            The subset β„­β‚…(k, n, j) of β„­β‚„(k, n, j), given in (5.1.23).

                                            Equations
                                            Instances For
                                              source
                                              theorem β„­β‚…_def {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {p : 𝔓 X} :
                                              p ∈ β„­β‚… k n j ↔ p ∈ β„­β‚„ k n j ∧ βˆ€ u ∈ π”˜β‚ k n j, ¬↑(π“˜ p) βŠ† ⋃ i ∈ 𝓛 n u, ↑i
                                              source
                                              theorem β„­β‚…_subset_β„­β‚„ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              β„­β‚… k n j βŠ† β„­β‚„ k n j
                                              source
                                              theorem 𝔏₀_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} :
                                              𝔏₀ k n βŠ† β„­ k n
                                              source
                                              theorem 𝔏₀_disjoint_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              Disjoint (𝔏₀ k n) (ℭ₁ k n j)
                                              source
                                              theorem 𝔏₁_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {l : β„•} :
                                              𝔏₁ k n j l βŠ† ℭ₁ k n j
                                              source
                                              theorem 𝔏₁_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {l : β„•} :
                                              𝔏₁ k n j l βŠ† β„­ k n
                                              source
                                              theorem 𝔏₂_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              𝔏₂ k n j βŠ† ℭ₁ k n j
                                              source
                                              theorem 𝔏₂_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              𝔏₂ k n j βŠ† β„­ k n
                                              source
                                              theorem 𝔏₂_disjoint_ℭ₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              Disjoint (𝔏₂ k n j) (ℭ₃ k n j)
                                              source
                                              theorem 𝔏₃_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {l : β„•} :
                                              𝔏₃ k n j l βŠ† ℭ₁ k n j
                                              source
                                              theorem 𝔏₃_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} {l : β„•} :
                                              𝔏₃ k n j l βŠ† β„­ k n
                                              source
                                              theorem 𝔏₄_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              𝔏₄ k n j βŠ† ℭ₁ k n j
                                              source
                                              theorem 𝔏₄_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              𝔏₄ k n j βŠ† β„­ k n
                                              source
                                              theorem β„­β‚…_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              β„­β‚… k n j βŠ† ℭ₁ k n j
                                              source
                                              theorem β„­β‚…_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k : β„•} {n : β„•} {j : β„•} :
                                              β„­β‚… k n j βŠ† β„­ k n
                                              source
                                              def highDensityTiles {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                              Set (𝔓 X)

                                              The set $\mathcal{P}_{F,G}$, defined in (5.1.24).

                                              Equations
                                              Instances For
                                                source
                                                theorem highDensityTiles_empty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (hF : MeasureTheory.volume F = 0) :
                                                highDensityTiles = βˆ…
                                                source
                                                theorem highDensityTiles_empty' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (hG : MeasureTheory.volume G = 0) :
                                                highDensityTiles = βˆ…
                                                source
                                                def G₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                Set X

                                                The exceptional set G₁, defined in (5.1.25).

                                                Equations
                                                • G₁ = ⋃ p ∈ highDensityTiles, ↑(π“˜ p)
                                                Instances For
                                                  source
                                                  theorem G₁_empty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (hF : MeasureTheory.volume F = 0) :
                                                  G₁ = βˆ…
                                                  source
                                                  theorem G₁_empty' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (hG : MeasureTheory.volume G = 0) :
                                                  G₁ = βˆ…
                                                  source
                                                  def setA {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : β„•) (k : β„•) (n : β„•) :
                                                  Set X

                                                  The set A(Ξ», k, n), defined in (5.1.26).

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem setA_subset_iUnion_𝓒 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {l : β„•} {k : β„•} {n : β„•} :
                                                    setA l k n βŠ† ⋃ i ∈ 𝓒 k, ↑i
                                                    source
                                                    theorem setA_subset_setA {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {l : β„•} {k : β„•} {n : β„•} :
                                                    setA (l + 1) k n βŠ† setA l k n
                                                    source
                                                    theorem measurable_setA {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {l : β„•} {k : β„•} {n : β„•} :
                                                    MeasurableSet (setA l k n)
                                                    source
                                                    def MsetA {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (l : β„•) (k : β„•) (n : β„•) :
                                                    Finset (Grid X)

                                                    Finset of cubes in setA. Appears in the proof of Lemma 5.2.5.

                                                    Equations
                                                    Instances For
                                                      source
                                                      def Gβ‚‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                      Set X

                                                      The set Gβ‚‚, defined in (5.1.27).

                                                      Equations
                                                      Instances For
                                                        source
                                                        def G₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                        Set X

                                                        The set G₃, defined in (5.1.28).

                                                        Equations
                                                        Instances For
                                                          source
                                                          def G' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                          Set X

                                                          The set G', defined below (5.1.28).

                                                          Equations
                                                          Instances For
                                                            source
                                                            def 𝔓₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                            Set (𝔓 X)

                                                            The set 𝔓₁, defined in (5.1.30).

                                                            Equations
                                                            Instances For