Fix typos in blueprint and lean files (#1)

* Update Defs.lean

* Update Carleson.lean

* Update main.tex

Carleson/Carleson.lean

@@ -139,7 +139,7 @@ lemma equation3_1 {f : X → ℂ} (hf : LocallyIntegrable f)
   rw [h3, ← neg_sub, ← integral_univ, ← integral_diff]
   all_goals sorry
 
-  /- Proof should be straightward from the definition of maximalFunction and conditions on `𝓠`.
+  /- Proof should be straightforward from the definition of maximalFunction and conditions on `𝓠`.
   We have to approximate `Q` by an indicator function.
   2^σ ≈ r, 2^σ' ≈ R
   There is a small difference in integration domain, and for that we use the estimate IsCZKernel.norm_le_vol_inv

Carleson/Defs.lean

@@ -120,7 +120,7 @@ class IsCZKernel (τ : ℝ) (K : X → X → ℂ) : Prop where
 
 /-- In Mathlib we only have the operator norm for continuous linear maps,
 and (I think that) `T_*` is not linear.
-Here is the norm for an arbitary map `T` between normed spaces
+Here is the norm for an arbitrary map `T` between normed spaces
 (the infimum is defined to be 0 if the operator is not bounded). -/
 def operatorNorm {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] (T : E → F) : ℝ :=
   sInf { c | 0 ≤ c ∧ ∀ x, ‖T x‖ ≤ c * ‖x‖ }

blueprint/src/chapter/main.tex

@@ -626,7 +626,7 @@ \chapter{Overview of the proof of Theorem \ref{thm main 1}}
 \dens_2(\bigcup_{\fu\in \fU}\fT(\fu))^{1/q-1/2} \, .$$
 \end{prop}
 
-Theorem \ref{thm main 1} is formulated at the level of genereality
+Theorem \ref{thm main 1} is formulated at the level of generality
 for general kernels satisfying the mere H\"older regularity condition \eqref{eqkernel y smooth}. On the other hand, the $\tau$-cancellative condition \eqref{ew vdc cond} is a testing against more regular,
 namely Lipschitz functions. To bridge the gap, we follow \cite{zk-polynomial} to observe a variant of \eqref{ew vdc cond} that we formulate
 in the following Proposition proved in Section \ref{liphoel}.
@@ -1013,7 +1013,7 @@ \chapter{P. \ref{prop-linear}
 By \eqref{coverball} and $G\subset B(o,D^S)$, there is at least
 one $I\in \mathcal{D}$ with $s(I)=s$ and $x\in I$.
 By \eqref{dyadicproperty}, this $I$ is unique. By \eqref{eq dis freq cover}, there is precisely one $\fp\in \fP(I)$ such that
-$\tQ(x)\in \fc(\fp)$. Hecne there is precisely one  $\fp\in \fP$ with  $\ps(\fp)=s$ such that
+$\tQ(x)\in \fc(\fp)$. Hence there is precisely one  $\fp\in \fP$ with  $\ps(\fp)=s$ such that
 $x\in E(\fp)$. For this $\fp$, the value $T_{\fp}(x)$ by its definition in \eqref{definetp}
 equals the right-hand side of \eqref{insump}. This proves the lemma.
 \end{proof}
@@ -1061,7 +1061,7 @@ \section{Proof of L.\ref{dyadiclemma}, dyadic structure}
   \begin{equation}\label{jballs}
       \mu(B(y,2^{j}D^k))\le A^j \mu(B(y,D^k))\, .
   \end{equation}
- As $X$ is the union of the balls $B(y,2^{j}D^k)$ and $\mu$ is not zero, at least one ov
+ As $X$ is the union of the balls $B(y,2^{j}D^k)$ and $\mu$ is not zero, at least one of
  the balls $B(y,2^{j}D^k)$ has positive measure und thus $B(y,D^k)$ has positive measure.
 
  Applying \eqref{jballs} for $j'$ the smallest integer larger than $\ln_2(8D^{2S})$, using $-S\le k\le S$
@@ -1561,7 +1561,7 @@ \section{Proof of L.\ref{tilelemma}, tile structure}
 \end{lemma}
 
 \begin{proof}
-    This follows immediatly from the definition \eqref{definedE} and monotonicity of suprema with respect to set inclusion.
+    This follows immediately from the definition \eqref{definedE} and monotonicity of suprema with respect to set inclusion.
 \end{proof}
 
 Choose a grid structure $(\mathcal{D}, c, s)$. For cubes $I \in \mathcal{D}$, we will denote
@@ -1661,7 +1661,7 @@ \section{Proof of L.\ref{tilelemma}, tile structure}
 $$
 We define $\sc((I, z)) = I$ and $\fcc((I, z)) = z$. We further set $s(\fp) = s(\sc(\fp))$, $c(\fp) = c(\sc(\fp))$. Then \eqref{tilecenter}, \eqref{tilescale} hold.
 
-It remains to construct the map $\Omega$. We first construct an auxilliary map $\Omega_1$. For each $I \in \mathcal{D}$, we pick an enumeration of the finite set $Z(I)$
+It remains to construct the map $\Omega$. We first construct an auxiliary map $\Omega_1$. For each $I \in \mathcal{D}$, we pick an enumeration of the finite set $Z(I)$
 $$
     Z(I) = \{z_1, \dotsc, z_M\}\,.
 $$
@@ -2131,7 +2131,7 @@ \section{Proof of Lemma \ref{allgbound}, the exceptional sets}
 \begin{proof}
 Let $\fp,\fp'$ as in the lemma. As by definition of $E_1$
 we have
-$E_1(\fp)\subset \sc(\fp)$ and analoguously for $\fp'$, we conclude from \eqref{eintersect} that  $\sc(\fp)\cap \sc(\fp')\neq \emptyset$. Let without loss of generality $\sc(\fp)$ be maximal in
+$E_1(\fp)\subset \sc(\fp)$ and analogously for $\fp'$, we conclude from \eqref{eintersect} that  $\sc(\fp)\cap \sc(\fp')\neq \emptyset$. Let without loss of generality $\sc(\fp)$ be maximal in
 $\{\sc(\fp),\sc(\fp')\}$, then $\sc(\fp')\subset \sc(\fp)$.
 By \eqref{eintersect}, we conclude by definition of $E_1$ that $\fc(\fp)\cap \fc(\fp')\neq \emptyset$. By
 \eqref{eq freq dyadic} we conclude $\fc(\fp)\subset \fc(\fp')$. It follows that $\fp'\le \fp$. By maximality
@@ -2476,7 +2476,7 @@ \section{Proof of Lemma \ref{allgbound}, the exceptional sets}
 Using $D = 2^{100a^2}$ and $a \ge 4$ and $\kappa Z \ge 1$ proves the lemma.
 \end{proof}
 
-\section{Auxilliary lemmas}
+\section{Auxiliary lemmas}
 
 Before proving Lemma \ref{subsecflemma} and Lemma \ref{subsecalemma}, we collect some useful properties of $\lesssim$.
 
@@ -3412,7 +3412,7 @@ \section{The density  arguments}\label{sec TT* T*T}
   \begin{equation}
       \le  2^{200a^3}({q}-1)^{-1} \tau^{-1}\dens_1(\mathfrak{A})^{\frac {q-1}{2p}}\dens_2(\mathfrak{A})^{\frac 1{q}-\frac 12}  \|f\|_2\|g\|_2\, .
   \end{equation}
- With the definiiton of $p$, this  implies
+ With the definition of $p$, this  implies
 Proposition \ref{antichainprop}.
 
 
@@ -3560,7 +3560,7 @@ \section{Proof of L. \ref{lem basic TT*}, the tile correlation bound }\label{sec
     \le 2^{4a} d_{\fp_2}(\tQ(x_2),\fcc(\fp_2))\le 2^{4a}
     \, .
 \end{equation}
-By the triangle ineqality, we obtain from \eqref{dponetwo} and
+By the triangle inequality, we obtain from \eqref{dponetwo} and
 \eqref{tgeo0.5}
 \begin{equation}\label{tgeo1}
      1+d_{\fp_1}(\fcc(\fp_1), \fcc(\fp_2))\le  2+2^{4a} +d_{\fp_1}(\tQ(x_1), \tQ(x_2))\, .
@@ -3577,7 +3577,7 @@ \section{Proof of L. \ref{lem basic TT*}, the tile correlation bound }\label{sec
 \begin{equation}\label{tgeo1.5}
     \le  2+2^{4a}+d_{B(x_1,8D^{\ps(\fp_1)})}(\tQ(x_1), \tQ(x_2))\, .
 \end{equation}
-This is further estimated by aplying the doubling property  \eqref{firstdb} three times by
+This is further estimated by applying the doubling property  \eqref{firstdb} three times by
 \begin{equation}\label{tgeo2}
     \le  2+2^{4a}+2^{3a}d_{B_1(x_1, D^{s(\fp_1)})}(\tQ(x_1), \tQ(x_2))\, .
 \end{equation}
@@ -3614,7 +3614,7 @@ \section{Proof of L. \ref{lem basic TT*}, the tile correlation bound }\label{sec
 \begin{equation}
 \rho(x,y)\le \frac 12 D^{\ps(\fp)}\, .
 \end{equation}
-Now \eqref{ynotfar} follows by the tirangle inequality.
+Now \eqref{ynotfar} follows by the triangle inequality.
 \end{proof}
 
 
@@ -3966,7 +3966,7 @@ \section{Proof of Lemma \ref{lem antichain 1}, the geometric estimate}
 We turn to \eqref{eqanti2}.
 Consider the element $\fp'\in \mathfrak{A}'$ as above
 with $L\subset \sc(\fp')$ and $s(L)<s(\fp')$.
-As $L\subset L'$, we conclude twith the dyadic property that $L'\subset \sc(\fp')$.
+As $L\subset L'$, we conclude with the dyadic property that $L'\subset \sc(\fp')$.
 By maximality of $L$, we have
 $L'\not\in \mathcal{L}$.
 This together with the existence of the given $\fp'\in \mathfrak{A}$
@@ -4235,7 +4235,7 @@ \section{Tree Estimate}
 $$
     P_{\mathcal{C}}f(x) :=\sum_{J\in\mathcal{C}}\mathbf{1}_J(x) \frac{1}{\mu(J)}\int_J f(y) \, \mathrm{d}\mu(y)\,.
 $$
-Define for each $\fu \in \fU$ the auxilliary operator
+Define for each $\fu \in \fU$ the auxiliary operator
 \begin{equation}
     \label{eq def S op}
     S_{\fu}f(x):=\sum_{I\in\mathcal{D}} \mathbf{1}_{I}(x) \sum_{\substack{J\in \mathcal{J}(\fT(\fu))\\