New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(analysis/fourier): convergence of Fourier series #17913
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good. Given how many times you use (fourier_series.repr (to_Lp 2 haar_add_circle ℂ f) i
for f
a continuous function (and I expect it to show up more and more in the future), would it make sense to introduce f.fourier_coeff i
for this?
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Speed up all 30 declaration with elaboration time > 10s (on my machine).
…o jyxu/identify_interval_ends2
…to to_Lp_injective
This PR/issue depends on: |
Marking this as draft because in the time it took for the prerequisites to get merged, I realised that the changes to "continuous_map.eval_clm" could be done in a different (bettter) way. |
... and the alternative approach doesn't work. Sorry for the noise. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Thanks for the review! bors r+ |
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>
Pull request successfully merged into master. Build succeeded: |
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 off
is absolutely summable, then the Fourier series converges uniformly, and hence pointwise everywhere, tof
. (Note that it is obvious in this case that the Fourier series converges uniformly to something, the difficult part is that the limit is actuallyf
.)homeo_Icc_quot
from ℝ to archimedean groups #17983