Documentation

Carleson.ForestOperator.LargeSeparation

Section 7.5 #

source
def TileStructure.Forest.𝓙₅ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : Forest X n) (u₁ uβ‚‚ : 𝔓 X) :
Set (Grid X)

The definition 𝓙' at the start of Section 7.5.1. We use a different notation to distinguish it from the 𝓙' used in Section 7.6

Equations
source
def TileStructure.Forest.Ο‡tilde {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] (J : Grid X) (u₁ : 𝔓 X) :
X β†’ NNReal

The definition of Ο‡-tilde, defined in the proof of Lemma 7.5.2

Equations
source
theorem TileStructure.Forest.Ο‡tilde_pos_iff {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u₁ : 𝔓 X} {x : X} {J : Grid X} :
0 < Ο‡tilde J u₁ x ↔ x ∈ π“˜ u₁ ∧ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)
source
theorem TileStructure.Forest.Ο‡tilde_le_eight {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u₁ : 𝔓 X} {x : X} {J : Grid X} :
Ο‡tilde J u₁ x ≀ 8
source
theorem TileStructure.Forest.four_lt_Ο‡tilde {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u₁ : 𝔓 X} {x : X} {J : Grid X} (xJ : x ∈ J) (xu : x ∈ π“˜ u₁) :
4 < Ο‡tilde J u₁ x
source
theorem TileStructure.Forest.dist_Ο‡tilde_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u₁ : 𝔓 X} {x x' : X} {J : Grid X} (mx : x ∈ π“˜ u₁) (mx' : x' ∈ π“˜ u₁) :
dist (Ο‡tilde J u₁ x) (Ο‡tilde J u₁ x') ≀ dist x x' / ↑(defaultD a) ^ s J
source
def TileStructure.Forest.Ο‡ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : Forest X n) (u₁ uβ‚‚ : 𝔓 X) (J : Grid X) (x : X) :
NNReal

The definition of Ο‡, defined in the proof of Lemma 7.5.2

Equations
source
def TileStructure.Forest.holderFunction {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} (t : Forest X n) (u₁ uβ‚‚ : 𝔓 X) (f₁ fβ‚‚ : X β†’ β„‚) (J : Grid X) (x : X) :
β„‚

The definition of h_J, defined in the proof of Section 7.5.2

Equations
  • One or more equations did not get rendered due to their size.
source
theorem TileStructure.Forest.IF_subset_THEN_distance_between_centers {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {J J' : Grid X} (subset : ↑J βŠ† ↑J') :
dist (c J) (c J') < 4 * ↑(defaultD a) ^ s J'
source
theorem TileStructure.Forest.IF_subset_THEN_not_disjoint {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {A B : Grid X} (h : ↑A βŠ† ↑B) :
Β¬Disjoint ↑B ↑A
source
theorem TileStructure.Forest.IF_disjoint_with_ball_THEN_distance_bigger_than_radius {X : Type u_1} [MetricSpace X] {J : X} {r : ℝ} {pSet : Set X} {p : X} (belongs : p ∈ pSet) (h : Disjoint (Metric.ball J r) pSet) :
dist J p β‰₯ r
source
theorem TileStructure.Forest.dist_triangle5 {X : Type u_1} [MetricSpace X] (a b c d e : X) :
dist a e ≀ dist a b + dist b c + dist c d + dist d e
source
theorem TileStructure.Forest.π“˜_subset_iUnion_𝓙_𝔖₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} :
↑(π“˜ u₁) βŠ† ⋃ J ∈ 𝓙 (t.𝔖₀ u₁ uβ‚‚), ↑J

Subsection 7.5.1 and Lemma 7.5.2 #

source
theorem TileStructure.Forest.union_𝓙₅ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) :
⋃ J ∈ t.𝓙₅ u₁ uβ‚‚, ↑J = ↑(π“˜ u₁)

Part of Lemma 7.5.1.

source
theorem TileStructure.Forest.pairwiseDisjoint_𝓙₅ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} :
(t.𝓙₅ u₁ uβ‚‚).PairwiseDisjoint fun (I : Grid X) => ↑I

Part of Lemma 7.5.1.

source
theorem TileStructure.Forest.four_lt_sum_Ο‡tilde {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hx : x ∈ π“˜ u₁) :
4 < βˆ‘ J' ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset, Ο‡tilde J' u₁ x
source
theorem TileStructure.Forest.bigger_than_𝓙_is_not_in_𝓙₀ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {𝔖 : Set (𝔓 X)} {A B : Grid X} (le : A ≀ B) (sle : s A < s B) (A_in : A ∈ 𝓙 𝔖) :
B βˆ‰ 𝓙₀ 𝔖
source
theorem TileStructure.Forest.moderate_scale_change {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J J' : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hJ' : J' ∈ t.𝓙₅ u₁ uβ‚‚) (hd : Β¬Disjoint (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (Metric.ball (c J') (8 * ↑(defaultD a) ^ s J'))) :
s J - 1 ≀ s J'

Lemma 7.5.3 (stated somewhat differently).

source
theorem TileStructure.Forest.sum_Ο‡ {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (x : X) :
βˆ‘ J ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset, t.Ο‡ u₁ uβ‚‚ J x = (↑(π“˜ u₁)).indicator 1 x

Part of Lemma 7.5.2.

source
theorem TileStructure.Forest.Ο‡_le_indicator {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x : X} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
t.Ο‡ u₁ uβ‚‚ J x ≀ (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)).indicator 1 x

Part of Lemma 7.5.2.

source
@[irreducible]
def TileStructure.Forest.C7_5_2 (a : β„•) :
NNReal

The constant used in dist_Ο‡_le. Has value 2 ^ (226 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.C7_5_2_def (a : β„•) :
C7_5_2 a = 2 ^ (226 * ↑a ^ 3)
source
theorem TileStructure.Forest.quarter_add_two_mul_D_mul_card_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J : Grid X} (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
1 / 4 + 2 * ↑(defaultD a) * ↑{J' ∈ (t.𝓙₅ u₁ uβ‚‚).toFinset | Β¬Disjoint (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (Metric.ball (c J') (8 * ↑(defaultD a) ^ s J'))}.card ≀ ↑(C7_5_2 a)
source
theorem TileStructure.Forest.dist_Ο‡_le {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (mx : x ∈ π“˜ u₁) (mx' : x' ∈ π“˜ u₁) :
dist (t.Ο‡ u₁ uβ‚‚ J x) (t.Ο‡ u₁ uβ‚‚ J x') ≀ ↑(C7_5_2 a) * dist x x' / ↑(defaultD a) ^ s J

Part of Lemma 7.5.2.

Subsection 7.5.2 and Lemma 7.5.4 #

source
theorem TileStructure.Forest.C7_5_5_def (a : β„•) :
C7_5_5 a = 2 ^ (151 * ↑a ^ 3)
source
@[irreducible]
def TileStructure.Forest.C7_5_5 (a : β„•) :
NNReal

The constant used in holder_correlation_tile. Has value 2 ^ (151 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.ψ_le_max {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] {x : ℝ} :
ψ (defaultD a) x ≀ 0 βŠ” (2 - 4 * x) ^ (↑a)⁻¹
source
theorem TileStructure.Forest.le_of_mem_E {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {x x' y : X} (hy : y ∈ E p) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
2 - 4 * (↑(defaultD a) ^ (-𝔰 p) * dist y x) ≀ dist x x' / ↑(defaultD a) ^ 𝔰 p * 4
source
theorem TileStructure.Forest.enorm_ψ_le_edist {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {x x' y : X} (my : y ∈ E p) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
β€–Οˆ (defaultD a) (↑(defaultD a) ^ (-𝔰 p) * dist y x)β€–β‚‘ ≀ 4 * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
source
theorem TileStructure.Forest.volume_xDsp_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {x : X} (hx : x ∈ π“˜ p) :
MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (3 * a) ≀ MeasureTheory.volume (Metric.ball x (↑(defaultD a) ^ 𝔰 p))

This bound is used in both nontrivial cases of Lemma 7.5.5.

source
theorem TileStructure.Forest.holder_correlation_tile_one {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) (hx' : x' βˆ‰ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
β€–adjointCarleson p f xβ€–β‚‘ ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
source
theorem TileStructure.Forest.integrable_adjointCarleson_interior {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {x : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) :
MeasureTheory.Integrable (fun (y : X) => Complex.exp (Complex.I * ↑((𝒬 u) x)) * ((starRingEnd β„‚) (Ks (𝔰 p) y x) * Complex.exp (Complex.I * (↑((Q y) y) - ↑((Q y) x))) * f y)) (MeasureTheory.volume.restrict (E p))
source
theorem TileStructure.Forest.holder_correlation_rearrange {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {u p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hf : MeasureTheory.BoundedCompactSupport f) :
edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ (∫⁻ (y : X) in E p, β€–f yβ€–β‚‘ * β€–Ks (𝔰 p) y xβ€–β‚‘ * β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€–β‚‘) + ∫⁻ (y : X) in E p, β€–f yβ€–β‚‘ * β€–Ks (𝔰 p) y x - Ks (𝔰 p) y x'β€–β‚‘

Sub-equations (7.5.10) and (7.5.11) in Lemma 7.5.5.

source
@[irreducible]
def TileStructure.Forest.Q7_5_5 (a : β„•) :
NNReal

Multiplicative factor for the bound on β€–- Q y x + Q y x' + 𝒬 u x - 𝒬 u x'β€–β‚‘.

Equations
source
theorem TileStructure.Forest.Q7_5_5_def (a : β„•) :
Q7_5_5 a = 10 * 2 ^ (6 * a)
source
theorem TileStructure.Forest.QQQQ_bound_real {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u p : 𝔓 X} {x x' y : X} (my : y ∈ E p) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€– ≀ ↑(Q7_5_5 a) * (dist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
source
theorem TileStructure.Forest.QQQQ_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u p : 𝔓 X} {x x' y : X} (my : y ∈ E p) (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
β€–-(Q y) x + (Q y) x' + (𝒬 u) x - (𝒬 u) x'β€–β‚‘ ≀ ↑(Q7_5_5 a) * (↑(nndist x x') / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹
source
theorem TileStructure.Forest.holder_correlation_tile_two {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f) (hx : x ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) (hx' : x' ∈ Metric.ball (𝔠 p) (5 * ↑(defaultD a) ^ 𝔰 p)) :
edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
source
theorem TileStructure.Forest.holder_correlation_tile {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u p : 𝔓 X} {x x' : X} {f : X β†’ β„‚} (hu : u ∈ t) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f) :
edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarleson p f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarleson p f x') ≀ ↑(C7_5_5 a) / MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p)) * (edist x x' / ↑(defaultD a) ^ 𝔰 p) ^ (↑a)⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘

Lemma 7.5.5.

source
theorem TileStructure.Forest.limited_scale_impact_first_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) :
s J ≀ 𝔰 p

Part of Lemma 7.5.6.

source
theorem TileStructure.Forest.limited_scale_impact_second_estimate {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) :
𝔰 p ≀ s J + 3

Part of Lemma 7.5.6.

source
theorem TileStructure.Forest.limited_scale_impact {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) :
𝔰 p ∈ Set.Icc (s J) (s J + 3)

Lemma 7.5.6.

source
theorem TileStructure.Forest.local_tree_control_sumsumsup {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
↑(⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ βˆ‘ k ∈ Finset.Icc (s J) (s J + 3), βˆ‘ p ∈ {p : 𝔓 X | 𝔰 p = k ∧ Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))}, ⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarleson p f xβ€–β‚‘
source
theorem TileStructure.Forest.local_tree_control_sup_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} {k : β„€} (mk : k ∈ Finset.Icc (s J) (s J + 3)) (mp : 𝔰 p = k ∧ Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J))) (nfm : Measurable fun (x : X) => β€–f xβ€–β‚‘) :
⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarleson p f xβ€–β‚‘ ≀ 2 ^ (103 * a ^ 3) * (MeasureTheory.volume (Metric.ball (c J) (16 * ↑(defaultD a) ^ k)))⁻¹ * ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘
source
theorem TileStructure.Forest.C7_5_7_def (a : β„•) :
C7_5_7 a = 2 ^ (104 * ↑a ^ 3)
source
@[irreducible]
def TileStructure.Forest.C7_5_7 (a : β„•) :
NNReal

The constant used in local_tree_control. Has value 2 ^ (104 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.local_tree_control {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
↑(⨆ x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ \ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ ↑(C7_5_7 a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

Lemma 7.5.7.

source
theorem TileStructure.Forest.scales_impacting_interval {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ p : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hp : p ∈ (fun (x : 𝔓 X) => t.𝔗 x) u₁ βˆͺ (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) (h : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) :
s J ≀ 𝔰 p

Lemma 7.5.8.

source
theorem TileStructure.Forest.volume_cpDsp_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {p : 𝔓 X} {J : Grid X} (hd : Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))) (hs : s J ≀ 𝔰 p) :
MeasureTheory.volume (Metric.ball (c J) (32 * ↑(defaultD a) ^ 𝔰 p)) / 2 ^ (4 * a) ≀ MeasureTheory.volume (Metric.ball (𝔠 p) (4 * ↑(defaultD a) ^ 𝔰 p))
source
theorem TileStructure.Forest.gtc_integral_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {f : X β†’ β„‚} {J : Grid X} {k : β„€} {β„­ : Set (𝔓 X)} (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) :
βˆ‘ p ∈ {p ∈ β„­.toFinset | Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) ∧ 𝔰 p = k}, ∫⁻ (x : X) in E p, β€–f xβ€–β‚‘ ≀ ∫⁻ (x : X) in Metric.ball (c J) (32 * ↑(defaultD a) ^ k), β€–f xβ€–β‚‘
source
theorem TileStructure.Forest.global_tree_control1_edist_part1 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu : u ∈ t) {β„­ : Set (𝔓 X)} (hβ„­ : β„­ βŠ† (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarlesonSum β„­ f x') ≀ ↑(C7_5_5 a) * 2 ^ (4 * a) * edist x x' ^ (↑a)⁻¹ * βˆ‘ k ∈ Finset.Icc (s J) ↑(defaultS X), ↑(defaultD a) ^ (-↑k / ↑a) * ⨍⁻ (x : X) in Metric.ball (c J) (32 * ↑(defaultD a) ^ k), β€–f xβ€–β‚‘ βˆ‚MeasureTheory.volume

Part 1 of equation (7.5.18) of Lemma 7.5.9.

source
theorem TileStructure.Forest.gtc_sum_Icc_le_two {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {J : Grid X} :
βˆ‘ k ∈ Finset.Icc (s J) ↑(defaultS X), ↑(defaultD a) ^ ((↑(s J) - ↑k) / ↑a) ≀ 2
source
@[irreducible]
def TileStructure.Forest.C7_5_9d (a : β„•) :
NNReal

The constant used in global_tree_control1_edist.

Equations
source
theorem TileStructure.Forest.C7_5_9d_def (a : β„•) :
C7_5_9d a = C7_5_5 a * 2 ^ (4 * a + 1)
source
theorem TileStructure.Forest.global_tree_control1_edist_part2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u : 𝔓 X} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu : u ∈ t) {β„­ : Set (𝔓 X)} (hβ„­ : β„­ βŠ† (fun (x : 𝔓 X) => t.𝔗 x) u) (hf : MeasureTheory.BoundedCompactSupport f) (hs : βˆ€ p ∈ β„­, Β¬Disjoint (Metric.ball (𝔠 p) (8 * ↑(defaultD a) ^ 𝔰 p)) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) β†’ s J ≀ 𝔰 p) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
edist (Complex.exp (Complex.I * ↑((𝒬 u) x)) * adjointCarlesonSum β„­ f x) (Complex.exp (Complex.I * ↑((𝒬 u) x')) * adjointCarlesonSum β„­ f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

Part 2 of equation (7.5.18) of Lemma 7.5.9.

source
theorem TileStructure.Forest.global_tree_control1_edist_left {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
edist (Complex.exp (Complex.I * ↑((𝒬 u₁) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f x) (Complex.exp (Complex.I * ↑((𝒬 u₁) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

Equation (7.5.18) of Lemma 7.5.9 for β„­ = t u₁.

source
theorem TileStructure.Forest.global_tree_control1_edist_right {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {x x' : X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) (hx : x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) (hx' : x' ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J)) :
edist (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x)) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f x) (Complex.exp (Complex.I * ↑((𝒬 uβ‚‚) x')) * adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f x') ≀ ↑(C7_5_9d a) * (edist x x' / ↑(defaultD a) ^ s J) ^ (↑a)⁻¹ * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

Equation (7.5.18) of Lemma 7.5.9 for β„­ = t uβ‚‚ ∩ 𝔖₀ t u₁ uβ‚‚.

source
theorem TileStructure.Forest.C7_5_9s_def (a : β„•) :
C7_5_9s a = C7_5_5 a * 2 ^ (4 * a + 2)
source
@[irreducible]
def TileStructure.Forest.C7_5_9s (a : β„•) :
NNReal

The constant used in global_tree_control1_supbound.

Equations
source
theorem TileStructure.Forest.global_tree_control1_supbound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (β„­ : Set (𝔓 X)) (hβ„­ : β„­ = (fun (x : 𝔓 X) => t.𝔗 x) u₁ ∨ β„­ = (fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum β„­ f xβ€–β‚‘ ≀ (β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum β„­ f xβ€–β‚‘) + ↑(C7_5_9s a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x

Equation (7.5.17) of Lemma 7.5.9.

source
theorem TileStructure.Forest.C7_5_10_def (a : β„•) :
C7_5_10 a = 2 ^ (155 * ↑a ^ 3)
source
@[irreducible]
def TileStructure.Forest.C7_5_10 (a : β„•) :
NNReal

The constant used in global_tree_control2. Has value 2 ^ (155 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.global_tree_control2 {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf : MeasureTheory.BoundedCompactSupport f) :
↑(⨆ x ∈ Metric.ball (c J) (8 * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) f xβ€–β‚Š) ≀ β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), ↑‖adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) f xβ€–β‚Š + ↑(C7_5_10 a) * β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (fun (x : X) => β€–f xβ€–) x

Lemma 7.5.10

source
@[irreducible]
def TileStructure.Forest.C7_5_4 (a : β„•) :
NNReal

The constant used in holder_correlation_tree. Has value 2 ^ (535 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.C7_5_4_def (a : β„•) :
C7_5_4 a = 2 ^ (535 * ↑a ^ 3)
source
theorem TileStructure.Forest.holder_correlation_tree {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f₁ fβ‚‚ : X β†’ β„‚} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
HolderOnWith (C7_5_4 a * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) f₁ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (fun (x : X) => β€–f₁ xβ€–) x).toNNReal) * ((β¨… x ∈ Metric.ball (c J) (8⁻¹ * ↑(defaultD a) ^ s J), β€–adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚) fβ‚‚ xβ€–β‚Š) + (β¨… x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (fun (x : X) => β€–fβ‚‚ xβ€–) x).toNNReal)) (nnΟ„ X) (t.holderFunction u₁ uβ‚‚ f₁ fβ‚‚ J) (Metric.ball (c J) (8 * ↑(defaultD a) ^ s J))

Lemma 7.5.4.

Subsection 7.5.3 and Lemma 7.4.5 #

source
theorem TileStructure.Forest.C7_5_11_def (a n : β„•) :
C7_5_11 a n = 2 ^ (↑(defaultZ a) * ↑n / 2 - 201 * ↑a ^ 3)
source
@[irreducible]
def TileStructure.Forest.C7_5_11 (a n : β„•) :
NNReal

The constant used in lower_oscillation_bound. Has value 2 ^ (Z * n / 2 - 201 * a ^ 3) in the blueprint.

Equations
source
theorem TileStructure.Forest.lower_oscillation_bound {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {J : Grid X} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hJ : J ∈ t.𝓙₅ u₁ uβ‚‚) :
↑(C7_5_11 a n) ≀ dist_{c J ,8 * ↑(defaultD a) ^ s J} (𝒬 u₁) (𝒬 uβ‚‚)

Lemma 7.5.11

source
theorem TileStructure.Forest.C7_4_5_def (a n : β„•) :
C7_4_5 a n = 2 ^ (541 * ↑a ^ 3 - ↑(defaultZ a) * ↑n / (4 * ↑a ^ 2 + 2 * ↑a ^ 3))
source
@[irreducible]
def TileStructure.Forest.C7_4_5 (a n : β„•) :
NNReal

The constant used in correlation_distant_tree_parts. Has value 2 ^ (541 * a ^ 3 - Z * n / (4 * a ^ 2 + 2 * a ^ 3)) in the blueprint.

Equations
source
theorem TileStructure.Forest.correlation_distant_tree_parts {X : Type u_1} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q (defaultD a) (defaultΞΊ a) (defaultS X) (cancelPt X)] {n : β„•} {t : Forest X n} {u₁ uβ‚‚ : 𝔓 X} {f₁ fβ‚‚ g₁ gβ‚‚ : X β†’ β„‚} (hu₁ : u₁ ∈ t) (huβ‚‚ : uβ‚‚ ∈ t) (hu : u₁ β‰  uβ‚‚) (h2u : π“˜ u₁ ≀ π“˜ uβ‚‚) (hf₁ : Bornology.IsBounded (Set.range f₁)) (h2f₁ : HasCompactSupport f₁) (hfβ‚‚ : Bornology.IsBounded (Set.range fβ‚‚)) (h2fβ‚‚ : HasCompactSupport fβ‚‚) :
β€–βˆ« (x : X), adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u₁) g₁ x * (starRingEnd β„‚) (adjointCarlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) uβ‚‚ ∩ t.𝔖₀ u₁ uβ‚‚) gβ‚‚ x)β€–β‚‘ ≀ ↑(C7_4_5 a n) * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator u₁ g₁) x).toReal) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (fun (x : X) => ((↑(π“˜ u₁)).indicator (t.adjointBoundaryOperator uβ‚‚ gβ‚‚) x).toReal) 2 MeasureTheory.volume

Lemma 7.4.5