small fixes

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]

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
@@ -2897,7 +2897,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]
@@ -4387,7 +4387,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\,.
     $$
@@ -4399,7 +4399,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\,.
     $$