Fourier inversion

Stream: PrimeNumberTheorem+

[Sébastien Gouëzel]

I haven't followed the details of the project, but I have seen that you have some Fourier theory somewhere. I don't know if you will need it, but I have just PRed the Fourier inversion formula to mathlib (in inner product spaces, which includes the particular case of the line), in #10810. Don't hold your breath, though, because it will take some time before it gets in (I will need to cut it into smaller PRs for easier reviews).

[Patrick Massot]

@Sébastien Gouëzel please don’t forget to edit the overview and undergrad yaml files in this PR.

[David Loeffler]

Hi Sebastian, this is splendid! if there is anything I can do to help in the reviewing process please ping me. Can Mathlib's results on Fourier series also be sharpened this way (i.e. getting pointwise convergence at continuity points without assuming global continuity of the function as we presently do)?

[Sébastien Gouëzel]

If you want to help with the review, you can definitely review the PRs yourself: anyone can review PRs, not only the official maintainers, and this is very much appreciated! In fact, you would probably be the ideal reviewer for #10833, since it's based on a file you have authored.

[David Loeffler]

Sure, I'll take a look at it!