Section 7.1 and Lemma 7.1.3 #
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 : 𝔓 X)
(x : X)
:
The definition σ(u, x) given in Section 7.1.
We may assume u ∈ t whenever proving things about this definition.
Instances For
def
TileStructure.Forest.σMax
{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)
(hσ : (t.σ u x).Nonempty)
:
Instances For
def
TileStructure.Forest.σMin
{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)
(hσ : (t.σ u x).Nonempty)
:
Instances For
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)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2
Equations
Instances For
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)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓙(𝔖), defined above Lemma 7.1.2
Equations
Instances For
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)]
{𝔖 : Set (𝔓 X)}
:
(𝓙 𝔖).PairwiseDisjoint fun (I : Grid X) => ↑I
theorem
TileStructure.Forest.S_eq_zero_of_topCube_mem_𝓙₀
{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)}
(h𝔖 : 𝔖.Nonempty)
(h : topCube ∈ 𝓙₀ 𝔖)
:
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)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2
Equations
Instances For
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)]
(𝔖 : Set (𝔓 X))
:
The definition of `𝓛(𝔖), defined above Lemma 7.1.2
Equations
Instances For
theorem
TileStructure.Forest.le_of_mem_𝓛
{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)}
{L : Grid X}
(hL : L ∈ 𝓛 𝔖)
{p : 𝔓 X}
(hp : p ∈ 𝔖)
(hpL : ¬Disjoint ↑(𝓘 p) ↑L)
:
def
TileStructure.Forest.approxOnCube
{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)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
(f : X → E')
(x : X)
:
E'
The projection operator P_𝓒 f(x), given above Lemma 7.1.3.
In lemmas the c will be pairwise disjoint on C.
Equations
Instances For
theorem
TileStructure.Forest.stronglyMeasurable_approxOnCube
{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)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
(f : X → E')
:
theorem
TileStructure.Forest.integrable_approxOnCube
{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)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
(C : Set (Grid X))
{f : X → E'}
:
theorem
TileStructure.Forest.approxOnCube_nonneg
{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)]
{C : Set (Grid X)}
{f : X → ℝ}
(hf : ∀ (y : X), f y ≥ 0)
{x : X}
:
theorem
TileStructure.Forest.approxOnCube_apply
{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)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{C : Set (Grid X)}
(hC : C.PairwiseDisjoint fun (I : Grid X) => ↑I)
(f : X → E')
{x : X}
{J : Grid X}
(hJ : J ∈ C)
(xJ : x ∈ J)
:
theorem
TileStructure.Forest.boundedCompactSupport_approxOnCube
{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)]
{𝕜 : Type u_3}
[RCLike 𝕜]
{C : Set (Grid X)}
{f : X → 𝕜}
:
theorem
TileStructure.Forest.integral_eq_lintegral_approxOnCube
{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)]
{C : Set (Grid X)}
(hC : C.PairwiseDisjoint fun (I : Grid X) => ↑I)
{J : Grid X}
(hJ : J ∈ C)
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
:
theorem
TileStructure.Forest.norm_approxOnCube_le_approxOnCube_norm
{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)]
{E' : Type u_2}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{C : Set (Grid X)}
{f : X → E'}
{x : X}
:
def
TileStructure.Forest.cubeOf
{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)]
(i : ℤ)
(x : X)
:
Grid X
The definition I_i(x), given above Lemma 7.1.3.
The cube of scale s that contains x. There is at most 1 such cube, if it exists.
Equations
- TileStructure.Forest.cubeOf i x = Classical.epsilon fun (I : Grid X) => x ∈ I ∧ s I = i
Instances For
theorem
TileStructure.Forest.cubeOf_spec
{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)]
{i : ℤ}
(hi : i ∈ Set.Icc (-↑(defaultS X)) ↑(defaultS X))
(I : Grid X)
{x : X}
(hx : x ∈ I)
:
def
TileStructure.Forest.nontangentialMaximalFunction
{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)]
(θ : Θ X)
(f : X → ℂ)
(x : X)
:
The definition T_𝓝^θ f(x), given in (7.1.3).
For convenience, the suprema are written a bit differently than in the blueprint
(avoiding cubeOf), but this should be equivalent.
This is 0 if x doesn't lie in a cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TileStructure.Forest.ijIntegral
{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 → ℂ)
(I J : Grid X)
:
Scaled integral appearing in the definition of boundaryOperator.
Equations
Instances For
theorem
TileStructure.Forest.ijIntegral_lt_top
{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 → ℂ}
{I J : Grid X}
(hf : MeasureTheory.BoundedCompactSupport f)
:
def
TileStructure.Forest.boundaryOperator
{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)
(f : X → ℂ)
(x : X)
:
The operator S_{1,𝔲} f(x), given in (7.1.4).
Equations
- t.boundaryOperator u f x = ∑ I : Grid X, (↑I).indicator (fun (x : X) => ∑ J ∈ t.𝓙' u (c I) (s I), TileStructure.Forest.ijIntegral f I J) x
Instances For
theorem
TileStructure.Forest.measurable_boundaryOperator
{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}
{f : X → ℂ}
:
Measurable (t.boundaryOperator u f)
theorem
TileStructure.Forest.boundaryOperator_lt_top
{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}
{f : X → ℂ}
(hf : MeasureTheory.BoundedCompactSupport f)
:
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)]
:
The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3.
Equations
Instances For
def
TileStructure.Forest.c𝓑
{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)]
(z : ℕ × ℕ × Grid X)
:
X
The center function for the collection of balls 𝓑.
Equations
- TileStructure.Forest.c𝓑 z = c z.2.2
Instances For
def
TileStructure.Forest.r𝓑
{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)]
(z : ℕ × ℕ × Grid X)
:
The radius function for the collection of balls 𝓑.
Instances For
theorem
TileStructure.Forest.laverage_le_biInf_MB'
{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}
{c₀ : X}
{r₀ : ℝ}
(hr : 4 * ↑(defaultD a) ^ s J + dist (c J) c₀ ≤ r₀)
(h : ∃ i ∈ 𝓑, c𝓑 i = c₀ ∧ r𝓑 i = r₀)
:
⨍⁻ (x : X) in Metric.ball c₀ r₀, ‖f x‖ₑ ∂MeasureTheory.volume ≤ ⨅ x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x
theorem
TileStructure.Forest.laverage_le_biInf_MB
{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}
{r₀ : ℝ}
(hr : 4 * ↑(defaultD a) ^ s J ≤ r₀)
(h : ∃ i ∈ 𝓑, c𝓑 i = c J ∧ r𝓑 i = r₀)
:
⨍⁻ (x : X) in Metric.ball (c J) r₀, ‖f x‖ₑ ∂MeasureTheory.volume ≤ ⨅ x ∈ J, MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 f x
theorem
TileStructure.Forest.convex_scales
{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}
(hu : u ∈ t)
:
(↑(t.σ u x)).OrdConnected
Lemma 7.1.1, freely translated.
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)]
{𝔖 : Set (𝔓 X)}
:
(𝓛 𝔖).PairwiseDisjoint fun (I : Grid X) => ↑I
Part of Lemma 7.1.2
@[irreducible]
The constant used in first_tree_pointwise.
Has value 10 * 2 ^ (104 * a ^ 3) in the blueprint.
Instances For
theorem
TileStructure.Forest.first_tree_pointwise
{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 → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
Lemma 7.1.4
theorem
TileStructure.Forest.second_tree_pointwise
{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 → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
:
Lemma 7.1.5
@[irreducible]
The constant used in third_tree_pointwise.
Has value 2 ^ (151 * a ^ 3) in the blueprint.
Equations
- TileStructure.Forest.C7_1_6 a = 2 ^ (151 * ↑a ^ 3)
Instances For
theorem
TileStructure.Forest.sum_p_eq_sum_I_sum_p
{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)
(f : X → ℤ → NNReal)
:
theorem
TileStructure.Forest.third_tree_pointwise
{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 → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
Lemma 7.1.6
@[irreducible]
The constant used in pointwise_tree_estimate.
Has value 2 ^ (151 * a ^ 3) in the blueprint.
Equations
Instances For
theorem
TileStructure.Forest.pointwise_tree_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 : 𝔓 X}
{x x' : X}
{f : X → ℂ}
{L : Grid X}
(hu : u ∈ t)
(hL : L ∈ 𝓛 ((fun (x : 𝔓 X) => t.𝔗 x) u))
(hx : x ∈ L)
(hx' : x' ∈ L)
(hf : MeasureTheory.BoundedCompactSupport f)
:
↑‖carlesonSum ((fun (x : 𝔓 X) => t.𝔗 x) u) (fun (y : X) => Complex.exp (Complex.I * -↑((𝒬 u) y)) * f y) x‖₊ ≤ ↑(C7_1_3 a) * (MB MeasureTheory.volume 𝓑 c𝓑 r𝓑 (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ‖f x‖) x' + t.boundaryOperator u (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) fun (x : X) => ↑‖f x‖) x') + nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 ((fun (x : 𝔓 X) => t.𝔗 x) u)) f) x'
Lemma 7.1.3.