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

docs/undergrad.yaml

@@ -352,7 +352,7 @@ Single Variable Real Analysis:
     normal convergence:
     continuity of the limit: 'continuous_of_uniform_approx_of_continuous'
     differentiability of the limit:
-    Weierstrass polynomial approximation theorem:
+    Weierstrass polynomial approximation theorem: 'polynomial_functions_closure_eq_top'
     Weierstrass trigonometric approximation theorem:
   Convexity:
     convex functions of a real variable: 'convex_on'
@@ -421,27 +421,29 @@ Topology:
     continuous linear maps: 'continuous_linear_map'
     norm of a continuous linear map: 'linear_map.mk_continuous'
     uniform convergence norm (sup-norm): 'emetric.tendsto_uniformly_on_iff'
-    normed space of bounded continuous normed-space-valued functions: 'bounded_continuous_function.normed_space'
+    normed space of bounded continuous functions: 'bounded_continuous_function.normed_space'
     its completeness: 'bounded_continuous_function.complete_space'
     Heine-Borel theorem (closed bounded subsets are compact in finite dimension): 'finite_dimensional.proper'
     Riesz' lemma (unit-ball characterization of finite dimension):
     Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
-  Hilbert Spaces:
+  Hilbert spaces:
     Hilbert projection theorem: 'exists_norm_eq_infi_of_complete_convex'
     orthogonal projection onto closed vector subspaces: 'orthogonal_projection_fn'
     dual space: 'normed_space.dual.normed_space'
     Riesz representation theorem: 'inner_product_space.to_dual'
     inner product spaces $l^2$ and $L^2$: 'measure_theory.L2.inner_product_space'
     their completeness: 'measure_theory.Lp.complete_space'
-    Hilbert (orthonormal) bases (in the separable case): 'exists_is_orthonormal_dense_span'
-    Hilbert basis of trigonometric polynomials:
-    Hilbert bases of orthogonal polynomials:
+    Hilbert bases, i.e. complete orthonormal sets (in the separable case): 'exists_is_orthonormal_dense_span'
+    example, the Hilbert basis of trigonometric polynomials: 'fourier_Lp'
+    its orthonormality: 'orthonormal_fourier'
+    its completeness: 'span_fourier_Lp_closure_eq_top'
+    example, classical Hilbert bases of orthogonal polynomials, their orthonormality and completeness:
     Lax-Milgram theorem:
     $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem:
 
 # 9.
 Multivariable calculus:
-  Differential Calculus:
+  Differential calculus:
     differentiable functions on an open subset of $\R^n$: 'differentiable_on'
     differentials (linear tangent functions): 'fderiv'
     directional derivative:
@@ -506,7 +508,7 @@ Measures and integral Calculus:
     integrable functions: 'measure_theory.integrable'
     dominated convergence theorem: 'measure_theory.tendsto_integral_of_dominated_convergence'
     finite dimensional vector-valued integrable functions: 'measure_theory.integrable'
-    continuity of integrals with respect to parameters:
+    continuity of integrals with respect to parameters: 'interval_integral.continuous_of_dominated_interval'
     differentiability of integrals with respect to parameters:
     $\mathrm{L}^p$ spaces where $1 ≤ p ≤ ∞$: 'measure_theory.Lp'
     Completeness of $\mathrm{L}^p$ spaces: 'measure_theory.Lp.complete_space'
@@ -524,7 +526,7 @@ Measures and integral Calculus:
     Dirichlet theorem:
     Fejer theorem:
     Parseval theorem:
-    Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(R^d)$:
+    Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(\R^d)$:
     Plancherel’s theorem:
 
 # 11.

src/analysis/fourier.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
+import measure_theory.continuous_map_dense
 import measure_theory.l2_space
 import measure_theory.haar_measure
 import analysis.complex.circle
@@ -12,14 +13,17 @@ import topology.continuous_function.stone_weierstrass
 
 # Fourier analysis on the circle
 
-This file contains some first steps towards Fourier series.
+This file contains basic technical results for a development of Fourier series.
 
 ## Main definitions
 
 * `haar_circle`, Haar measure on the circle, normalized to have total measure `1`
 * instances `measure_space`, `probability_measure` for the circle with respect to this measure
 * for `n : ℤ`, `fourier n` is the monomial `λ z, z ^ n`, bundled as a continuous map from `circle`
   to `ℂ`
+* for `n : ℤ` and `p : ℝ≥0∞`, `fourier_Lp p n` is an abbreviation for the monomial `fourier n`
+  considered as an element of the Lᵖ-space `Lp ℂ p haar_circle`, via the embedding
+  `continuous_map.to_Lp`
 
 ## Main statements
 
