mathlib

7922df8f - feat (analysis/fourier): Fourier analysis on the additive circle (#17598)

feat (analysis/fourier): Fourier analysis on the additive circle (#17598) This ticket rewrites the existing `analysis.fourier` file to base things on the additive circle `add_circle T = ℝ / ℤ • T` rather than the unit circle in `ℂ` as before. This makes it much easier to actually evaluate Fourier coefficients, because we can link up with the huge library of lemmas about integration on subsets of ℝ. I've tried to keep the main part of Heather's code much as it was before; I did refactor one lemma about conjugation-invariant subalgebras of `C(X, ℂ)`, moving the bulk of it into `stone_weierstrass`.