minor changes in README and plancherel (#2)

README.md

@@ -63,7 +63,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. 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 blueprint/src/print.tex`). If you have the Python package `invoke` you can also run `inv bp`.
 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

blueprint/src/chapter/plancherel.tex

@@ -2,22 +2,22 @@ \chapter{Plancherel's Theorem}
 \label{chap:plancherel}
 
 
-\begin{lemma}
+\begin{theorem}
   \label{lem:plancherel}
   \uses{}
   \lean{MeasureTheory.memℒp_fourierIntegral, MeasureTheory.snorm_fourierIntegral} % the full Lean name this corresponds to (can be a comma-separated list)
   \leanok % the *statement* of the lemma is formalized
   Let $V$ be a finite-dimensional inner product space over $\R$ and let $E$ be a normed space over $\C$. Suppose that $f : V \to C$ is in $L^1(V,E)\cap L^2(V,E)$ and let $\widehat{f}$ be the Fourier transform of $f$. Then $\widehat{f}\in L^2(V,E)$ and
   \[\|\widehat{f}\|_{L^2} = \|f\|_{L^2}.\]
-  \end{lemma}
+  \end{theorem}
     \begin{proof}
     % \uses{} % Put any results used in the proof but not in the statement here
     % \leanok % uncomment if the lemma has been proven
     Write proof here
 \end{proof}
 
 \begin{corollary}
-  \label{lem:reparametrization}
+  \label{lem:fourier-is-l2-linear}
   \uses{lem:plancherel} % the (list of) LaTeX labels of the lemmas that are used for this result
   \lean{MeasureTheory.fourierIntegralL2} % the full Lean name this corresponds to (can be a comma-separated list)
   \leanok % the *statement* of the lemma is formalized