feat(analysis/fourier): Fourier series for functions in L2; Parseval'…

…s identity (#11320)

docs/100.yaml

@@ -275,6 +275,10 @@
   author : Yury G. Kudryashov
 76:
   title  : Fourier Series
+  decls   :
+    - fourier_series_repr
+    - has_sum_fourier_series
+  author : Heather Macbeth
 77:
   title  : Sum of kth powers
   decls  :

docs/undergrad.yaml

@@ -435,9 +435,7 @@ Topology:
     inner product space $L^2$: 'measure_theory.L2.inner_product_space'
     its completeness: 'measure_theory.Lp.complete_space'
     Hilbert bases: 'hilbert_basis' # the document specifies "in the separable case" but we don't require this
-    example, the Hilbert basis of trigonometric polynomials: 'fourier_Lp'
-    its orthonormality: 'orthonormal_fourier'
-    its completeness: 'span_fourier_Lp_closure_eq_top'
+    example, the Hilbert basis of trigonometric polynomials: 'fourier_series'
     example, classical Hilbert bases of orthogonal polynomials: ''
     Lax-Milgram theorem: ''
     $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem: ''
@@ -490,7 +488,7 @@ Multivariable calculus:
     Lagrange multipliers: ''
 
 # 10.
-Measures and integral Calculus:
+Measures and integral calculus:
   Measure theory:
     measurable spaces: 'measurable_space'
     sigma-algebras: 'measurable_space'
@@ -520,13 +518,13 @@ Measures and integral Calculus:
     change of variables to spherical co-ordinates: ''
     convolution: ''
     regularization and approximation by convolution: ''
-  Fourier Analysis:
+  Fourier analysis:
     Fourier series of locally integrable periodic real-valued functions: ''
     Riemann-Lebesgue lemma: ''
     convolution product of periodic functions: ''
     Dirichlet theorem: ''
     Fejer theorem: ''
-    Parseval theorem: ''
+    Parseval theorem: 'tsum_sq_fourier_series_repr'
     Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(\R^d)$: ''
     Plancherel’s theorem: ''
 

src/analysis/fourier.lean

@@ -3,18 +3,19 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
+import analysis.complex.circle
+import analysis.inner_product_space.l2_space
 import measure_theory.function.continuous_map_dense
 import measure_theory.function.l2_space
 import measure_theory.measure.haar
-import analysis.complex.circle
 import topology.metric_space.emetric_paracompact
 import topology.continuous_function.stone_weierstrass
 
 /-!
 
 # Fourier analysis on the circle
 
-This file contains basic technical results for a development of Fourier series.
+This file contains basic results on Fourier series.
 
 ## Main definitions
 
@@ -25,6 +26,8 @@ This file contains basic technical results for a development of Fourier series.
 * 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`
+* `fourier_series` is the canonical isometric isomorphism from `Lp ℂ 2 haar_circle` to `ℓ²(ℤ, ℂ)`
+  induced by taking Fourier series
 
 ## Main statements
 
@@ -41,20 +44,15 @@ by continuous functions.
 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².
-
-## TODO
-
-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.
+The last two results together provide that the functions `fourier_Lp 2 n` form a Hilbert basis for
+L²; this is named as `fourier_series`.
 
+Parseval's identity, `tsum_sq_fourier_series_repr`, is a direct consequence of the construction of
+this Hilbert basis.
 -/
 
 noncomputable theory
-open_locale ennreal complex_conjugate
+open_locale ennreal complex_conjugate classical
 open topological_space continuous_map measure_theory measure_theory.measure algebra submodule set
 
 local attribute [instance] fact_one_le_two_ennreal
@@ -81,7 +79,7 @@ end haar_circle
 
 /-! ### Monomials on the circle -/
 
-section fourier
+section monomials
 
 /-- The family of monomials `λ z, z ^ n`, parametrized by `n : ℤ` and considered as bundled
 continuous maps from `circle` to `ℂ`. -/
@@ -169,6 +167,10 @@ 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)
 
+lemma coe_fn_fourier_Lp (p : ℝ≥0∞) [fact (1 ≤ p)] (n : ℤ) :
+  ⇑(fourier_Lp p n) =ᵐ[haar_circle] fourier n :=
+coe_fn_to_Lp 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 ≠ ∞) :
@@ -207,4 +209,53 @@ begin
     (fourier_add_half_inv_index hij)
 end
 
+end monomials
+
+section fourier
+
+/-- We define `fourier_series` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haar_circle`, which by
+definition is an isometric isomorphism from `Lp ℂ 2 haar_circle` to `ℓ²(ℤ, ℂ)`. -/
+def fourier_series : hilbert_basis ℤ ℂ (Lp ℂ 2 haar_circle) :=
+hilbert_basis.mk orthonormal_fourier (span_fourier_Lp_closure_eq_top (by norm_num))
+
+/-- The elements of the Hilbert basis `fourier_series` for `Lp ℂ 2 haar_circle` are the functions
+`fourier_Lp 2`, the monomials `λ z, z ^ n` on the circle considered as elements of `L2`. -/
+@[simp] lemma coe_fourier_series : ⇑fourier_series = fourier_Lp 2 := hilbert_basis.coe_mk _ _
+
+/-- Under the isometric isomorphism `fourier_series` from `Lp ℂ 2 haar_circle` to `ℓ²(ℤ, ℂ)`, the
+`i`-th coefficient is the integral over the circle of `λ t, t ^ (-i) * f t`. -/
+lemma fourier_series_repr (f : Lp ℂ 2 haar_circle) (i : ℤ) :
+  fourier_series.repr f i = ∫ t : circle, t ^ (-i) * f t ∂ haar_circle :=
+begin
+  transitivity ∫ t : circle, conj ((fourier_Lp 2 i : circle → ℂ) t) * f t ∂ haar_circle,
+  { simp [fourier_series.repr_apply_apply f i, measure_theory.L2.inner_def] },
+  apply integral_congr_ae,
+  filter_upwards [coe_fn_fourier_Lp 2 i],
+  intros t ht,
+  rw [ht, ← fourier_neg],
+  simp [-fourier_neg]
+end
+
+/-- The Fourier series of an `L2` function `f` sums to `f`, in the `L2` topology on the circle. -/
+lemma has_sum_fourier_series (f : Lp ℂ 2 haar_circle) :
+  has_sum (λ i, fourier_series.repr f i • fourier_Lp 2 i) f :=
+by simpa using hilbert_basis.has_sum_repr fourier_series f
+
+/-- **Parseval's identity**: the sum of the squared norms of the Fourier coefficients equals the
+`L2` norm of the function. -/
+lemma tsum_sq_fourier_series_repr (f : Lp ℂ 2 haar_circle) :
+  ∑' i : ℤ, ∥fourier_series.repr f i∥ ^ 2 = ∫ t : circle, ∥f t∥ ^ 2 ∂ haar_circle :=
+begin
+  have H₁ : ∥fourier_series.repr f∥ ^ 2 = ∑' i, ∥fourier_series.repr f i∥ ^ 2,
+  { exact_mod_cast lp.norm_rpow_eq_tsum _ (fourier_series.repr f),
+    norm_num },
+  have H₂ : ∥fourier_series.repr f∥ ^ 2 = ∥f∥ ^2 := by simp,
+  have H₃ := congr_arg is_R_or_C.re (@L2.inner_def circle ℂ ℂ _ _ _ _ _ _ _ f f),
+  rw ← integral_re at H₃,
+  { simp only [← norm_sq_eq_inner] at H₃,
+    rw [← H₁, H₂],
+    exact H₃ },
+  { exact L2.integrable_inner f f },
+end
+
 end fourier