change definition of 𝓑 to include more exponents

Carleson/ForestOperator/L2Estimate.lean

@@ -213,13 +213,14 @@ private lemma nontangential_integral_bound₂ (hf : BoundedCompactSupport f) {x
     _ = ⨍⁻ y in ball (c I) (16 * D ^ s I), ‖f y‖ₑ ∂volume := by rw [setLaverage_eq]
     _ ≤ MB volume 𝓑 c𝓑 r𝓑 f x := by
       rw [MB, maximalFunction, inv_one, ENNReal.rpow_one]
-      have : ⟨4, I⟩ ∈ 𝓑 := by simp [𝓑]
+      have : (4, 0, I) ∈ 𝓑 := by simp [𝓑]
       refine le_of_eq_of_le ?_ (le_biSup _ this)
       have : x ∈ ball (c I) (2 ^ 4 * (D : ℝ) ^ s I) := by
         refine (ball_subset_ball ?_) (Grid_subset_ball hx)
         unfold s
         linarith [defaultD_pow_pos a (GridStructure.s I)]
-      simp_rw [c𝓑, r𝓑, ENNReal.rpow_one, indicator_of_mem this, enorm_eq_nnnorm]
+      simp_rw [c𝓑, r𝓑, ENNReal.rpow_one, Nat.cast_zero, add_zero, indicator_of_mem this,
+        enorm_eq_nnnorm]
       norm_num
 
 -- Pointwise bound needed for Lemma 7.2.2
@@ -553,7 +554,7 @@ lemma e728 (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) :
         split_ifs with hIJ; swap; · rfl
         refine mul_le_mul_right' (mul_le_mul_right' ?_ _) _
         obtain ⟨b, mb, eb⟩ : ∃ i ∈ 𝓑, ball (c𝓑 i) (r𝓑 i) = ball (c I) (16 * D ^ s I) := by
-          use ⟨4, I⟩; norm_num [𝓑, c𝓑, r𝓑]
+          use (4, 0, I); norm_num [𝓑, c𝓑, r𝓑]
         rw [MB, maximalFunction]; simp_rw [inv_one, ENNReal.rpow_one]
         exact le_iSup₂_of_le b mb (by rw [indicator_of_mem (eb ▸ hIJ.1 my), eb])
     _ = _ := by
