Documentation

Carleson.TileExistence

source
theorem ball_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
noncomputable def J' (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
    2 ^ J' X = 8 * nnD a ^ (2 * defaultS X)
    source
    noncomputable def C4_1_1 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 (x : X) => Metric.ball x (↑(defaultD a) ^ k)) :
      ↑Y.encard ≀ ↑(C4_1_1 X)
      source
      def property_set (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
        theorem zorn_apply_maximal_set (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
        source
        noncomputable def Yk (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
        Set X
        Equations
        Instances For
          source
          theorem Yk_pairwise {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
          (Yk X k).PairwiseDisjoint fun (x : X) => Metric.ball x (↑(defaultD a) ^ k)
          source
          theorem Yk_subset {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 (x : X) => Metric.ball x (↑(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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
          (Yk X k).Countable
          source
          @[implicit_reducible]
          noncomputable def Yk_encodable (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (k : β„€) :
          Encodable ↑(Yk X k)
          Equations
          Instances For
            source
            @[implicit_reducible]
            def Encodable.linearOrder {Ξ± : Type u_2} (i : Encodable Ξ±) :
            LinearOrder Ξ±
            Equations
            Instances For
              source
              @[instance_reducible]
              noncomputable instance instLinearOrderElemYk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} :
              WellFoundedLT ↑(Yk X k)
              source
              @[instance_reducible]
              noncomputable def instSizeOfElemYk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} :
              SizeOf ↑(Yk X k)
              Equations
              Instances For
                source
                theorem I_induction_proof {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                theorem aux {s k : β„€} (h1 : 0 ≀ s + (k - 1)) :
                (s + (k - 1)).toNat < (s + k).toNat
                source
                @[irreducible]
                def I1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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
                    @[irreducible]
                    def Xk {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                        theorem I1_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                        theorem I2_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                        theorem Xk_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) :
                        MeasurableSet (Xk hk)
                        source
                        theorem I3_measurableSet {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                        theorem I1_prop_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) {x : X} {y1 y2 : ↑(Yk X k)} :
                        x ∈ I1 hk y1 ∩ I1 hk y2 β†’ y1 = y2
                        source
                        theorem I3_prop_1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {k : β„€} (hk : -↑(defaultS X) ≀ k) {x : X} {y1 y2 : ↑(Yk X k)} :
                        x ∈ I3 hk y1 ∩ I3 hk y2 β†’ y1 = y2
                        source
                        theorem I3_prop_3_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                        theorem I2_prop_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                        theorem I3_prop_2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                        theorem dyadic_property {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 transitive_boundary' {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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
                          Instances For
                            source
                            def ShortVariables.termK' :
                            Lean.ParserDescr
                            Equations
                            Instances For
                              source
                              theorem K_pos {a : β„•} :
                              0 < ↑const_K
                              source
                              noncomputable def C4_1_7 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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
                                noncomputable def const_n (a : β„•) {t : ℝ} (_ht : t ∈ Set.Ioo 0 1) :
                                β„•
                                Equations
                                Instances For
                                  source
                                  theorem prefloor_nonneg (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 kappa_le_log2D_inv_mul_K_inv (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 ∧ Metric.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 β†’ β„€} {F 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 ∧ Metric.infEDist x (I3 hk y)ᢜ ≀ ↑t * ↑(defaultD a) ^ k} ≀ 2 * ↑t ^ defaultΞΊ a * MeasureTheory.volume.real (I3 hk y)
                                  source
                                  structure 𝓓 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                  Type u_1
                                  Instances For
                                    source
                                    theorem 𝓓.ext {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} {inst✝ : PseudoMetricSpace X} {inst✝¹ : ProofData a q K σ₁ Οƒβ‚‚ F G} {x y : 𝓓 X} (k : x.k = y.k) :
                                    x.y ≍ y.y β†’ x = y
                                    source
                                    theorem 𝓓.ext_iff {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} {inst✝ : PseudoMetricSpace X} {inst✝¹ : ProofData a q K σ₁ Οƒβ‚‚ F G} {x y : 𝓓 X} :
                                    x = y ↔ x.k = y.k ∧ x.y ≍ y.y
                                    source
                                    noncomputable def max_𝓓 (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                    𝓓 X
                                    Equations
                                    Instances For
                                      source
                                      noncomputable def 𝓓.coe {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (z : 𝓓 X) :
                                      Set X
                                      Equations
                                      Instances For
                                        source
                                        def forget_map (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] (x : 𝓓 X) :
                                        (k : ↑(Set.Icc (-↑(defaultS X)) ↑(defaultS X))) Γ— ↑(Yk X ↑k)
                                        Equations
                                        Instances For
                                          source
                                          theorem forget_map_inj {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                          Function.Injective (forget_map X)
                                          source
                                          theorem 𝓓_finite (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] :
                                          Finite (𝓓 X)
                                          source
                                          @[implicit_reducible]
                                          noncomputable def grid_existence (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                                            noncomputable def C𝓩 :
                                            ℝ

                                            The constant appearing in 4.2.2 (3 / 10).

                                            Equations
                                            Instances For
                                              source
                                              noncomputable def 𝓩_cands {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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
                                                noncomputable def 𝓩 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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) => ball_{c I, ↑(defaultD a) ^ s I / 4} x C𝓩) ∧ βˆ€ z ∈ 𝓩_cands I, z.card ≀ (𝓩 I).card
                                                  source
                                                  theorem 𝓩_subset {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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) => ball_{c I, ↑(defaultD a) ^ s I / 4} x C𝓩
                                                  source
                                                  theorem 𝓩_max_card {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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_reducible]
                                                  noncomputable instance instInhabitedSubtypeΘRealMemFinset𝓩 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†₯(𝓩 I)
                                                  Equations
                                                  source
                                                  noncomputable def C4_2_1 :
                                                  ℝ

                                                  7 / 10

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem frequency_ball_cover {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1

                                                    Equation (4.2.3), Lemma 4.2.1

                                                    source
                                                    @[instance_reducible]
                                                    noncomputable def tileData_existence {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 β†’ β„€} {F 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 (Ω₁_aux I k) (Ω₁_aux I l)
                                                        source
                                                        theorem Construction.disjoint_ball_Ω₁_aux {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 z' : Θ X} (hz : z ∈ 𝓩 I) (hz' : z' ∈ 𝓩 I) (hn : z β‰  z') :
                                                        Disjoint (ball_{c I, ↑(defaultD a) ^ s I / 4} z' C𝓩) (Ω₁_aux I ↑((Finite.equivFin β†₯(𝓩 I)) ⟨z, hz⟩))
                                                        source
                                                        noncomputable def Construction.Ω₁ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {F 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 g : β†₯(𝓩 I)} (h : (Ω₁ ⟨I, f⟩ ∩ Ω₁ ⟨I, g⟩).Nonempty) :
                                                          f = g

                                                          Lemma 4.2.2

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

                                                          Equation (4.2.6), first inclusion

                                                          source
                                                          theorem Construction.Ω₁_subset_ball {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :
                                                          Ω₁ p βŠ† ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 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 β†’ β„€} {F 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, ball_{c I, ↑(defaultD a) ^ s I / 4} z C4_2_1 βŠ† ⋃ (f : β†₯(𝓩 I)), Ω₁ ⟨I, f⟩

                                                          Equation (4.2.5)

                                                          source
                                                          noncomputable def Construction.CΞ© :
                                                          ℝ

                                                          1 / 5

                                                          Equations
                                                          Instances For
                                                            source
                                                            @[irreducible]
                                                            def Construction.Ξ© {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
                                                              theorem Construction.𝔓_induction {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 : β†₯(𝓩 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 β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :
                                                              Ξ© p βŠ† ball_{𝔠 p, ↑(defaultD a) ^ 𝔰 p / 4} (𝒬 p) 1
                                                              source
                                                              theorem Construction.Ξ©_disjoint_aux {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 z : β†₯(𝓩 I)} (hn : y β‰  z) :
                                                              Disjoint (ball_{c I, ↑(defaultD a) ^ s I / 4} (↑y) CΞ©) (⋃ (z' : Θ X), ⋃ (x : z' ∈ ↑(𝓩 I.succ) ∩ Ω₁ ⟨I, z⟩), Ξ© ⟨I.succ, ⟨z', β‹―βŸ©βŸ©)
                                                              source
                                                              theorem Construction.Ξ©_disjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p p' : 𝔓 X} (hn : p β‰  p') (hπ“˜ : π“˜ p = π“˜ p') :
                                                              Disjoint (Ξ© p) (Ξ© p')
                                                              source
                                                              theorem Construction.Ξ©_biUnion {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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}, Ξ© p
                                                              source
                                                              theorem Construction.Ξ©_RFD {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [GridStructure X (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p q✝ : 𝔓 X} (hπ“˜ : π“˜ p ≀ π“˜ q✝) :
                                                              Disjoint (Ξ© p) (Ξ© q✝) ∨ Ξ© q✝ βŠ† Ξ© p
                                                              source
                                                              @[implicit_reducible]
                                                              noncomputable def tile_existence (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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