Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
The proof of Plancharel's theorem is done, except for one theorem about convolutions that is missing from mathlib (which I didn't notice earlier) and a silly norm-cast lemma that I couldn't figure out. Unfortunately, I couldn't prove that L^1 intersected L^2 is a normed space. I don't understand why, but nothing I tried worked in instance : NormedSpace. This also means that I couldn't even state the following lemmas (The inclusion is DenseInducing, etc.) without throwing errors. I also updated the .tex file, so that the online version should have all the links and the dependency graph should display the progress correctly. (I did not test this, apart from making sure the LaTeX compiles.)
- Loading branch information