Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-19 13:17 02ecb62a

View on Github →

feat(analysis/fourier): span of monomials is dense in L^p (#8328)

Estimated changes

Modified docs/undergrad.yaml

Modified src/analysis/fourier.lean

added def fourier_Lp

modified theorem orthonormal_fourier

added theorem span_fourier_Lp_closure_eq_top

modified theorem span_fourier_closure_eq_top

Modified src/measure_theory/continuous_map_dense.lean

Modified src/topology/algebra/group.lean

added theorem dense_range.topological_closure_map_subgroup

added theorem subgroup.topological_closure_coe

Modified src/topology/algebra/module.lean

added theorem dense_range.topological_closure_map_submodule