diff --git a/Carleson/Carleson.lean b/Carleson/Carleson.lean index befc1207..4627a58e 100644 --- a/Carleson/Carleson.lean +++ b/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 diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean index 3e7ab791..6ea187c0 100644 --- a/Carleson/Defs.lean +++ b/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‖ } diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index daa57a66..5d71b291 100644 --- a/blueprint/src/chapter/main.tex +++ b/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)