Lemma 7.2.4 (#132)

Carleson/ForestOperator.lean

@@ -201,7 +201,7 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L
         · unfold defaultD; positivity
       _ < _ := by rw [mul_comm]; gcongr
   have d1 : dist_{x, D ^ (s₂ - 1)} (𝒬 u) (Q x) < 1 := by
-    have := le_cdist_iterate (x := x) (r := D ^ (s₂ - 1)) (by sorry) (𝒬 u) (Q x) (100 * a)
+    have := le_cdist_iterate (x := x) (r := D ^ (s₂ - 1)) (by positivity) (𝒬 u) (Q x) (100 * a)
     calc
       _ ≤ dist_{x, D ^ s₂} (𝒬 u) (Q x) * 2 ^ (-100 * a : ℤ) := by
         rw [neg_mul, zpow_neg, le_mul_inv_iff₀ (by positivity), mul_comm]
@@ -274,11 +274,70 @@ lemma nontangential_operator_bound
     eLpNorm (nontangentialMaximalFunction θ f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
   sorry
 
+/-- The set of cubes in Lemma 7.2.4. -/
+def kissing (I : Grid X) : Finset (Grid X) :=
+  {J | s J = s I ∧ ¬Disjoint (ball (c I) (16 * D ^ s I)) (ball (c J) (16 * D ^ s J))}
+
+lemma subset_of_kissing (h : J ∈ kissing I) :
+    ball (c J) (D ^ s J / 4) ⊆ ball (c I) (33 * D ^ s I) := by
+  simp_rw [kissing, Finset.mem_filter, Finset.mem_univ, true_and] at h
+  obtain ⟨x, xI, xJ⟩ := not_disjoint_iff.mp h.2
+  apply ball_subset_ball'
+  calc
+    _ ≤ D ^ s J / 4 + dist (c J) x + dist x (c I) := by
+      rw [add_assoc]; exact add_le_add_left (dist_triangle ..) _
+    _ ≤ D ^ s J / 4 + 16 * D ^ s J + 16 * D ^ s I := by
+      gcongr
+      · exact (mem_ball'.mp xJ).le
+      · exact (mem_ball.mp xI).le
+    _ ≤ _ := by
+      rw [h.1, div_eq_mul_inv, mul_comm _ 4⁻¹, ← distrib_three_right]
+      exact mul_le_mul_of_nonneg_right (by norm_num) (by positivity)
+
+lemma volume_le_of_kissing (h : J ∈ kissing I) :
+    volume (ball (c I) (33 * D ^ s I)) ≤ 2 ^ (9 * a) * volume (ball (c J) (D ^ s J / 4)) := by
+  simp_rw [kissing, Finset.mem_filter, Finset.mem_univ, true_and] at h
+  obtain ⟨x, xI, xJ⟩ := not_disjoint_iff.mp h.2
+  have : ball (c I) (33 * D ^ s I) ⊆ ball (c J) (128 * D ^ s J) := by
+    apply ball_subset_ball'
+    calc
+      _ ≤ 33 * D ^ s I + dist (c I) x + dist x (c J) := by
+        rw [add_assoc]; exact add_le_add_left (dist_triangle ..) _
+      _ ≤ 33 * D ^ s I + 16 * D ^ s I + 16 * D ^ s J := by
+        gcongr
+        · exact (mem_ball'.mp xI).le
+        · exact (mem_ball.mp xJ).le
+      _ ≤ _ := by
+        rw [h.1, ← distrib_three_right]
+        exact mul_le_mul_of_nonneg_right (by norm_num) (by positivity)
+  have double := measure_ball_le_pow_two' (μ := volume) (x := c J) (r := D ^ s J / 4) (n := 9)
+  have A9 : (defaultA a : ℝ≥0) ^ 9 = (2 : ℝ≥0∞) ^ (9 * a) := by
+    simp only [defaultA]; norm_cast; ring
+  rw [show (2 : ℝ) ^ 9 * (D ^ s J / 4) = 128 * D ^ s J by ring, A9] at double
+  exact (measure_mono this).trans double
+
+lemma pairwiseDisjoint_of_kissing :
+    (kissing I).toSet.PairwiseDisjoint fun i ↦ ball (c i) (D ^ s i / 4) := fun j mj k mk hn ↦ by
+  apply disjoint_of_subset ball_subset_Grid ball_subset_Grid
+  simp_rw [Finset.mem_coe, kissing, Finset.mem_filter] at mj mk
+  exact (eq_or_disjoint (mj.2.1.trans mk.2.1.symm)).resolve_left hn
+
 /-- Lemma 7.2.4. -/
-lemma boundary_overlap (I : Grid X) :
-    Finset.card { J | s J = s I ∧ ¬ Disjoint (ball (c I) (4 * D ^ s I)) (ball (c J) (4 * D ^ s J)) }
-    ≤ 2 ^ (9 * a) := by
-  sorry
+lemma boundary_overlap (I : Grid X) : (kissing I).card ≤ 2 ^ (9 * a) := by
+  have key : (kissing I).card * volume (ball (c I) (33 * D ^ s I)) ≤
+      2 ^ (9 * a) * volume (ball (c I) (33 * D ^ s I)) := by
+    calc
+      _ = ∑ _ ∈ kissing I, volume (ball (c I) (33 * D ^ s I)) := by
+        rw [Finset.sum_const, nsmul_eq_mul]
+      _ ≤ ∑ J ∈ kissing I, 2 ^ (9 * a) * volume (ball (c J) (D ^ s J / 4)) :=
+        Finset.sum_le_sum fun _ ↦ volume_le_of_kissing
+      _ = 2 ^ (9 * a) * volume (⋃ J ∈ kissing I, ball (c J) (D ^ s J / 4)) := by
+        rw [← Finset.mul_sum]; congr
+        exact (measure_biUnion_finset pairwiseDisjoint_of_kissing fun _ _ ↦ measurableSet_ball).symm
+      _ ≤ _ := by gcongr; exact iUnion₂_subset fun _ ↦ subset_of_kissing
+  have vn0 : volume (ball (c I) (33 * D ^ s I)) ≠ 0 := by
+    refine (measure_ball_pos volume _ ?_).ne'; simp only [defaultD]; positivity
+  rw [ENNReal.mul_le_mul_right vn0 (measure_ball_ne_top _ _)] at key; norm_cast at key
 
 /-- Lemma 7.2.3. -/
 lemma boundary_operator_bound

blueprint/src/chapter/main.tex

@@ -524,7 +524,7 @@ \chapter{Proof of Metric Space Carleson, overview}
 For each $\fu\in \fU$ and each $\fp\in \fT(\fu)$
 we have $\scI(\fp) \ne \scI(\fu)$ and
 \begin{equation}\label{forest1}
-4\fp\lesssim 1\fu.
+4\fp\lesssim \fu.
 \end{equation}
 For each $\fu \in \fU$ and each $\fp,\fp''\in \fT(\fu)$ and $\fp'\in \fP$
 we have
@@ -2898,7 +2898,7 @@ \section{Proof of the Forest Union Lemma}
     $$
         B_{\fu}(\fcc(\fu), 1) \subset B_{\fu'}(\fcc(\fu'), 500) \subset B_{\fp}(\fcc(\fp), 4)\,.
     $$
-    Together with $\scI(\fp) \subset \scI(\fu') = \scI(\fu)$, this gives $4\fp \lesssim 1\fu$, which is \eqref{forest1}.
+    Together with $\scI(\fp) \subset \scI(\fu') = \scI(\fu)$, this gives $4\fp \lesssim \fu$, which is \eqref{forest1}.
 \end{proof}
 
 \begin{lemma}[forest convex]
@@ -4388,7 +4388,7 @@ \section{The pointwise tree estimate}
 
 \begin{proof}
     Let $s_1 = \underline{\sigma}(\fu, x)$. By definition, there exists a tile $\fp \in \fT(\fu)$ with $\ps(\fp) = s_1$ and $x \in E(\fp)$. Then $x \in \scI(\fp) \cap L$. By \eqref{dyadicproperty} and the definition of $\mathcal{L}(\fT(\fu))$, it follows that $L \subset \scI(\fp)$, in particular $x' \in \scI(\fp)$, so $x \in I_{s_1}(x')$.
-    Next, let $s_2 = \overline{\sigma}(\fu, x)$ and let $\fp' \in \fT(\fu)$ with $\ps(\fp') = s_2$ and $x \in E(\fp')$. Since $\fp' \in \fT(\fu)$, we have $4\fp' \lesssim 1\fu$. Since $\tQ(x) \in \fc(\fp')$, it follows that
+    Next, let $s_2 = \overline{\sigma}(\fu, x)$ and let $\fp' \in \fT(\fu)$ with $\ps(\fp') = s_2$ and $x \in E(\fp')$. Since $\fp' \in \fT(\fu)$, we have $4\fp' \lesssim \fu$. Since $\tQ(x) \in \fc(\fp')$, it follows that
     $$
         d_{\fp}(\fcc(\fu), \tQ(x)) \le 5\,.
     $$
@@ -4400,7 +4400,7 @@ \section{The pointwise tree estimate}
     $$
         d_{B(x, D^{s_2})}(\fcc(\fu), \tQ(x)) \le 5 \cdot 2^{5a}\,.
     $$
-    Finally, by applying \eqref{seconddb} $2^{100a}$ times, we obtain
+    Finally, by applying \eqref{seconddb} $100a$ times, we obtain
     $$
         d_{B(x, D^{s_2-1})}(\fcc(\fu), \tQ(x)) \le 5 \cdot 2^{-95a} < 1\,.
     $$
@@ -4688,6 +4688,7 @@ \section{An auxiliary \texorpdfstring{$L^2$}{L2} tree estimate}
 \end{lemma}
 
 \begin{proof}
+    \leanok
     Suppose that $B(c(I), 16 D^{s(I)}) \cap B(c(J), 16 D^{s(J)}) \ne \emptyset$ and $s(I) = s(J)$. Then $B(c(I), 33 D^{s(I)}) \subset B(c(J), 128 D^{s(J)})$. Hence by the doubling property \eqref{doublingx}
     $$
         2^{9a}\mu(B(c(J), \frac{1}{4}D^{s(J)})) \ge \mu(B(c(I), 33 D^{s(I)}))\,,