Section 5.3 #
Note: the lemmas 5.3.1-5.3.3 are in TileStructure.
Section 5.4 and Lemma 5.1.2 #
def
ℭ₆
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
:
The subset ℭ₆(k, n, j) of ℭ₅(k, n, j), given above (5.4.1).
Instances For
def
𝔗₁
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
(u : 𝔓 X)
:
The subset 𝔗₁(u) of ℭ₁(k, n, j), given in (5.4.1).
In lemmas, we will assume u ∈ 𝔘₁ k n l
Instances For
theorem
𝓘_lt_of_mem_𝔗₁
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{p : 𝔓 X}
{p' : 𝔓 X}
(h : p ∈ 𝔗₁ k n j p')
:
def
𝔘₂
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
:
The subset 𝔘₂(k, n, j) of 𝔘₁(k, n, j), given in (5.4.2).
Instances For
def
URel
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
(u : 𝔓 X)
(u' : 𝔓 X)
:
The relation ∼ defined below (5.4.2). It is an equivalence relation on 𝔘₂ k n j.
Instances For
theorem
URel.not_disjoint
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{u : 𝔓 X}
{u' : 𝔓 X}
(hu : u ∈ 𝔘₂ k n j)
(hu' : u' ∈ 𝔘₂ k n j)
(huu' : URel k n j u u')
:
¬Disjoint (Metric.ball (𝒬 u) 100) (Metric.ball (𝒬 u') 100)
Lemma 5.4.1, part 2.
theorem
URel.eq
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{u : 𝔓 X}
{u' : 𝔓 X}
(hu : u ∈ 𝔘₂ k n j)
(hu' : u' ∈ 𝔘₂ k n j)
(huu' : URel k n j u u')
:
Lemma 5.4.1, part 1.
theorem
urel_of_not_disjoint
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{x : 𝔓 X}
{y : 𝔓 X}
(my : y ∈ 𝔘₂ k n j)
(xny : x ≠ y)
(xye : 𝓘 x = 𝓘 y)
(nd : ¬Disjoint (Metric.ball (𝒬 x) 100) (Metric.ball (𝒬 y) 100))
:
URel k n j y x
Helper for 5.4.2 that is also used in 5.4.9.
theorem
equivalenceOn_urel
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
:
EquivalenceOn (URel k n j) (𝔘₂ k n j)
Lemma 5.4.2.
def
𝔘₃
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
:
𝔘₃(k, n, j) ⊆ 𝔘₂ k n j is an arbitary set of representatives of URel on 𝔘₂ k n j,
given above (5.4.5).
Instances For
def
𝔗₂
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
(u : 𝔓 X)
:
The subset 𝔗₂(u) of ℭ₆(k, n, j), given in (5.4.5).
In lemmas, we will assume u ∈ 𝔘₃ k n l
Instances For
theorem
forest_geometry
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{p : 𝔓 X}
{u : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hp : p ∈ 𝔗₂ k n j u)
:
Lemma 5.4.4, verifying (2.0.32)
theorem
forest_convex
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{u : 𝔓 X}
:
(𝔗₂ k n j u).OrdConnected
Lemma 5.4.5, verifying (2.0.33)
theorem
forest_separation
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{p : 𝔓 X}
{u : 𝔓 X}
{u' : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hu' : u' ∈ 𝔘₃ k n j)
(huu' : u ≠ u')
(hp : p ∈ 𝔗₂ k n j u')
(h : 𝓘 p ≤ 𝓘 u)
:
Lemma 5.4.6, verifying (2.0.36)
Note: swapped u and u' to match (2.0.36)
theorem
forest_inner
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{p : 𝔓 X}
{u : 𝔓 X}
(hu : u ∈ 𝔘₃ k n j)
(hp : p ∈ 𝔗₂ k n j u)
:
Lemma 5.4.7, verifying (2.0.37)
theorem
forest_stacking
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
(x : X)
(hkn : k ≤ n)
:
Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34.
def
aux𝔘₄
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(s : Set (𝔓 X))
:
Pick a maximal subset of s satisfying ∀ x, stackSize s x ≤ 2 ^ n
Instances For
@[irreducible]
def
𝔘₄
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(j : ℕ)
(l : ℕ)
:
The sets (𝔘₄(k, n, j, l))_l form a partition of 𝔘₃ k n j.
Instances For
theorem
pairwiseDisjoint_𝔘₄
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
:
Set.univ.PairwiseDisjoint (𝔘₄ k n j)
Section 5.5 and Lemma 5.1.3 #
def
ℜ₁
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
:
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₁
Equations
Instances For
def
ℜ₂
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
:
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₂
Equations
Instances For
def
ℜ₃
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
:
The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃
Equations
Instances For
theorem
mem_iUnion_iff_mem_of_mem_ℭ
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{p : 𝔓 X}
{f : ℕ → ℕ → Set (𝔓 X)}
(hp : p ∈ ℭ k n ∧ k ≤ n)
(hf : ∀ (k n : ℕ), f k n ⊆ ℭ k n)
:
Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.1.
theorem
mem_iUnion_iff_mem_of_mem_ℭ₁
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{p : 𝔓 X}
{f : ℕ → Set (𝔓 X)}
(hp : p ∈ ℭ₁ k n j ∧ j ≤ 2 * n + 3)
(hf : ∀ (j : ℕ), f j ⊆ ℭ₁ k n j)
:
Lemma allowing to peel ⋃ (j ≤ 2 * n + 3) from unions in the proof of Lemma 5.5.1.
def
𝔏₀'
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
(k : ℕ)
(n : ℕ)
(l : ℕ)
:
The subset 𝔏₀(k, n, l) of 𝔏₀(k, n), given in Lemma 5.5.3.
We use the name 𝔏₀' in Lean. The indexing is off-by-one w.r.t. the blueprint
Instances For
theorem
pairwiseDisjoint_L0'
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
:
Set.univ.PairwiseDisjoint (𝔏₀' k n)
Part of Lemma 5.5.2
theorem
antichain_L0'
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{l : ℕ}
:
IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) (𝔏₀' k n l)
Part of Lemma 5.5.2
theorem
antichain_L2
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
:
IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) (𝔏₂ k n j)
Lemma 5.5.3
theorem
antichain_L1
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{l : ℕ}
:
IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) (𝔏₁ k n j l)
Part of Lemma 5.5.4
theorem
antichain_L3
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
{k : ℕ}
{n : ℕ}
{j : ℕ}
{l : ℕ}
:
IsAntichain (fun (x1 x2 : 𝔓 X) => x1 ≤ x2) (𝔏₃ k n j l)
Part of Lemma 5.5.4
Proposition 2.0.2 #
theorem
discrete_carleson
(X : Type u_1)
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[MetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
[TileStructure Q (defaultD a) (defaultκ a) (defaultS X) (cancelPt X)]
:
∃ (G' : Set X),
MeasurableSet G' ∧ 2 * MeasureTheory.volume G' ≤ MeasureTheory.volume G ∧ ∀ (f : X → ℂ),
Measurable f →
(∀ (x : X), ‖f x‖ ≤ F.indicator 1 x) →
∫⁻ (x : X) in G \ G', ↑‖carlesonSum Set.univ f x‖₊ ≤ ↑(C2_0_2 (↑a) (nnq X)) * MeasureTheory.volume G ^ (1 - q⁻¹) * MeasureTheory.volume F ^ q⁻¹