Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-24 18:59 7922df8f

View 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 stone_weierstrass.

Estimated changes

deleted theorem coe_fn_fourier_Lp
deleted theorem coe_fourier_series
deleted def fourier
deleted def fourier_Lp
deleted theorem fourier_add
deleted theorem fourier_neg
deleted def fourier_series
deleted theorem fourier_series_repr
deleted def fourier_subalgebra
deleted theorem fourier_subalgebra_coe
deleted theorem fourier_zero
deleted def haar_circle
deleted theorem has_sum_fourier_series
deleted theorem orthonormal_fourier