@@ -665,12 +666,15 @@ lemma boundary_operator_bound_aux (hf : BoundedCompactSupport f) (hg : BoundedCo
     _ ≤ 2 ^ (9 * a + 1) * eLpNorm f 2 volume * (2 ^ (a + (3 / 2 : ℝ)) * eLpNorm g 2 volume) := by
       have ST : HasStrongType (α := X) (α' := X) (ε₁ := ℂ) (MB volume 𝓑 c𝓑 r𝓑) 2 2 volume volume
           (CMB (defaultA a) 2) := by
-        refine hasStrongType_MB 𝓑.to_countable (R := 2 ^ (S + 5) * D ^ S)
+        refine hasStrongType_MB 𝓑.to_countable (R := 2 ^ (S + 5) * D ^ (S + 𝓑max))
           (fun ⟨bs, bi⟩ mb ↦ ?_) (by norm_num)
-        simp_rw [𝓑, mem_prod, mem_Icc, zero_le, mem_univ, and_true, true_and] at mb
-        unfold r𝓑; gcongr
+        simp_rw [𝓑, mem_prod, mem_Iic, mem_univ, and_true] at mb
+        obtain ⟨mb1, mb2⟩ := mb
+        rw [r𝓑, ← zpow_natCast (n := S + 𝓑max), Nat.cast_add]
+        gcongr
         · exact one_le_two
-        · rw [← zpow_natCast]; exact zpow_le_zpow_right₀ one_le_D scale_mem_Icc.2
+        · exact one_le_D
+        · exact scale_mem_Icc.2
       specialize ST g (hg.memℒp 2)
       rw [CMB_defaultA_two_eq, ENNReal.coe_rpow_of_ne_zero two_ne_zero, ENNReal.coe_ofNat] at ST
       exact mul_le_mul_left' ST.2 _

Carleson/ForestOperator/PointwiseEstimate.lean

@@ -234,17 +234,21 @@ lemma boundaryOperator_lt_top (hf : BoundedCompactSupport f) : t.boundaryOperato
     exact ENNReal.sum_lt_top.mpr (fun _ _ ↦ ijIntegral_lt_top hf)
   · simp [hx]
 
+
+/- Number of additional exponents we have to include in `𝓑`. Feel free to increase if needed. -/
+def 𝓑max : ℕ := 3
+
 /-- The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3. -/
-def 𝓑 : Set (ℕ × Grid X) := Icc 0 (S + 5) ×ˢ univ
+def 𝓑 : Set (ℕ × ℕ × Grid X) := Iic (S + 5) ×ˢ Iic 𝓑max ×ˢ univ
 
 /-- The center function for the collection of balls 𝓑. -/
-def c𝓑 (z : ℕ × Grid X) : X := c z.2
+def c𝓑 (z : ℕ × ℕ × Grid X) : X := c z.2.2
 
 /-- The radius function for the collection of balls 𝓑. -/
-def r𝓑 (z : ℕ × Grid X) : ℝ := 2 ^ z.1 * D ^ s z.2
+def r𝓑 (z : ℕ × ℕ × Grid X) : ℝ := 2 ^ z.1 * D ^ (s z.2.2 + z.2.1)
 
 lemma 𝓑_finite : (𝓑 (X := X)).Finite :=
-  finite_Icc .. |>.prod finite_univ
+  finite_Iic _ |>.prod <| finite_Iic _ |>.prod finite_univ
 
 /-- Lemma 7.1.1, freely translated. -/
 lemma convex_scales (hu : u ∈ t) : OrdConnected (t.σ u x : Set ℤ) := by
@@ -520,16 +524,16 @@ private lemma L7_1_4_laverage_le_MB (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx'
     {p : 𝔓 X} (pu : p ∈ t.𝔗 u) (xp : x ∈ E p) :
     (∫⁻ y in ball (𝔠 p) (16 * D ^ 𝔰 p), ‖g y‖₊) / volume (ball (𝔠 p) (16 * D ^ 𝔰 p)) ≤
     MB volume 𝓑 c𝓑 r𝓑 g x' := by
-  have mem_𝓑 : ⟨4, 𝓘 p⟩ ∈ 𝓑 := by simp [𝓑]
+  have mem_𝓑 : (4, 0, 𝓘 p) ∈ 𝓑 := by simp [𝓑]
   convert le_biSup (hi := mem_𝓑) <| fun i ↦ ((ball (c𝓑 i) (r𝓑 i)).indicator (x := x') <|
     fun _ ↦ ⨍⁻ y in ball (c𝓑 i) (r𝓑 i), ‖g y‖₊ ∂volume)
-  · have x'_in_ball : x' ∈ ball (c𝓑 (4, 𝓘 p)) (r𝓑 (4, 𝓘 p)) := by
-      simp only [c𝓑, r𝓑, _root_.s]
+  · have x'_in_ball : x' ∈ ball (c𝓑 (4, 0, 𝓘 p)) (r𝓑 (4, 0, 𝓘 p)) := by
+      simp_rw [c𝓑, r𝓑, _root_.s, Nat.cast_zero, add_zero]
       have : x' ∈ 𝓘 p := subset_of_mem_𝓛 hL pu (not_disjoint_iff.mpr ⟨x, xp.1, hx⟩) hx'
       refine Metric.ball_subset_ball ?_ <| Grid_subset_ball this
       linarith [defaultD_pow_pos a (GridStructure.s (𝓘 p))]
-    have hc𝓑 : 𝔠 p = c𝓑 (4, 𝓘 p) := by simp [c𝓑, 𝔠]
-    have hr𝓑 : 16 * D ^ 𝔰 p = r𝓑 (4, 𝓘 p) := by rw [r𝓑, 𝔰]; norm_num
+    have hc𝓑 : 𝔠 p = c𝓑 (4, 0, 𝓘 p) := by simp [c𝓑, 𝔠]
+    have hr𝓑 : 16 * D ^ 𝔰 p = r𝓑 (4, 0, 𝓘 p) := by rw [r𝓑, 𝔰]; norm_num
     simp [-defaultD, laverage, x'_in_ball, ENNReal.div_eq_inv_mul, hc𝓑, hr𝓑]
   · simp only [MB, maximalFunction, ENNReal.rpow_one, inv_one]
 

blueprint/src/chapter/main.tex

@@ -4308,12 +4308,12 @@ \section{The pointwise tree estimate}
     :=\sum_{I\in\mathcal{D}} \mathbf{1}_{I}(x) \sum_{\substack{J\in \mathcal{J}(\fT(\fu))\\
     J\subset B(c(I), 16 D^{s(I)})\\ s(J) \le s(I)}} \frac{D^{(s(J) - s(I))/a}}{\mu(B(c(I), 16D^{s(I)}))}\int_J |f(y)| \, \mathrm{d}\mu(y)\,.
 \end{equation}
-%changed definition
+%changed definition (2x)
 Define also the collection of balls
 $$
-    \mathcal{B} = \{B(c(I), 2^s D^{s(I)}) \ : \ I \in \mathcal{D}\,, 0 \le s \le S + 5\}\,.
+    \mathcal{B} = \{B(c(I), 2^s D^{s(I)+t}) \ : \ I \in \mathcal{D}\,, 0 \le s \le S + 5\,, 0 \le t \le 3\}\,.
 $$
-%changed definition.
+%changed definition. (2x) We can increase the 3 further, if desired
 
 The following pointwise estimate for operators associated to sets $\fT(\fu)$ is the main result of this subsection.