theorem integrableOn_K_mul_f {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] {f : X → ℂ} {x' : X} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) {r : ENNReal} (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (y : X) => K x' y * f y) (Set.EAnnulus.ci x' r) MeasureTheory.volume

theorem TileStructure.Forest.eLpNorm_MB_le {X : Type u_2} {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)] {𝕜 : Type u_4} [RCLike 𝕜] {f : X → 𝕜} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) : MeasureTheory.eLpNorm (maximalFunction MeasureTheory.volume 𝓑 c𝓑 r𝓑 1 f) 2 MeasureTheory.volume ≤ ↑(CMB (↑(defaultA a)) 2) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Section 7.2 and Lemma 7.2.1

theorem TileStructure.Forest.C7_2_2_def (a : ℕ) : C7_2_2 a = 2 ^ ((𝕔 + 2) * a ^ 3)

@[irreducible]

def TileStructure.Forest.C7_2_2 (a : ℕ) : NNReal

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

Equations

• TileStructure.Forest.C7_2_2 a = 2 ^ ((𝕔 + 2) * a ^ 3)

theorem TileStructure.Forest.le_C7_2_2 {a : ℕ} (a4 : 4 ≤ a) : 2 * C_Ts a + 2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * CMB (↑(defaultA a)) 2 ≤ C7_2_2 a

theorem TileStructure.Forest.nontangential_operator_bound {X : Type u_2} {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 → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (θ : Θ X) : MeasureTheory.eLpNorm (nontangentialMaximalFunction θ f) 2 MeasureTheory.volume ≤ ↑(C7_2_2 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Lemma 7.2.2.

noncomputable def TileStructure.Forest.kissing {X : Type u_2} {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)] (I : Grid X) : Finset (Grid X)

The set of cubes in Lemma 7.2.4.

Equations

• TileStructure.Forest.kissing I = {J : Grid X | s J = s I ∧ ¬Disjoint (Metric.ball (c I) (16 * ↑(defaultD a) ^ s I)) (Metric.ball (c J) (16 * ↑(defaultD a) ^ s J))}

theorem TileStructure.Forest.subset_of_kissing {X : Type u_2} {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)] {I J : Grid X} (h : J ∈ kissing I) : Metric.ball (c J) (↑(defaultD a) ^ s J / 4) ⊆ Metric.ball (c I) (33 * ↑(defaultD a) ^ s I)

theorem TileStructure.Forest.volume_le_of_kissing {X : Type u_2} {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)] {I J : Grid X} (h : J ∈ kissing I) : MeasureTheory.volume (Metric.ball (c I) (33 * ↑(defaultD a) ^ s I)) ≤ 2 ^ (9 * a) * MeasureTheory.volume (Metric.ball (c J) (↑(defaultD a) ^ s J / 4))

theorem TileStructure.Forest.pairwiseDisjoint_of_kissing {X : Type u_2} {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)] {I : Grid X} : (↑(kissing I)).PairwiseDisjoint fun (i : Grid X) => Metric.ball (c i) (↑(defaultD a) ^ s i / 4)

theorem TileStructure.Forest.boundary_overlap {X : Type u_2} {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)] (I : Grid X) : (kissing I).card ≤ 2 ^ (9 * a)

Lemma 7.2.4.

theorem TileStructure.Forest.e728_push_toReal {X : Type u_2} {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} {f : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) : (t.boundaryOperator u f x).toReal = ∑ I : Grid X, (↑I).indicator (fun (x : X) => ∑ J ∈ t.𝓙' u (c I) (s I), (ijIntegral f I J).toReal) x

theorem TileStructure.Forest.e728_rearrange {X : Type u_2} {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} {f g : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) : ∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal = ∑ I : Grid X, (↑(MeasureTheory.volume (Metric.ball (c I) (16 * ↑(defaultD a) ^ s I)))⁻¹.toReal * ∫ (x : X) in ↑I, (starRingEnd ℂ) (g x)) * ↑(∑ J ∈ t.𝓙' u (c I) (s I), (↑(defaultD a) ^ ((↑(s J) - ↑(s I)) / ↑a) * ∫⁻ (y : X) in ↑J, ‖f y‖ₑ).toReal)

theorem TileStructure.Forest.e728 {X : Type u_2} {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} {f g : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal‖ₑ ≤ ∑ J ∈ (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)).toFinset, ∫⁻ (y : X) in ↑J, ‖f y‖ₑ * maximalFunction MeasureTheory.volume 𝓑 c𝓑 r𝓑 1 g y * ∑ I : Grid X, if ↑J ⊆ Metric.ball (c I) (16 * ↑(defaultD a) ^ s I) ∧ s J ≤ s I then ↑(defaultD a) ^ ((↑(s J) - ↑(s I)) / ↑a) else 0

Equation (7.2.8) in the proof of Lemma 7.2.3.

theorem TileStructure.Forest.boundary_geometric_series {X : Type u_2} {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} : (∑ I : Grid X, if ↑J ⊆ Metric.ball (c I) (16 * ↑(defaultD a) ^ s I) ∧ s J ≤ s I then ↑(defaultD a) ^ ((↑(s J) - ↑(s I)) / ↑a) else 0) ≤ 2 ^ (9 * a + 1)

Bound for the inner sum in Equation (7.2.8).

theorem TileStructure.Forest.C7_2_3_def (a : ℕ) : C7_2_3 a = 2 ^ (12 * ↑a)

@[irreducible]

noncomputable def TileStructure.Forest.C7_2_3 (a : ℕ) : NNReal

can be improved to 2 ^ (10 * a + 5 / 2)

Equations

• TileStructure.Forest.C7_2_3 a = 2 ^ (12 * ↑a)

theorem TileStructure.Forest.boundary_operator_bound_aux {X : Type u_2} {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} {f g : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * ↑(t.boundaryOperator u f x).toReal‖ₑ ≤ ↑(C7_2_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume * MeasureTheory.eLpNorm g 2 MeasureTheory.volume

theorem TileStructure.Forest.boundary_operator_bound {X : Type u_2} {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} {f : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) : MeasureTheory.eLpNorm (t.boundaryOperator u f) 2 MeasureTheory.volume ≤ ↑(C7_2_3 a) * MeasureTheory.eLpNorm f 2 MeasureTheory.volume

Lemma 7.2.3.

@[irreducible]

def TileStructure.Forest.C7_2_1 (a : ℕ) : NNReal

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

Equations

• TileStructure.Forest.C7_2_1 a = 2 ^ ((𝕔 + 5 + 𝕔 / 4) * a ^ 3)

theorem TileStructure.Forest.C7_2_1_def (a : ℕ) : C7_2_1 a = 2 ^ ((𝕔 + 5 + 𝕔 / 4) * a ^ 3)

@[simp]

theorem TileStructure.Forest.Complex.enorm_real (x : ℝ) : ‖↑x‖ₑ = ‖x‖ₑ

theorem TileStructure.Forest.tree_projection_estimate {X : Type u_2} {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} {f g : X → ℂ} (hf : MeasureTheory.BoundedCompactSupport f MeasureTheory.volume) (hg : MeasureTheory.BoundedCompactSupport g MeasureTheory.volume) (hu : u ∈ t) : ‖∫ (x : X), (starRingEnd ℂ) (g x) * carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) f x‖ₑ ≤ ↑(C7_2_1 a) * MeasureTheory.eLpNorm (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖f x‖) 2 MeasureTheory.volume * MeasureTheory.eLpNorm (approxOnCube (𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖g x‖) 2 MeasureTheory.volume

Lemma 7.2.1.