@@ -28,25 +32,34 @@ dense in `C(circle, ℂ)`, i.e. that its `submodule.topological_closure` is `⊤
 the Stone-Weierstrass theorem after checking that it is a subalgebra, closed under conjugation, and
 separates points.
 
-The theorem `orthonormal_fourier` states that the functions `fourier n`, when sent via
-`continuous_map.to_Lp` to the L^2 space on the circle, form an orthonormal set.
+The theorem `span_fourier_Lp_closure_eq_top` states that for `1 ≤ p < ∞` the span of the monomials
+`fourier_Lp` is dense in `Lp ℂ p haar_circle`, i.e. that its `submodule.topological_closure` is
+`⊤`.  This follows from the previous theorem using general theory on approximation of Lᵖ functions
+by continuous functions.
 
-## TODO
+The theorem `orthonormal_fourier` states that the monomials `fourier_Lp 2 n` form an orthonormal
+set (in the L² space of the circle).
+
+By definition, a Hilbert basis for an inner product space is an orthonormal set whose span is
+dense.  Thus, the last two results together establish that the functions `fourier_Lp 2 n` form a
+Hilbert basis for L².
 
-Show that the image of `submodule.span fourier` under `continuous_map.to_Lp` is dense in the `L^2`
-space on the circle. This follows from `span_fourier_closure_eq_top` using general theory (not yet
-in Lean) on approximation by continuous functions.
+## TODO
 
-Paired with `orthonormal_fourier`, this establishes that the functions `fourier` form a Hilbert
-basis for `L^2`.
+Once mathlib has general theory showing that a Hilbert basis of an inner product space induces a
+unitary equivalence with L², the results in this file will give Fourier series applications such
+as Parseval's formula.
 
 -/
 
 noncomputable theory
+open_locale ennreal
 open topological_space continuous_map measure_theory measure_theory.measure algebra submodule set
 
 local attribute [instance] fact_one_le_two_ennreal
 
+/-! ### Choice of measure on the circle -/
+
 section haar_circle
 /-! We make the circle into a measure space, using the Haar measure normalized to have total
 measure 1. -/
@@ -65,6 +78,8 @@ instance : measure_space circle :=
 
 end haar_circle
 
+/-! ### Monomials on the circle -/
+
 section fourier
 
 /-- The family of monomials `λ z, z ^ n`, parametrized by `n : ℤ` and considered as bundled
@@ -142,12 +157,28 @@ continuous_map.subalgebra_complex_topological_closure_eq_top_of_separates_points
   fourier_subalgebra_conj_invariant
 
 /-- The linear span of the monomials `z ^ n` is dense in `C(circle, ℂ)`. -/
-lemma span_fourier_closure_eq_top : (span ℂ (set.range fourier)).topological_closure = ⊤ :=
+lemma span_fourier_closure_eq_top : (span ℂ (range fourier)).topological_closure = ⊤ :=
 begin
   rw ← fourier_subalgebra_coe,
   exact congr_arg subalgebra.to_submodule fourier_subalgebra_closure_eq_top,
 end
 
+/-- The family of monomials `λ z, z ^ n`, parametrized by `n : ℤ` and considered as elements of
+the `Lp` space of functions on `circle` taking values in `ℂ`. -/
+abbreviation fourier_Lp (p : ℝ≥0∞) [fact (1 ≤ p)] (n : ℤ) : Lp ℂ p haar_circle :=
+to_Lp p haar_circle ℂ (fourier n)
+
+/-- For each `1 ≤ p < ∞`, the linear span of the monomials `z ^ n` is dense in
+`Lp ℂ p haar_circle`. -/
+lemma span_fourier_Lp_closure_eq_top {p : ℝ≥0∞} [fact (1 ≤ p)] (hp : p ≠ ∞) :
+  (span ℂ (range (fourier_Lp p))).topological_closure = ⊤ :=
+begin
+  convert (continuous_map.to_Lp_dense_range ℂ hp haar_circle ℂ).topological_closure_map_submodule
+    span_fourier_closure_eq_top,
+  rw [map_span, range_comp],
+  simp
+end
+
 /-- For `n ≠ 0`, a rotation by `n⁻¹ * real.pi` negates the monomial `z ^ n`. -/
 lemma fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (z : circle) :
   fourier n ((exp_map_circle (n⁻¹ * real.pi) * z)) = - fourier n z :=
@@ -160,7 +191,7 @@ begin
 end
 
 /-- The monomials `z ^ n` are an orthonormal set with respect to Haar measure on the circle. -/
-lemma orthonormal_fourier : orthonormal ℂ (λ n, to_Lp 2 haar_circle ℂ (fourier n)) :=
+lemma orthonormal_fourier : orthonormal ℂ (fourier_Lp 2) :=
 begin
   rw orthonormal_iff_ite,
   intros i j,

src/measure_theory/continuous_map_dense.lean

@@ -19,10 +19,10 @@ The result is presented in several versions:
   `measure_theory.Lp.bounded_continuous_function` of `Lp E p μ`, the additive subgroup of
   `Lp E p μ` consisting of equivalence classes containing a continuous representative, is dense in
   `Lp E p μ`.
-* `bounded_continuous_function.dense_range`: For finite-measure `μ`, the continuous linear map
-  `bounded_continuous_function.to_Lp p μ 𝕜` from `α →ᵇ E` to `Lp E p μ` has dense range.
-* `continuous_map.dense_range`: For compact `α` and finite-measure `μ`, the continuous linear map
-  `continuous_map.to_Lp p μ 𝕜` from `C(α, E)` to `Lp E p μ` has dense range.
+* `bounded_continuous_function.to_Lp_dense_range`: For finite-measure `μ`, the continuous linear
+  map `bounded_continuous_function.to_Lp p μ 𝕜` from `α →ᵇ E` to `Lp E p μ` has dense range.
+* `continuous_map.to_Lp_dense_range`: For compact `α` and finite-measure `μ`, the continuous linear
+  map `continuous_map.to_Lp p μ 𝕜` from `C(α, E)` to `Lp E p μ` has dense range.
 
 Note that for `p = ∞` this result is not true:  the characteristic function of the set `[0, ∞)` in
 `ℝ` cannot be continuously approximated in `L∞`.

src/topology/algebra/group.lean

@@ -230,6 +230,10 @@ def subgroup.topological_closure (s : subgroup G) : subgroup G :=
   inv_mem' := λ g m, by simpa [←mem_inv, inv_closure] using m,
   ..s.to_submonoid.topological_closure }
 
+@[simp, to_additive] lemma subgroup.topological_closure_coe {s : subgroup G} :
+  (s.topological_closure : set G) = closure s :=
+rfl
+
 @[to_additive]
 instance subgroup.topological_closure_topological_group (s : subgroup G) :
   topological_group (s.topological_closure) :=
@@ -254,6 +258,16 @@ by convert is_closed_closure
   s.topological_closure ≤ t :=
 closure_minimal h ht
 
+@[to_additive] lemma dense_range.topological_closure_map_subgroup [group H] [topological_space H]
+  [topological_group H] {f : G →* H} (hf : continuous f) (hf' : dense_range f) {s : subgroup G}
+  (hs : s.topological_closure = ⊤) :
+  (s.map f).topological_closure = ⊤ :=
+begin
+  rw set_like.ext'_iff at hs ⊢,
+  simp only [subgroup.topological_closure_coe, subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢,
+  exact hf'.dense_image hf hs
+end
+
 @[to_additive exists_nhds_half_neg]
 lemma exists_nhds_split_inv {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
   ∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v / w ∈ s :=

src/topology/algebra/module.lean

@@ -247,9 +247,23 @@ contained in the `topological_closure` of its image. -/
 lemma _root_.submodule.topological_closure_map [topological_space R] [has_continuous_smul R M]
   [has_continuous_add M] [has_continuous_smul R M₂] [has_continuous_add M₂] (f : M →L[R] M₂)
   (s : submodule R M) :
-  (s.topological_closure.map f.to_linear_map) ≤ (s.map f.to_linear_map).topological_closure :=
+  (s.topological_closure.map ↑f) ≤ (s.map (f : M →ₗ[R] M₂)).topological_closure :=
 image_closure_subset_closure_image f.continuous
 
+/-- Under a dense continuous linear map, a submodule whose `topological_closure` is `⊤` is sent to
+another such submodule.  That is, the image of a dense set under a map with dense range is dense.
+-/
+lemma _root_.dense_range.topological_closure_map_submodule [topological_space R]
+  [has_continuous_smul R M] [has_continuous_add M] [has_continuous_smul R M₂]
+  [has_continuous_add M₂] {f : M →L[R] M₂} (hf' : dense_range f) {s : submodule R M}
+  (hs : s.topological_closure = ⊤) :
+  (s.map (f : M →ₗ[R] M₂)).topological_closure = ⊤ :=
+begin
+  rw set_like.ext'_iff at hs ⊢,
+  simp only [submodule.topological_closure_coe, submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢,
+  exact hf'.dense_image f.continuous hs
+end
+
 /-- The continuous map that is constantly zero. -/
 instance: has_zero (M →L[R] M₂) := ⟨⟨0, continuous_zero⟩⟩
 instance : inhabited (M →L[R] M₂) := ⟨0⟩