reword

blueprint/src/chapter/plancherel.tex

@@ -7,7 +7,7 @@ \chapter{Plancherel's Theorem}
   \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$. If $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
+  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}
     \begin{proof}