diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean index 535a390..3b722f2 100644 --- a/Carleson/ForestOperator.lean +++ b/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 diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 0539757..a195444 100644 --- a/blueprint/src/chapter/main.tex +++ b/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)}))\,,