Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-21 19:30 049d2aca

View on Github →

feat(analysis/fourier): Fourier series for functions in L2; Parseval's identity (#11320)

Estimated changes

Modified docs/100.yaml

Modified docs/undergrad.yaml

Modified src/analysis/fourier.lean

added theorem coe_fn_fourier_Lp

added theorem coe_fourier_series

added def fourier_series

added theorem fourier_series_repr

added theorem has_sum_fourier_series

added theorem tsum_sq_fourier_series_repr