Carleson.TileStructure

source

class PreTileStructure {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances 𝕜 X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam ℕ) (κ : outParam ℝ) (S : outParam ℕ) (o : outParam X) extends GridStructure :

Type (u + 1)

Grid : Type u
fintype_Grid : Fintype (GridStructure.Grid X A)
coeGrid : GridStructure.Grid X A → Set X
s : GridStructure.Grid X A → ℤ
c : GridStructure.Grid X A → X
inj : Function.Injective fun (i : GridStructure.Grid X A) => (↑i, GridStructure.s i)
range_s_subset : Set.range GridStructure.s ⊆ Set.Icc (-↑S) ↑S
topCube : GridStructure.Grid X A
s_topCube : GridStructure.s topCube = ↑S
c_topCube : GridStructure.c topCube = o
subset_topCube : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ ↑topCube
Grid_subset_biUnion : ∀ {i : GridStructure.Grid X A}, ∀ k ∈ Set.Ico (-↑S) (GridStructure.s i), ↑i ⊆ ⋃ j ∈ GridStructure.s ⁻¹' {k}, ↑j
fundamental_dyadic' : ∀ {i j : GridStructure.Grid X A}, GridStructure.s i ≤ GridStructure.s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
ball_subset_Grid : ∀ {i : GridStructure.Grid X A}, Metric.ball (GridStructure.c i) (↑D ^ GridStructure.s i / 4) ⊆ ↑i
Grid_subset_ball : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ Metric.ball (GridStructure.c i) (4 * ↑D ^ GridStructure.s i)
small_boundary : ∀ {i : GridStructure.Grid X A} {t : NNReal}, ↑D ^ (-↑S - GridStructure.s i) ≤ t → MeasureTheory.volume.real {x : X | x ∈ ↑i ∧ EMetric.infEdist x (↑i)ᶜ ≤ ↑t * ↑D ^ GridStructure.s i} ≤ 2 * ↑t ^ κ * MeasureTheory.volume.real ↑i
coeGrid_measurable : ∀ {i : GridStructure.Grid X A}, MeasurableSet ↑i
𝔓 : Type u
fintype_𝔓 : Fintype (PreTileStructure.𝔓 𝕜 X A)
𝓘 : PreTileStructure.𝔓 𝕜 X A → GridStructure.Grid X A
surjective_𝓘 : Function.Surjective PreTileStructure.𝓘
𝒬 : PreTileStructure.𝔓 𝕜 X A → Θ X
range_𝒬 : Set.range 𝒬 ⊆ Set.range ⇑Q

Instances

source

theorem PreTileStructure.surjective_𝓘 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances 𝕜 X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : PreTileStructure Q D κ S o] :

Function.Surjective PreTileStructure.𝓘

source

theorem PreTileStructure.range_𝒬 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances 𝕜 X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : PreTileStructure Q D κ S o] :

Set.range 𝒬 ⊆ Set.range ⇑Q

source

def 𝔓 {𝕜 : Type u_1} [RCLike 𝕜] (X : Type u) {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] :

Type u

Equations

𝔓 X = PreTileStructure.𝔓 𝕜 X A

Instances For

source

instance instFintype𝔓 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] :

Fintype (𝔓 X)

Equations

instFintype𝔓 = PreTileStructure.fintype_𝔓

source

def 𝓘 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] :

𝔓 X → Grid X

Equations

𝓘 = PreTileStructure.𝓘

Instances For

source

theorem surjective_𝓘 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] :

Function.Surjective 𝓘

source

instance instInhabited𝔓 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] :

Inhabited (𝔓 X)

Equations

instInhabited𝔓 = { default := ⋯.choose }

source

def 𝔠 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] (p : 𝔓 X) :

Equations

𝔠 p = c (𝓘 p)

Instances For

source

