Documentation

Carleson.TileExistence

source
theorem realD_nonneg {a : β„•} :
0 ≀ ↑(defaultD a)
source
theorem ball_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {Y : Set X} (k : β„€) (hk_lower : -↑(defaultS X) ≀ k) (hY : Y βŠ† Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ ↑(defaultS X) - ↑(defaultD a) ^ k)) (y : X) (hy : y ∈ Y) :
Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ ↑(defaultS X)) βŠ† Metric.ball y (8 * ↑(defaultD a) ^ (2 * ↑(defaultS X)) * ↑(defaultD a) ^ k)
source
def J' (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
β„•
Equations
Instances For
    source
    theorem twopow_J {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 ^ J' X = 8 * defaultD a ^ (2 * defaultS X)
    source
    theorem twopow_J' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 ^ J' X = 8 * nnD a ^ (2 * defaultS X)
    source
    def C4_1_1 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    NNReal
    Equations
    Instances For
      source
      theorem counting_balls {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk_lower : -↑(defaultS X) ≀ k) {Y : Set X} (hY : Y βŠ† Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k)) (hYdisjoint : Y.PairwiseDisjoint fun (y : X) => Metric.ball y (↑(defaultD a) ^ k)) :
      ↑Y.encard ≀ ↑(C4_1_1 X)
      source
      def property_set (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
      Set (Set X)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem property_set_nonempty (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
        (if k = ↑(defaultS X) then {cancelPt X} else βˆ…) ∈ property_set X k
        source
        theorem chain_property_set_has_bound (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) (c : Set (Set X)) :
        c βŠ† property_set X k β†’ IsChain (fun (x1 x2 : Set X) => x1 βŠ† x2) c β†’ βˆƒ ub ∈ property_set X k, βˆ€ s ∈ c, s βŠ† ub
        source
        def zorn_apply_maximal_set (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
        βˆƒ s ∈ property_set X k, βˆ€ s' ∈ property_set X k, s βŠ† s' β†’ s' = s
        Equations
        • β‹― = β‹―
        Instances For
          source
          def Yk (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
          Set X
          Equations
          • Yk X k = β‹―.choose
          Instances For
            source
            theorem Yk_pairwise {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
            (Yk X k).PairwiseDisjoint fun (y : X) => Metric.ball y (↑(defaultD a) ^ k)
            source
            theorem Yk_subset {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
            Yk X k βŠ† Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k)
            source
            theorem Yk_maximal {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) {s : Set X} (hs_sub : s βŠ† Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k)) (hs_pairwise : s.PairwiseDisjoint fun (y : X) => Metric.ball y (↑(defaultD a) ^ k)) (hmax_sub : Yk X k βŠ† s) (hk_s : k = ↑(defaultS X) β†’ cancelPt X ∈ s) :
            s = Yk X k
            source
            theorem o_mem_Yk_S {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
            cancelPt X ∈ Yk X ↑(defaultS X)
            source
            theorem cover_big_ball {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
            Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k) βŠ† ⋃ y ∈ Yk X k, Metric.ball y (2 * ↑(defaultD a) ^ k)
            source
            theorem Yk_nonempty (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hmin : 0 < 4 * ↑(defaultD a) ^ defaultS X - ↑(defaultD a) ^ k) :
            (Yk X k).Nonempty
            source
            theorem Yk_finite {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk_lower : -↑(defaultS X) ≀ k) :
            (Yk X k).Finite
            source
            theorem Yk_countable (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
            (Yk X k).Countable
            source
            def Yk_encodable (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
            Encodable ↑(Yk X k)
            Equations
            Instances For
              source
              def Encodable.linearOrder {Ξ± : Type u_2} (i : Encodable Ξ±) :
              LinearOrder Ξ±
              Equations
              Instances For
                source
                instance instLinearOrderElemYk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} :
                LinearOrder ↑(Yk X k)
                Equations
                source
                instance instWellFoundedLTElemYk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} :
                WellFoundedLT ↑(Yk X k)
                Equations
                • β‹― = β‹―
                source
                def instSizeOfElemYk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} :
                SizeOf ↑(Yk X k)
                Equations
                • instSizeOfElemYk = { sizeOf := Encodable.encode }
                Instances For
                  source
                  theorem I_induction_proof {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (hneq : Β¬k = -↑(defaultS X)) :
                  -↑(defaultS X) ≀ k - 1
                  source
                  @[irreducible]
                  def I1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                  Set X
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[irreducible]
                    def I2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                    Set X
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[irreducible]
                      def Xk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) :
                      Set X
                      Equations
                      • Xk hk = ⋃ (y' : ↑(Yk X k)), I1 hk y'
                      Instances For
                        source
                        @[irreducible]
                        def I3 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                        Set X
                        Equations
                        Instances For
                          source
                          theorem I3_apply {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          I3 hk y = I1 hk y βˆͺ I2 hk y \ (Xk hk βˆͺ ⋃ (y' : ↑(Yk X k)), ⋃ (_ : y' < y), I3 hk y')
                          source
                          theorem I1_subset_I3 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          I1 hk y βŠ† I3 hk y
                          source
                          theorem I1_subset_I2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          I1 hk y βŠ† I2 hk y
                          source
                          theorem I3_subset_I2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          I3 hk y βŠ† I2 hk y
                          source
                          @[irreducible]
                          theorem I1_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          MeasurableSet (I1 hk y)
                          source
                          @[irreducible]
                          theorem I2_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          MeasurableSet (I2 hk y)
                          source
                          @[irreducible]
                          theorem Xk_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) :
                          MeasurableSet (Xk hk)
                          source
                          @[irreducible]
                          theorem I3_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          MeasurableSet (I3 hk y)
                          source
                          @[irreducible]
                          theorem I1_prop_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) {x : X} {y1 : ↑(Yk X k)} {y2 : ↑(Yk X k)} :
                          x ∈ I1 hk y1 ∩ I1 hk y2 β†’ y1 = y2
                          source
                          @[irreducible]
                          theorem I3_prop_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) {x : X} {y1 : ↑(Yk X k)} {y2 : ↑(Yk X k)} :
                          x ∈ I3 hk y1 ∩ I3 hk y2 β†’ y1 = y2
                          source
                          @[irreducible]
                          theorem I3_prop_3_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          I3 hk y βŠ† Metric.ball (↑y) (4 * ↑(defaultD a) ^ k)
                          source
                          @[irreducible]
                          theorem I2_prop_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) :
                          Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) βŠ† ⋃ (y : ↑(Yk X k)), I2 hk y
                          source
                          @[irreducible]
                          theorem I3_prop_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) :
                          Metric.ball (cancelPt X) (4 * ↑(defaultD a) ^ defaultS X - 2 * ↑(defaultD a) ^ k) βŠ† ⋃ (y : ↑(Yk X k)), I3 hk y
                          source
                          theorem I3_prop_3_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          Metric.ball (↑y) (2⁻¹ * ↑(defaultD a) ^ k) βŠ† I3 hk y
                          source
                          theorem I3_nonempty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                          (I3 hk y).Nonempty
                          source
                          theorem cover_by_cubes {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {l : β„€} (hl : -↑(defaultS X) ≀ l) {k : β„€} :
                          l ≀ k β†’ βˆ€ (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)), I3 hk y βŠ† ⋃ (yl : ↑(Yk X l)), I3 hl yl
                          source
                          @[irreducible]
                          theorem dyadic_property {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {l : β„€} (hl : -↑(defaultS X) ≀ l) {k : β„€} (hl_k : l ≀ k) (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) (y' : ↑(Yk X l)) :
                          Β¬Disjoint (I3 hl y') (I3 hk y) β†’ I3 hl y' βŠ† I3 hk y
                          source
                          structure ClosenessProperty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k1 : β„€} {k2 : β„€} (hk1 : -↑(defaultS X) ≀ k1) (hk2 : -↑(defaultS X) ≀ k2) (y1 : ↑(Yk X k1)) (y2 : ↑(Yk X k2)) :
                          Prop
                          Instances For
                            source
                            theorem ClosenessProperty.I3_subset {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k1 : β„€} {k2 : β„€} {hk1 : -↑(defaultS X) ≀ k1} {hk2 : -↑(defaultS X) ≀ k2} {y1 : ↑(Yk X k1)} {y2 : ↑(Yk X k2)} (self : ClosenessProperty hk1 hk2 y1 y2) :
                            I3 hk1 y1 βŠ† I3 hk2 y2
                            source
                            theorem ClosenessProperty.I3_infdist_lt {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k1 : β„€} {k2 : β„€} {hk1 : -↑(defaultS X) ≀ k1} {hk2 : -↑(defaultS X) ≀ k2} {y1 : ↑(Yk X k1)} {y2 : ↑(Yk X k2)} (self : ClosenessProperty hk1 hk2 y1 y2) :
                            EMetric.infEdist (↑y1) (I3 hk2 y2)ᢜ < 6 * ↑(defaultD a) ^ k1
                            source
                            theorem transitive_boundary' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k1 : β„€} {k2 : β„€} {k3 : β„€} (hk1 : -↑(defaultS X) ≀ k1) (hk2 : -↑(defaultS X) ≀ k2) (hk3 : -↑(defaultS X) ≀ k3) (hk1_2 : k1 < k2) (hk2_3 : k2 ≀ k3) (y1 : ↑(Yk X k1)) (y2 : ↑(Yk X k2)) (y3 : ↑(Yk X k3)) (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) :
                            ClosenessProperty hk1 hk3 y1 y3 β†’ ClosenessProperty hk1 hk2 y1 y2 ∧ ClosenessProperty hk2 hk3 y2 y3
                            source
                            theorem transitive_boundary {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k1 : β„€} {k2 : β„€} {k3 : β„€} (hk1 : -↑(defaultS X) ≀ k1) (hk2 : -↑(defaultS X) ≀ k2) (hk3 : -↑(defaultS X) ≀ k3) (hk1_2 : k1 ≀ k2) (hk2_3 : k2 ≀ k3) (y1 : ↑(Yk X k1)) (y2 : ↑(Yk X k2)) (y3 : ↑(Yk X k3)) (x : X) (hx : x ∈ I3 hk1 y1 ∩ I3 hk2 y2 ∩ I3 hk3 y3) :
                            ClosenessProperty hk1 hk3 y1 y3 β†’ ClosenessProperty hk1 hk2 y1 y2 ∧ ClosenessProperty hk2 hk3 y2 y3
                            source
                            def const_K {a : β„•} :
                            β„•
                            Equations
                            • const_K = 2 ^ (4 * a + 1)
                            Instances For
                              source
                              def ShortVariables.termK' :
                              Lean.ParserDescr
                              Equations
                              Instances For
                                source
                                theorem K_pos {a : β„•} :
                                0 < ↑const_K
                                source
                                def C4_1_7 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                NNReal
                                Equations
                                Instances For
                                  source
                                  theorem C4_1_7_eq (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                  C4_1_7 X = 2 ^ (4 * a)
                                  source
                                  theorem volume_tile_le_volume_ball {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) :
                                  MeasureTheory.volume (I3 hk y) ≀ ↑(C4_1_7 X) * MeasureTheory.volume (Metric.ball (↑y) (4⁻¹ * ↑(defaultD a) ^ k))
                                  source
                                  theorem le_s {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk_mK : -↑(defaultS X) ≀ k - ↑const_K) (k' : ↑(Set.Ioc (k - ↑const_K) k)) :
                                  -↑(defaultS X) ≀ ↑k'
                                  source
                                  theorem small_boundary' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) (hk : -↑(defaultS X) ≀ k) (hk_mK : -↑(defaultS X) ≀ k - ↑const_K) (y : ↑(Yk X k)) :
                                  βˆ‘' (z : ↑(Yk X (k - ↑const_K))), MeasureTheory.volume (⋃ (_ : ClosenessProperty hk_mK hk z y), I3 hk_mK z) ≀ 2⁻¹ * MeasureTheory.volume (I3 hk y)
                                  source
                                  theorem small_boundary {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) (hk : -↑(defaultS X) ≀ k) (hk_mK : -↑(defaultS X) ≀ k - ↑const_K) (y : ↑(Yk X k)) :
                                  βˆ‘' (z : ↑(Yk X (k - ↑const_K))), βˆ‘αΆ  (_ : ClosenessProperty hk_mK hk z y), MeasureTheory.volume (I3 hk_mK z) ≀ 2⁻¹ * MeasureTheory.volume (I3 hk y)
                                  source
                                  theorem le_s_1' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (n : β„•) {k : β„€} (hk_mn1K : -↑(defaultS X) ≀ k - ↑(n + 1) * ↑const_K) :
                                  -↑(defaultS X) ≀ k - ↑const_K - ↑n * ↑const_K
                                  source
                                  theorem le_s_2' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (n : β„•) {k : β„€} (hk_mn1K : -↑(defaultS X) ≀ k - ↑(n + 1) * ↑const_K) :
                                  -↑(defaultS X) ≀ k - ↑const_K
                                  source
                                  theorem boundary_sum_eq {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) {k' : β„€} (hk' : -↑(defaultS X) ≀ k') (y : ↑(Yk X k)) :
                                  βˆ‘' (y' : ↑(Yk X k')), βˆ‘αΆ  (_ : ClosenessProperty hk' hk y' y), MeasureTheory.volume (I3 hk' y') = MeasureTheory.volume (⋃ (y' : ↑(Yk X k')), ⋃ (_ : ClosenessProperty hk' hk y' y), I3 hk' y')
                                  source
                                  theorem smaller_boundary {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (n : β„•) {k : β„€} (hk : -↑(defaultS X) ≀ k) (hk_mnK : -↑(defaultS X) ≀ k - ↑n * ↑const_K) (y : ↑(Yk X k)) :
                                  βˆ‘' (y' : ↑(Yk X (k - ↑n * ↑const_K))), βˆ‘αΆ  (_ : ClosenessProperty hk_mnK hk y' y), MeasureTheory.volume (I3 hk_mnK y') ≀ 2⁻¹ ^ n * MeasureTheory.volume (I3 hk y)
                                  source
                                  theorem one_lt_realD (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                  1 < ↑(defaultD a)
                                  source
                                  def const_n (a : β„•) {t : ℝ} :
                                  t ∈ Set.Ioo 0 1 β†’ β„•
                                  Equations
                                  Instances For
                                    source
                                    theorem prefloor_nonneg (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :
                                    0 ≀ -Real.logb (↑(defaultD a)) t / ↑const_K
                                    source
                                    theorem const_n_prop_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :
                                    ↑(defaultD a) ^ (const_n a ht * const_K) ≀ t⁻¹
                                    source
                                    theorem const_n_prop_2 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (k : β„€) :
                                    t * ↑(defaultD a) ^ k ≀ ↑(defaultD a) ^ (k - ↑(const_n a ht) * ↑const_K)
                                    source
                                    theorem const_n_is_max (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (n : β„•) :
                                    ↑(defaultD a) ^ (n * const_K) ≀ t⁻¹ β†’ n ≀ const_n a ht
                                    source
                                    theorem const_n_prop_3 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :
                                    (t * ↑(defaultD a) ^ const_K)⁻¹ ≀ ↑(defaultD a) ^ (const_n a ht * const_K)
                                    source
                                    theorem const_n_nonneg (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :
                                    0 ≀ const_n a ht
                                    source
                                    theorem two_le_a (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                    2 ≀ a
                                    source
                                    theorem kappa_le_log2D_inv_mul_K_inv (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                    defaultΞΊ a ≀ (Real.logb 2 ↑(defaultD a) * ↑const_K)⁻¹
                                    source
                                    theorem boundary_measure {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) {t : NNReal} (ht : t ∈ Set.Ioo 0 1) (htD : ↑(defaultD a) ^ (-↑(defaultS X)) ≀ ↑t * ↑(defaultD a) ^ k) :
                                    MeasureTheory.volume {x : X | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᢜ ≀ ↑t * ↑(defaultD a) ^ k} ≀ 2 * ↑t ^ defaultΞΊ a * MeasureTheory.volume (I3 hk y)
                                    source
                                    theorem boundary_measure' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) (y : ↑(Yk X k)) {t : NNReal} (ht : t ∈ Set.Ioo 0 1) (htD : ↑(defaultD a) ^ (-↑(defaultS X)) ≀ ↑t * ↑(defaultD a) ^ k) :
                                    MeasureTheory.volume.real {x : X | x ∈ I3 hk y ∧ EMetric.infEdist x (I3 hk y)ᢜ ≀ ↑t * ↑(defaultD a) ^ k} ≀ 2 * ↑t ^ defaultΞΊ a * MeasureTheory.volume.real (I3 hk y)
                                    source
                                    theorem 𝓓.ext_iff {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} :
                                    βˆ€ {inst : PseudoMetricSpace X} {inst_1 : ProofData a q K σ₁ Οƒβ‚‚ F G} {x y : 𝓓 X}, x = y ↔ x.k = y.k ∧ HEq x.y y.y
                                    source
                                    theorem 𝓓.ext {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} :
                                    βˆ€ {inst : PseudoMetricSpace X} {inst_1 : ProofData a q K σ₁ Οƒβ‚‚ F G} {x y : 𝓓 X}, x.k = y.k β†’ HEq x.y y.y β†’ x = y
                                    source
                                    structure 𝓓 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                    Type u_1
                                    Instances For
                                      source
                                      theorem 𝓓.hk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (self : 𝓓 X) :
                                      -↑(defaultS X) ≀ self.k
                                      source
                                      theorem 𝓓.hk_max {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (self : 𝓓 X) :
                                      self.k ≀ ↑(defaultS X)
                                      source
                                      theorem 𝓓.hsub {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (self : 𝓓 X) :
                                      I3 β‹― self.y βŠ† I3 β‹― ⟨cancelPt X, β‹―βŸ©
                                      source
                                      def max_𝓓 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                      𝓓 X
                                      Equations
                                      Instances For
                                        source
                                        def 𝓓.coe {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (z : 𝓓 X) :
                                        Set X
                                        Equations
                                        • z.coe = I3 β‹― z.y
                                        Instances For
                                          source
                                          def forget_map (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (x : 𝓓 X) :
                                          (k : ↑(Set.Icc (-↑(defaultS X)) ↑(defaultS X))) Γ— ↑(Yk X ↑k)
                                          Equations
                                          • forget_map X x = ⟨⟨x.k, β‹―βŸ©, x.y⟩
                                          Instances For
                                            source
                                            theorem forget_map_inj {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                            Function.Injective (forget_map X)
                                            source
                                            def 𝓓_finite (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                            Finite (𝓓 X)
                                            Equations
                                            • β‹― = β‹―
                                            Instances For
                                              source
                                              def grid_existence (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                              GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)

                                              Proof that there exists a grid structure.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Proof that there exists a tile structure on a grid structure. #

                                                source
                                                def C𝓩 :
                                                ℝ

                                                The constant appearing in 4.2.2 (3 / 10).

                                                Equations
                                                Instances For
                                                  source
                                                  def 𝓩_cands {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) :
                                                  Finset (Finset (Θ X))
                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem exists_𝓩_max_card {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) :
                                                    βˆƒ zmax ∈ 𝓩_cands I, βˆ€ z ∈ 𝓩_cands I, z.card ≀ zmax.card
                                                    source
                                                    def 𝓩 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) :
                                                    Finset (Θ X)

                                                    A finset of maximal cardinality satisfying (4.2.1) and (4.2.2).

                                                    Equations
                                                    Instances For
                                                      source
                                                      theorem 𝓩_spec {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                      𝓩 I βŠ† Q.range ∧ ((↑(𝓩 I)).PairwiseDisjoint fun (x : Θ X) => Metric.ball x C𝓩) ∧ βˆ€ z ∈ 𝓩_cands I, z.card ≀ (𝓩 I).card
                                                      source
                                                      theorem 𝓩_subset {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                      𝓩 I βŠ† Q.range
                                                      source
                                                      theorem 𝓩_pairwiseDisjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                      (↑(𝓩 I)).PairwiseDisjoint fun (x : Θ X) => Metric.ball x C𝓩
                                                      source
                                                      theorem 𝓩_max_card {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} (z : Finset (Θ X)) :
                                                      z ∈ 𝓩_cands I β†’ z.card ≀ (𝓩 I).card
                                                      source
                                                      theorem 𝓩_nonempty {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                      (𝓩 I).Nonempty
                                                      source
                                                      instance instInhabitedSubtypeΘRealMemFinset𝓩 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                      Inhabited { x : Θ X // x ∈ 𝓩 I }
                                                      Equations
                                                      • instInhabitedSubtypeΘRealMemFinset𝓩 = { default := ⟨Exists.choose β‹―, β‹―βŸ© }
                                                      source
                                                      def C4_2_1 :
                                                      ℝ

                                                      7 / 10

                                                      Equations
                                                      Instances For
                                                        source
                                                        theorem frequency_ball_cover {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                        ↑Q.range βŠ† ⋃ z ∈ 𝓩 I, Metric.ball z C4_2_1

                                                        Equation (4.2.3), Lemma 4.2.1

                                                        source
                                                        def tileData_existence {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                        PreTileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          source
                                                          @[irreducible]
                                                          def Construction.Ω₁_aux {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) (k : β„•) :
                                                          Set (Θ X)
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            theorem Construction.Ω₁_aux_disjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) {k : β„•} {l : β„•} (hn : k β‰  l) :
                                                            Disjoint (Construction.Ω₁_aux I k) (Construction.Ω₁_aux I l)
                                                            source
                                                            theorem Construction.disjoint_ball_Ω₁_aux {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (I : Grid X) {z : Θ X} {z' : Θ X} (hz : z ∈ 𝓩 I) (hz' : z' ∈ 𝓩 I) (hn : z β‰  z') :
                                                            Disjoint (Metric.ball z' C𝓩) (Construction.Ω₁_aux I ↑((Finite.equivFin { x : Θ X // x ∈ 𝓩 I }) ⟨z, hz⟩))
                                                            source
                                                            def Construction.Ω₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                            Set (Θ X)
                                                            Equations
                                                            Instances For
                                                              source
                                                              theorem Construction.disjoint_frequency_cubes {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} {f : { x : Θ X // x ∈ 𝓩 I }} {g : { x : Θ X // x ∈ 𝓩 I }} (h : (Construction.Ω₁ ⟨I, f⟩ ∩ Construction.Ω₁ ⟨I, g⟩).Nonempty) :
                                                              f = g

                                                              Lemma 4.2.2

                                                              source
                                                              theorem Construction.ball_subset_Ω₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                              Metric.ball (𝒬 p) C𝓩 βŠ† Construction.Ω₁ p

                                                              Equation (4.2.6), first inclusion

                                                              source
                                                              theorem Construction.Ω₁_subset_ball {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                              Construction.Ω₁ p βŠ† Metric.ball (𝒬 p) C4_2_1

                                                              Equation (4.2.6), second inclusion

                                                              source
                                                              theorem Construction.iUnion_ball_subset_iUnion_Ω₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                              ⋃ z ∈ 𝓩 I, Metric.ball z C4_2_1 βŠ† ⋃ (f : { x : Θ X // x ∈ 𝓩 I }), Construction.Ω₁ ⟨I, f⟩

                                                              Equation (4.2.5)

                                                              source
                                                              def Construction.CΞ© :
                                                              ℝ

                                                              1 / 5

                                                              Equations
                                                              Instances For
                                                                source
                                                                @[irreducible]
                                                                def Construction.Ξ© {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                                Set (Θ X)
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  source
                                                                  @[irreducible]
                                                                  theorem Construction.𝔓_induction {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (P : 𝔓 X β†’ Prop) (base : βˆ€ (p : 𝔓 X), IsMax p.fst β†’ P p) (ind : βˆ€ (p : 𝔓 X), Β¬IsMax p.fst β†’ (βˆ€ (z : { x : Θ X // x ∈ 𝓩 p.fst.succ }), P ⟨p.fst.succ, z⟩) β†’ P p) (p : 𝔓 X) :
                                                                  P p
                                                                  source
                                                                  theorem Construction.Ξ©_subset_cball {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                                                                  Construction.Ξ© p βŠ† Metric.ball (𝒬 p) 1
                                                                  source
                                                                  theorem Construction.Ξ©_disjoint_aux {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} (nmaxI : Β¬IsMax I) {y : { x : Θ X // x ∈ 𝓩 I }} {z : { x : Θ X // x ∈ 𝓩 I }} (hn : y β‰  z) :
                                                                  Disjoint (Metric.ball (↑y) Construction.CΞ©) (⋃ (z' : Θ X), ⋃ (x : z' ∈ ↑(𝓩 I.succ) ∩ Construction.Ω₁ ⟨I, z⟩), Construction.Ξ© ⟨I.succ, ⟨z', β‹―βŸ©βŸ©)
                                                                  source
                                                                  theorem Construction.Ξ©_disjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q✝ K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {q : 𝔓 X} (hn : p β‰  q) (hπ“˜ : π“˜ p = π“˜ q) :
                                                                  Disjoint (Construction.Ξ© p) (Construction.Ξ© q)
                                                                  source
                                                                  theorem Construction.Ξ©_biUnion {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {I : Grid X} :
                                                                  ↑Q.range βŠ† ⋃ p ∈ π“˜ ⁻¹' {I}, Construction.Ξ© p
                                                                  source
                                                                  @[irreducible]
                                                                  theorem Construction.Ξ©_RFD {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q✝ K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {q : 𝔓 X} (hπ“˜ : π“˜ p ≀ π“˜ q) :
                                                                  Disjoint (Construction.Ξ© p) (Construction.Ξ© q) ∨ Construction.Ξ© q βŠ† Construction.Ξ© p
                                                                  source
                                                                  def tile_existence (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ : X β†’ β„€} {Οƒβ‚‚ : X β†’ β„€} {F : Set X} {G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] :
                                                                  TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)
                                                                  Equations
                                                                  Instances For