diff --git a/README.md b/README.md index d7c7b30..7fd5e1d 100644 --- a/README.md +++ b/README.md @@ -61,7 +61,7 @@ Note: To get this repository, you will need to download Lean's mathematical libr ## Building the blueprint -To test the Blueprint locally, you can compile `print.tex` using XeLaTeX (i.e. `xelatex print.tex` in the folder `blueprint/src`). If you have the Python package `invoke` you can also run `inv bp`. +To test the Blueprint locally, you can compile `print.tex` using XeLaTeX (i.e. `xelatex print.tex` in the folder `blueprint/src`). If you have the Python package `invoke` you can also run `inv bp` which puts the output in `blueprint/print/print.pdf`. If you feel adventurous and want to build the web version of the blueprint locally, you need to install some packages by following the instructions [here](https://pypi.org/project/leanblueprint/). But if the pdf builds locally, you can just make a pull request and use the online blueprint. ## Making a pull request diff --git a/blueprint/src/chapter/interpolation.tex b/blueprint/src/chapter/interpolation.tex index 9f1361c..dffbf0b 100644 --- a/blueprint/src/chapter/interpolation.tex +++ b/blueprint/src/chapter/interpolation.tex @@ -108,39 +108,39 @@ \section{Rietz-Thorin's Interpolation Theorem} Details to be filled later. \end{proof} - \begin{comment} - (Note: This is used by Stein-Shakarchi to prove the dual of $L^p$ is $L^q$, so it may be already formalized by the time - we get to this point?)\\\\ - Approximate $g$ by simple functions from below, i.e. consider a sequence $\{g_n\}_{n\in \bbn}$ of simple functions - such that for each $x$ we have $|g_n (x)| \leq |g(x)|$ and the $g_n$ converge to $g$ pointwise.\\ - If $p>1$ (thus $q<\infty$), consider - \[ f_n(x) = |g_n(x)|^{q-1} \mathrm{sign}(g(x)) \cdot \frac{1}{||g_n||^{q-1}_{L^q}} \] - Observe that $||f_n||_{L^p}=1$. For this, first note that $p(q-1)=q$ since - \[\frac{1}{p} = 1- \frac{1}{q}=\frac{q-1}{q} \ \Rightarrow \ q = p(q-1) \] - and then write - \[||f_n||^p_{L^p} = \int \left|\frac{1}{||g_n||_{L^q}^{q-1}} \cdot |g_n(x)|^{q-1} \mathrm{sign} g(x) \right|^p = \frac{1}{||g_n||_{L^q}^{p(q-1)}} \int |g_n(x)|^{p(q-1)} = \frac{1}{||g_n||_{L^q}^q} ||g_n||_{L^q}^q = 1 \] - So by assumption - \[ \left|\int f_n g\right| \leq M \] - And by direct computation - \[ \int f_n g = \int \] - - HOLE HERE - Then, we conclude by Fatou's Lemma - - If $p=1$, since the measure is $\sigma$-finite, write $X$ as an increasing union of subsets $\{E_n\}$ and take - \[ f_n (x) = \frac{1}{\mu(E_n)} \mathrm{sign}(g(x)) \chi_{E_n} (x) \] - Then $||f_n(x)||_{L^1} = \frac{1}{\mu(E_n)} \cdot \mu(E_n) = 1$. - - - Now, it is easy to show for both cases that $||g||\geq M$ by H\"older's inequality: since $M$ is the supremum of the absolute value of $\int fg$ for our possible $f$, - fix an $\epsilon>0$ and choose an $f$ such that - \[\left| \int fg \right| \geq M-\epsilon \] - so that - \[ M- \epsilon \leq ||fg||_{L^1} \leq ||f||_{L^p} ||g||_{L^q} \leq ||g||_{L^q} \] - Since $\epsilon$ is arbitrarily small, this gives - \[ ||g||_{L^q} \geq M \] - - \end{comment} + % \begin{comment} + % (Note: This is used by Stein-Shakarchi to prove the dual of $L^p$ is $L^q$, so it may be already formalized by the time + % we get to this point?)\\\\ + % Approximate $g$ by simple functions from below, i.e. consider a sequence $\{g_n\}_{n\in \bbn}$ of simple functions + % such that for each $x$ we have $|g_n (x)| \leq |g(x)|$ and the $g_n$ converge to $g$ pointwise.\\ + % If $p>1$ (thus $q<\infty$), consider + % \[ f_n(x) = |g_n(x)|^{q-1} \mathrm{sign}(g(x)) \cdot \frac{1}{||g_n||^{q-1}_{L^q}} \] + % Observe that $||f_n||_{L^p}=1$. For this, first note that $p(q-1)=q$ since + % \[\frac{1}{p} = 1- \frac{1}{q}=\frac{q-1}{q} \ \Rightarrow \ q = p(q-1) \] + % and then write + % \[||f_n||^p_{L^p} = \int \left|\frac{1}{||g_n||_{L^q}^{q-1}} \cdot |g_n(x)|^{q-1} \mathrm{sign} g(x) \right|^p = \frac{1}{||g_n||_{L^q}^{p(q-1)}} \int |g_n(x)|^{p(q-1)} = \frac{1}{||g_n||_{L^q}^q} ||g_n||_{L^q}^q = 1 \] + % So by assumption + % \[ \left|\int f_n g\right| \leq M \] + % And by direct computation + % \[ \int f_n g = \int \] + + % HOLE HERE + % Then, we conclude by Fatou's Lemma + + % If $p=1$, since the measure is $\sigma$-finite, write $X$ as an increasing union of subsets $\{E_n\}$ and take + % \[ f_n (x) = \frac{1}{\mu(E_n)} \mathrm{sign}(g(x)) \chi_{E_n} (x) \] + % Then $||f_n(x)||_{L^1} = \frac{1}{\mu(E_n)} \cdot \mu(E_n) = 1$. + + + % Now, it is easy to show for both cases that $||g||\geq M$ by H\"older's inequality: since $M$ is the supremum of the absolute value of $\int fg$ for our possible $f$, + % fix an $\epsilon>0$ and choose an $f$ such that + % \[\left| \int fg \right| \geq M-\epsilon \] + % so that + % \[ M- \epsilon \leq ||fg||_{L^1} \leq ||f||_{L^p} ||g||_{L^q} \leq ||g||_{L^q} \] + % Since $\epsilon$ is arbitrarily small, this gives + % \[ ||g||_{L^q} \geq M \] + + % \end{comment} As a last step towards proving the theorem, let us recall a consequence of Hölder's inequality, which will only really be substantial in a corner case of our proof. \begin{lemma} @@ -248,7 +248,7 @@ \section{Rietz-Thorin's Interpolation Theorem} \[||Tf||_{L^q} \leq ||Tf||_{L^{q_0}}^{1-t} ||Tf||_{L^{q_1}}^{t} \leq M_0^{1-t} M_1^t ||f||_{L^{\infty}} \] which is what we wanted.\\\\ If $p<\infty$ and $q=1$, then (since they must be at least $1$ by definition of $L^p$ spaces) we have that $q_0$ and $q_1$ must also both be $1$ (for example, since $\frac{1}{q}$ is a convex combination of the other two reciprocals, the largest one must be $1$, and from that rearranging terms shows the other one is $1$). - In this case, take $g_z=g$ for all $z$ and repeat the proof above (note:isn't this what already happens if we do not consider this case separately?). + In this case, take $g_z=g$ for all $z$ and repeat the proof above (note:ixsn't this what already happens if we do not consider this case separately?). } \end{itemize} @@ -335,31 +335,31 @@ \subsection{Extending the Fourier transform} By Rietz-Thorin interpolation theorem, it can be uniquely extended to bounded linear operators $L^p \to L^q$ whenever $1\leq p \leq 2$ and $q$ is conjugate to $p$. -\begin{comment} This subsection is to be potentially added later -\subsection{Young's Inequality for Convolutions} -Here, we work with $X=Y=\R^d$ with standard scalar product and the usual Lebesgue measure.\\ - -\begin{lemma} - \label{lem:young_convolution} - \uses{} - \lean{} - %\leanok - For any $f\in L^p$ and $g \in L^r$, their convolution - \[ (f * g) (x) = \int_{\R^d} f(x-y) g(y) dy \] - is well-defined (i.e. the right-hand side is integrable for almost every $x$) and, if $\frac{1}{q} = \frac{1}{p} + \frac{1}{r} - 1$, we have - \[ || f * g ||_{L^q} \leq ||f||_{L^p} ||g||_{L^r}\] - - \end{lemma} - \begin{proof} - \uses{thm:riesz_interpolation} % Put any results used in the proof but not in the statement here - % \leanok % uncomment if the lemma has been proven - \begin{itemize} - \item{\textbf{Case 1:} assume $f$ and $g$ are simple functions. Fix $g$ and consider the operator $Tf = f * g$, which is linear by linearity of integrals. - Let $M:= ||g||_{L^r}$. If $r'$ is the conjugate exponent to $r$, then by H\"older's inequality - \[||T(f)||_{L^{\infty}} \] - } - TO BE COMPLETED - \end{itemize} - \end{proof} +% \begin{comment} This subsection is to be potentially added later +% \subsection{Young's Inequality for Convolutions} +% Here, we work with $X=Y=\R^d$ with standard scalar product and the usual Lebesgue measure.\\ + +% \begin{lemma} +% \label{lem:young_convolution} +% \uses{} +% \lean{} +% %\leanok +% For any $f\in L^p$ and $g \in L^r$, their convolution +% \[ (f * g) (x) = \int_{\R^d} f(x-y) g(y) dy \] +% is well-defined (i.e. the right-hand side is integrable for almost every $x$) and, if $\frac{1}{q} = \frac{1}{p} + \frac{1}{r} - 1$, we have +% \[ || f * g ||_{L^q} \leq ||f||_{L^p} ||g||_{L^r}\] + +% \end{lemma} +% \begin{proof} +% \uses{thm:riesz_interpolation} % Put any results used in the proof but not in the statement here +% % \leanok % uncomment if the lemma has been proven +% \begin{itemize} +% \item{\textbf{Case 1:} assume $f$ and $g$ are simple functions. Fix $g$ and consider the operator $Tf = f * g$, which is linear by linearity of integrals. +% Let $M:= ||g||_{L^r}$. If $r'$ is the conjugate exponent to $r$, then by H\"older's inequality +% \[||T(f)||_{L^{\infty}} \] +% } +% TO BE COMPLETED +% \end{itemize} +% \end{proof} \end{comment}