Commit 2022-11-24 18:59 7922df8f

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.