feat(measure_theory/function/continuous_map_dense): compactly supported functions are dense in L^p (#18710)

We have already the fact that bounded continuous functions are dense in L^p. We refactor the proof to extract an approach that is common to bounded continuous functions and to compactly supported functions, to avoid code duplication as much as possible. We also give elementary versions of the statements (in the form: for all epsilon > 0, there exists g such that...) as they may be easier to use, and specialized versions for integrable functions.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: loefflerd

src/analysis/fourier/add_circle.lean

@@ -263,7 +263,7 @@ lemma coe_fn_fourier_Lp (p : ℝ≥0∞) [fact (1 ≤ p)] (n : ℤ) :
 lemma span_fourier_Lp_closure_eq_top {p : ℝ≥0∞} [fact (1 ≤ p)] (hp : p ≠ ∞) :
   (span ℂ (range (@fourier_Lp T _ p _))).topological_closure = ⊤ :=
 begin
-  convert (continuous_map.to_Lp_dense_range ℂ hp (@haar_add_circle T hT) ℂ
+  convert (continuous_map.to_Lp_dense_range ℂ (@haar_add_circle T hT) hp ℂ
     ).topological_closure_map_submodule (span_fourier_closure_eq_top),
   rw [map_span, range_comp],
   simp only [continuous_linear_map.coe_coe],