def 𝔰 {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {D : ℕ} {κ : ℝ} {S : ℕ} {o : X} [FunctionDistances 𝕜 X] {Q : MeasureTheory.SimpleFunc X (Θ X)} [PreTileStructure Q D κ S o] (p : 𝔓 X) :

ℤ

Equations

𝔰 p = s (𝓘 p)

Instances For

source

class TileStructure {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] (Q : outParam (MeasureTheory.SimpleFunc X (Θ X))) (D : outParam ℕ) (κ : outParam ℝ) (S : outParam ℕ) (o : outParam X) extends PreTileStructure :

Type (u + 1)

A tile structure.

Grid : Type u
fintype_Grid : Fintype (GridStructure.Grid X A)
coeGrid : GridStructure.Grid X A → Set X
s : GridStructure.Grid X A → ℤ
c : GridStructure.Grid X A → X
inj : Function.Injective fun (i : GridStructure.Grid X A) => (↑i, GridStructure.s i)
range_s_subset : Set.range GridStructure.s ⊆ Set.Icc (-↑S) ↑S
topCube : GridStructure.Grid X A
s_topCube : GridStructure.s topCube = ↑S
c_topCube : GridStructure.c topCube = o
subset_topCube : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ ↑topCube
Grid_subset_biUnion : ∀ {i : GridStructure.Grid X A}, ∀ k ∈ Set.Ico (-↑S) (GridStructure.s i), ↑i ⊆ ⋃ j ∈ GridStructure.s ⁻¹' {k}, ↑j
fundamental_dyadic' : ∀ {i j : GridStructure.Grid X A}, GridStructure.s i ≤ GridStructure.s j → ↑i ⊆ ↑j ∨ Disjoint ↑i ↑j
ball_subset_Grid : ∀ {i : GridStructure.Grid X A}, Metric.ball (GridStructure.c i) (↑D ^ GridStructure.s i / 4) ⊆ ↑i
Grid_subset_ball : ∀ {i : GridStructure.Grid X A}, ↑i ⊆ Metric.ball (GridStructure.c i) (4 * ↑D ^ GridStructure.s i)
small_boundary : ∀ {i : GridStructure.Grid X A} {t : NNReal}, ↑D ^ (-↑S - GridStructure.s i) ≤ t → MeasureTheory.volume.real {x : X | x ∈ ↑i ∧ EMetric.infEdist x (↑i)ᶜ ≤ ↑t * ↑D ^ GridStructure.s i} ≤ 2 * ↑t ^ κ * MeasureTheory.volume.real ↑i
coeGrid_measurable : ∀ {i : GridStructure.Grid X A}, MeasurableSet ↑i
𝔓 : Type u
fintype_𝔓 : Fintype (PreTileStructure.𝔓 ℝ X A)
𝓘 : PreTileStructure.𝔓 ℝ X A → GridStructure.Grid X A
surjective_𝓘 : Function.Surjective PreTileStructure.𝓘
𝒬 : PreTileStructure.𝔓 ℝ X A → Θ X
range_𝒬 : Set.range 𝒬 ⊆ Set.range ⇑Q
Ω : PreTileStructure.𝔓 ℝ X A → Set (Θ X)
biUnion_Ω : ∀ {i : GridStructure.Grid X A}, Set.range ⇑Q ⊆ ⋃ p ∈ PreTileStructure.𝓘 ⁻¹' {i}, Ω p
disjoint_Ω : ∀ {p p' : PreTileStructure.𝔓 ℝ X A}, p ≠ p' → PreTileStructure.𝓘 p = PreTileStructure.𝓘 p' → Disjoint (Ω p) (Ω p')
relative_fundamental_dyadic : ∀ {p p' : PreTileStructure.𝔓 ℝ X A}, PreTileStructure.𝓘 p ≤ PreTileStructure.𝓘 p' → Disjoint (Ω p) (Ω p') ∨ Ω p' ⊆ Ω p
cball_subset : ∀ {p : 𝔓 X}, Metric.ball (𝒬 p) 5⁻¹ ⊆ Ω p
subset_cball : ∀ {p : PreTileStructure.𝔓 ℝ X A}, Ω p ⊆ Metric.ball (𝒬 p) 1

Instances

source

theorem TileStructure.biUnion_Ω {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : TileStructure Q D κ S o] {i : GridStructure.Grid X A} :

Set.range ⇑Q ⊆ ⋃ p ∈ PreTileStructure.𝓘 ⁻¹' {i}, Ω p

source

theorem TileStructure.disjoint_Ω {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : TileStructure Q D κ S o] {p : PreTileStructure.𝔓 ℝ X A} {p' : PreTileStructure.𝔓 ℝ X A} (h : p ≠ p') (hp : PreTileStructure.𝓘 p = PreTileStructure.𝓘 p') :

Disjoint (Ω p) (Ω p')

source

theorem TileStructure.relative_fundamental_dyadic {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : TileStructure Q D κ S o] {p : PreTileStructure.𝔓 ℝ X A} {p' : PreTileStructure.𝔓 ℝ X A} (h : PreTileStructure.𝓘 p ≤ PreTileStructure.𝓘 p') :

Disjoint (Ω p) (Ω p') ∨ Ω p' ⊆ Ω p

source

theorem TileStructure.cball_subset {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : TileStructure Q D κ S o] {p : 𝔓 X} :

Metric.ball (𝒬 p) 5⁻¹ ⊆ Ω p

source

theorem TileStructure.subset_cball {X : Type u} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] [FunctionDistances ℝ X] {Q : outParam (MeasureTheory.SimpleFunc X (Θ X))} {D : outParam ℕ} {κ : outParam ℝ} {S : outParam ℕ} {o : outParam X} [self : TileStructure Q D κ S o] {p : PreTileStructure.𝔓 ℝ X A} :

Ω p ⊆ Metric.ball (𝒬 p) 1

source

def «termDist_(_)» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def «termNndist_(_)» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def «termBall_(_)» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem dist_𝓘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {f : Θ X} {g : Θ X} (p : 𝔓 X) :

dist f g = dist f g

source

@[simp]

theorem nndist_𝓘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {f : Θ X} {g : Θ X} (p : 𝔓 X) :

nndist f g = nndist f g

source

@[simp]

theorem ball_𝓘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {f : Θ X} (p : 𝔓 X) {r : ℝ} :

Metric.ball f r = Metric.ball f r

source

@[simp]

theorem cball_subset {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :

Metric.ball (𝒬 p) 5⁻¹ ⊆ Ω p

source

@[simp]

theorem subset_cball {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :

Ω p ⊆ Metric.ball (𝒬 p) 1

source

theorem cball_disjoint {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') :

Disjoint (Metric.ball (𝒬 p) 5⁻¹) (Metric.ball (𝒬 p') 5⁻¹)

source

def E {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

Set X

The set E defined in Proposition 2.0.2.

Equations

E p = {x : X | x ∈ 𝓘 p ∧ Q x ∈ Ω p ∧ 𝔰 p ∈ Set.Icc (σ₁ x) (σ₂ x)}

Instances For

source

def carlesonOn {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) (f : X → ℂ) :

X → ℂ

The operator T_𝔭 defined in Proposition 2.0.2, considered on the set F. It is the map T ∘ (1_F * ·) : f ↦ T (1_F * f), also denoted T1_F The operator T in Proposition 2.0.2 is therefore applied to (F := Set.univ)`.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def carlesonSum {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) :

ℂ

The operator T_ℭ f defined at the bottom of Section 7.4. We will use this in other places of the formalization as well.

Equations

carlesonSum ℭ f x = ∑ p ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ ℭ) Finset.univ, carlesonOn p f x

Instances For

source

theorem carlesonOn_def' {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) (f : X → ℂ) :

carlesonOn p f = (E p).indicator fun (x : X) => ∫ (y : X), Ks (𝔰 p) x y * f y * Complex.exp (Complex.I * (↑((Q x) y) - ↑((Q x) x)))

source

def TileLike (X : Type u_1) [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

Type u_1

Equations

TileLike X = (Grid X × (Set (Θ X))ᵒᵈ)

Instances For

source

def TileLike.fst {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (x : TileLike X) :

Grid X

Equations

x.fst = x.1

Instances For

source

def TileLike.snd {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (x : TileLike X) :

Set (Θ X)

Equations

x.snd = x.2

Instances For

source

@[simp]

theorem TileLike.fst_mk {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (x : Grid X) (y : Set (Θ X)) :

TileLike.fst (x, y) = x

source

@[simp]

theorem TileLike.snd_mk {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (x : Grid X) (y : Set (Θ X)) :

TileLike.snd (x, y) = y

source

instance instPartialOrderTileLike {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

PartialOrder (TileLike X)

Equations

instPartialOrderTileLike = id inferInstance

source

theorem TileLike.le_def {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (x : TileLike X) (y : TileLike X) :

x ≤ y ↔ x.fst ≤ y.fst ∧ y.snd ⊆ x.snd

source

def toTileLike {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

TileLike X

Equations

toTileLike p = (𝓘 p, Ω p)

Instances For

source

@[simp]

theorem toTileLike_fst {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

(toTileLike p).fst = 𝓘 p

source

@[simp]

theorem toTileLike_snd {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

(toTileLike p).snd = Ω p

source

def smul {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :

TileLike X

This is not defined as such in the blueprint, but λp ≲ λ'p' can be written using smul l p ≤ smul l' p'. Beware: smul 1 p is very different from toTileLike p.

Equations

smul l p = (𝓘 p, Metric.ball (𝒬 p) l)

Instances For

source

@[simp]

theorem smul_fst {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :

(smul l p).fst = 𝓘 p

source

@[simp]

theorem smul_snd {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :

(smul l p).snd = Metric.ball (𝒬 p) l

source

theorem smul_mono_left {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {l : ℝ} {l' : ℝ} {p : 𝔓 X} (h : l ≤ l') :

smul l' p ≤ smul l p

source

theorem smul_le_toTileLike {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :

smul 1 p ≤ toTileLike p

source

theorem toTileLike_le_smul {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :

toTileLike p ≤ smul 5⁻¹ p

source

theorem 𝒬_mem_Ω {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} :

𝒬 p ∈ Ω p

source

theorem 𝒬_inj {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (h : 𝒬 p = 𝒬 p') (h𝓘 : 𝓘 p = 𝓘 p') :

p = p'

source

theorem toTileLike_injective {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

Function.Injective fun (p : 𝔓 X) => toTileLike p

source

instance instPartialOrder𝔓Real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

PartialOrder (𝔓 X)

Equations

instPartialOrder𝔓Real = PartialOrder.lift toTileLike ⋯

source

theorem 𝔓.le_def {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q✝ K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {q : 𝔓 X} :

p ≤ q ↔ toTileLike p ≤ toTileLike q

source

theorem 𝔓.le_def' {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q✝ K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {q : 𝔓 X} :

p ≤ q ↔ 𝓘 p ≤ 𝓘 q ∧ Ω q ⊆ Ω p

source

theorem 𝓘_strictMono {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

StrictMono 𝓘

source

theorem eq_of_𝓘_eq_𝓘_of_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (h1 : 𝓘 p = 𝓘 p') (h2 : p ≤ p') :

p = p'

source

theorem not_lt_of_𝓘_eq_𝓘 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (h1 : 𝓘 p = 𝓘 p') :

¬p < p'

source

theorem 𝓘_strict_mono {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] :

StrictMono 𝓘

source

theorem smul_mono {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} {m : ℝ} {m' : ℝ} {n : ℝ} {n' : ℝ} (hp : smul n p ≤ smul m p') (hm : m' ≤ m) (hn : n ≤ n') :

smul n' p ≤ smul m' p'

Lemma 5.3.1

source

theorem smul_C2_1_2 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (m : ℝ) {n : ℝ} {k : ℝ} (hk : 0 < k) (hp : 𝓘 p ≠ 𝓘 p') (hl : smul n p ≤ smul k p') :

smul (n + C2_1_2 a * m) p ≤ smul m p'

Lemma 5.3.2 (generalizing 1 to k > 0)

source

def C5_3_3 (a : ℕ) :

ℝ

The constraint on λ in the first part of Lemma 5.3.3.

Equations

C5_3_3 a = (1 - C2_1_2 a)⁻¹

Instances For

source

theorem C5_3_3_le {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] :

C5_3_3 a ≤ 11 / 10

source

theorem wiggle_order_11_10 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) :

smul n p ≤ smul n p'

Lemma 5.3.3, Equation (5.3.3)

source

theorem wiggle_order_100 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (hp : smul 10 p ≤ smul 1 p') (hn : 𝓘 p ≠ 𝓘 p') :

smul 100 p ≤ smul 100 p'

Lemma 5.3.3, Equation (5.3.4)

source

theorem wiggle_order_500 {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {p' : 𝔓 X} (hp : smul 2 p ≤ smul 1 p') (hn : 𝓘 p ≠ 𝓘 p') :

smul 4 p ≤ smul 500 p'

Lemma 5.3.3, Equation (5.3.5)

source

def C5_3_2 (a : ℕ) :

ℝ

Equations

C5_3_2 a = 2 ^ (-95 * ↑a)

Instances For

source

def TileLike.toTile {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (t : TileLike X) :

Set (X × Θ X)

Equations

t.toTile = ↑t.fst ×ˢ t.snd

Instances For

source

def TileLike.toSet {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (t : TileLike X) :

Set X

From a TileLike, we can construct a set. This is used in the definitions E₁ and E₂.

Equations

t.toSet = ↑t.1 ∩ G ∩ ⇑Q ⁻¹' t.2

Instances For

source

def E₁ {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

Set X

Equations

E₁ p = (toTileLike p).toSet

Instances For

source

def E₂ {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (l : ℝ) (p : 𝔓 X) :

Set X

Equations

E₂ l p = (smul l p).toSet

Instances For

source

theorem E₁_subset {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (p : 𝔓 X) :

E₁ p ⊆ ↑(𝓘 p)

𝔓(𝔓') in the blueprint is lowerClosure 𝔓' in Lean.

source

def dens₁ {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (𝔓' : Set (𝔓 X)) :

ENNReal

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def dens₂ {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (𝔓' : Set (𝔓 X)) :

ENNReal

This density is defined to live in ℝ≥0∞. Use ENNReal.toReal to get a real number.

Equations

dens₂ 𝔓' = ⨆ p ∈ 𝔓', ⨆ (r : ℝ), ⨆ (_ : r ≥ 4 * ↑(defaultD a) ^ 𝔰 p), MeasureTheory.volume (F ∩ Metric.ball (𝔠 p) r) / MeasureTheory.volume (Metric.ball (𝔠 p) r)

Instances For

source

theorem isAntichain_iff_disjoint {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (𝔄 : Set (𝔓 X)) :

IsAntichain (fun (x1 x2 : TileLike X) => x1 ≤ x2) (toTileLike '' 𝔄) ↔ ∀ (p p' : 𝔓 X), p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' → Disjoint (toTileLike p).toTile (toTileLike p').toTile

Stack sizes #

source

def stackSize {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (C : Set (𝔓 X)) (x : X) :

ℕ

The number of tiles p in s whose underlying cube 𝓘 p contains x.

Equations

stackSize C x = ∑ p ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ C) Finset.univ, (↑(𝓘 p)).indicator 1 x

Instances For

source

theorem stackSize_setOf_add_stackSize_setOf_not {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {x : X} {P : 𝔓 X → Prop} :

stackSize {p : 𝔓 X | p ∈ C ∧ P p} x + stackSize {p : 𝔓 X | p ∈ C ∧ ¬P p} x = stackSize C x

source

theorem stackSize_congr {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {x : X} {x' : X} (h : ∀ p ∈ C, x ∈ ↑(𝓘 p) ↔ x' ∈ ↑(𝓘 p)) :

stackSize C x = stackSize C x'

source

theorem stackSize_mono {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} {C' : Set (𝔓 X)} {x : X} (h : C ⊆ C') :

stackSize C x ≤ stackSize C' x

source

theorem stackSize_real {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] (C : Set (𝔓 X)) (x : X) :

↑(stackSize C x) = ∑ p ∈ Finset.filter (fun (p : 𝔓 X) => p ∈ C) Finset.univ, (↑(𝓘 p)).indicator 1 x

source

theorem stackSize_measurable {X : Type u_1} [PseudoMetricSpace X] {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ : X → ℤ} {σ₂ : X → ℤ} {F : Set X} {G : Set X} [ProofData a q K σ₁ σ₂ F G] [TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)] {C : Set (𝔓 X)} :

Measurable fun (x : X) => ↑(stackSize C x)