mathlib
247a102b - feat(analysis/fourier): convergence of Fourier series (#17913)

Commit
2 years ago
feat(analysis/fourier): convergence of Fourier series (#17913) This PR adds a straightforward but useful criterion for convergence of Fourier series: for a continuous periodic function `f`, if the sequence of Fourier coefficients of `f` is absolutely summable, then the Fourier series converges uniformly, and hence pointwise everywhere, to `f`. (Note that it is obvious in this case that the Fourier series converges uniformly to _something_, the difficult part is that the limit is actually `f`.) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Author
Parents
Loading