Documentation

Carleson.Discrete.Defs

source
def aux𝓒 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                  theorem exists_bound_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                  βˆƒ (n : β„• Γ— β„•), βˆ€ x ∈ {kn : β„• Γ— β„• | (β„­ kn.1 kn.2).Nonempty}, x.2 ≀ n.2
                  source
                  def maxβ„­ (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                  β„•
                  Equations
                  Instances For
                    source
                    theorem le_maxβ„­_of_nonempty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} (h : (β„­ k n).Nonempty) :
                    n ≀ maxβ„­ X
                    source
                    theorem eq_empty_of_maxβ„­_lt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} (hn : maxβ„­ X < n) :
                    β„­ k n = βˆ…
                    source
                    theorem dens1_le_dens' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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)} (hP : P βŠ† TilesAt k) :
                    dens₁ P ≀ dens' k P

                    Lemma 5.3.11

                    source
                    theorem dens1_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {k n : β„•} {A : Set (𝔓 X)} (hA : A βŠ† β„­ k n) :
                    dens₁ A ≀ 2 ^ (4 * ↑a - ↑n + 1)

                    Lemma 5.3.12

                    source
                    def 𝔅 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 pairwiseDisjoint_ℭ₁' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 (knj : β„• Γ— β„• Γ— β„•) => ℭ₁ knj.1 knj.2.1 knj.2.2
                          source
                          theorem card_𝔅_of_mem_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem π”˜β‚_subset_ℭ₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 pairwiseDisjoint_β„­β‚… {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 (knj : β„• Γ— β„• Γ— β„•) => β„­β‚… knj.1 knj.2.1 knj.2.2
                                                source
                                                theorem 𝔏₀_subset_β„­ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 PF,G, defined in (5.1.24).

                                                Equations
                                                Instances For
                                                  source
                                                  theorem highDensityTiles_empty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                                                  Instances For
                                                    source
                                                    theorem G₁_empty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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
                                                    theorem measurable_G₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                    MeasurableSet G₁
                                                    source
                                                    def setA {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                                                          theorem measurable_Gβ‚‚ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                          MeasurableSet Gβ‚‚
                                                          source
                                                          def G₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                                                            theorem measurable_G₃ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                            MeasurableSet G₃
                                                            source
                                                            def G' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                                                              theorem measurable_G' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                              MeasurableSet G'
                                                              source
                                                              def 𝔓₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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