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 β†’ β„€} {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
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
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
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
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 (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 β†’ β„€} {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.
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
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
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 (y : X) => Metric.ball y (↑(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 (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 β†’ β„€} {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
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
source
def Encodable.linearOrder {Ξ± : Type u_2} (i : Encodable Ξ±) :
LinearOrder Ξ±
Equations
source
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
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
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
@[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.
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
  • One or more equations did not get rendered due to their size.
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'
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
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
@[irreducible]
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
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
source
def ShortVariables.termK' :
Lean.ParserDescr
Equations
source
theorem K_pos {a : β„•} :
0 < ↑const_K
source
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
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
theorem one_lt_realD (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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
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 two_le_a (X : Type u_1) {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F 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 β†’ β„€} {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 ∧ 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 β†’ β„€} {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 ∧ EMetric.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
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 ∧ HEq x.y y.y
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) :
HEq x.y y.y β†’ x = y
source
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
source
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
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
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
def 𝓓_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)
Equations
  • β‹― = β‹―
source
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.

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

source
def C𝓩 :
ℝ

The constant appearing in 4.2.2 (3 / 10).

Equations
source
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
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
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
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 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 { x : Θ X // x ∈ 𝓩 I }
Equations
source
def C4_2_1 :
ℝ

7 / 10

Equations
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
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.
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.
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 { x : Θ X // x ∈ 𝓩 I }) ⟨z, hz⟩))
source
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
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 : { x : Θ X // x ∈ 𝓩 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 : { x : Θ X // x ∈ 𝓩 I }), Ω₁ ⟨I, f⟩

Equation (4.2.5)

source
def Construction.CΞ© :
ℝ

1 / 5

Equations
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.
source
@[irreducible]
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 : { 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 β†’ β„€} {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 : { x : Θ X // x ∈ 𝓩 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
@[irreducible]
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
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