Commit 2022-11-24 18:59 7922df8fView on Github →
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