Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-08 13:02 247a102b

View on Github →

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.)

Estimated changes