Revision #1737 → #2574 · back to history
modifiedFourier series48216a05cc2d
| Field | From #1737 | To #2574 |
|---|
| mathlib.decl | AddCircle.hasSum_fourier_series_of_summable | hasSum_fourier_series_of_summable |
| provenance | ai | ai-moderated |
modifiedSufficient condition for recovery (dual of Nyquist–Shannon)8b8b0c4fe992
| Field | From #1737 | To #2574 |
|---|
| mathlib.decl | AddCircle.hasSum_fourier_series_of_summable | hasSum_fourier_series_of_summable |
| provenance | ai | ai-moderated |
modifiedPeriodic functions have discrete spectra0c2992ec244e
| Field | From #1737 | To #2574 |
|---|
| mathlib.decl | AddCircle.fourierCoeff | fourierCoeff |
| provenance | ai | ai-moderated |