[Merged by Bors] - feat(analysis/fourier): convergence of Fourier series

docs/100.yaml

@@ -297,8 +297,8 @@
 76:
   title  : Fourier Series
   decls   :
-    - fourier_series_repr
-    - has_sum_fourier_series
+    - fourier_coeff
+    - has_sum_fourier_series_L2
   author : Heather Macbeth
 77:
   title  : Sum of kth powers

docs/undergrad.yaml

@@ -436,7 +436,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_series'
+    example, the Hilbert basis of trigonometric polynomials: 'fourier_basis'
     example, classical Hilbert bases of orthogonal polynomials: ''
     Lax-Milgram theorem: 'is_coercive.continuous_linear_equiv_of_bilin'
     $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem: ''
@@ -521,12 +521,12 @@ Measures and integral calculus:
     approximation by convolution: 'cont_diff_bump_of_inner.convolution_tendsto_right'
     regularization by convolution: 'has_compact_support.cont_diff_convolution_left'
   Fourier analysis:
-    Fourier series of locally integrable periodic real-valued functions: 'fourier_series'
+    Fourier series of locally integrable periodic real-valued functions: 'fourier_basis'
     Riemann-Lebesgue lemma: ''
     convolution product of periodic functions: ''
     Dirichlet theorem: ''
     Fejer theorem: ''
-    Parseval theorem: 'tsum_sq_fourier_series_repr'
+    Parseval theorem: 'tsum_sq_fourier_coeff'
     Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(\R^d)$: ''
     Plancherel’s theorem: ''
 

src/analysis/fourier/add_circle.lean

@@ -26,36 +26,34 @@ This file contains basic results on Fourier series for functions on the additive
   so we do not declare it as a `measure_space` instance, to avoid confusion.)
 * for `n : ℤ`, `fourier n` is the monomial `λ x, exp (2 π i n x / T)`, bundled as a continuous map
   from `add_circle T` 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_add_circle`, via the embedding
-  `continuous_map.to_Lp`.
-* `fourier_series` is the canonical isometric isomorphism from `Lp ℂ 2 haar_add_circle` to
-  `ℓ²(ℤ, ℂ)` induced by taking Fourier coefficients.
+* `fourier_basis` is the Hilbert basis of `Lp ℂ 2 haar_add_circle` given by the images of the
+  monomials `fourier n`.
+* `fourier_coeff f n`, for `f : add_circle T → ℂ`, is the `n`-th Fourier coefficient of `f`
+  (defined as an integral over `add_circle T`).
 
 ## Main statements
 
 The theorem `span_fourier_closure_eq_top` states that the span of the monomials `fourier n` is
 dense in `C(add_circle T, ℂ)`, i.e. that its `submodule.topological_closure` is `⊤`.  This follows
-from the Stone-Weierstrass theorem after checking that it is a subalgebra, closed under conjugation,
-and separates points.
-
-The theorem `span_fourier_Lp_closure_eq_top` states that for `1 ≤ p < ∞` the span of the monomials
-`fourier_Lp` is dense in the Lᵖ space of `add_circle T`, 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.
-
-The theorem `orthonormal_fourier` states that the monomials `fourier_Lp 2 n` form an orthonormal set
-(in the L² space of `add_circle T` with respect to `haar_add_circle`).
-
-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.
+from the Stone-Weierstrass theorem after checking that the span is a subalgebra, is closed under
+conjugation, and separates points.
+
+Using this and general theory on approximation of Lᵖ functions by continuous functions, we deduce
+(`span_fourier_Lp_closure_eq_top`) that for any `1 ≤ p < ∞`, the span of the Fourier monomials is
+dense in the Lᵖ space of `add_circle T`. For `p = 2` we show (`orthonormal_fourier`) that the
+monomials are also orthonormal, so they form a Hilbert basis for L², which is named as
+`fourier_basis`; in particular, for `L²` functions `f`, the Fourier series of `f` converges to `f`
+in the `L²` topology (`has_sum_fourier_series_L2`). Parseval's identity, `tsum_sq_fourier_coeff`, is
+a direct consequence.
+
+For continuous maps `f : add_circle T → ℂ`, the theorem
+`continuous_map.has_sum_fourier_series_of_summable` states that if the sequence of Fourier
+coefficients of `f` is summable, then the Fourier series `∑ (i:ℤ), f.fourier_coeff i * fourier i`
+converges to `f` in the uniform-convergence topology of `C(add_circle T, ℂ)`.
 -/
 
 noncomputable theory
-open_locale ennreal complex_conjugate classical real
+open_locale ennreal complex_conjugate real
 open topological_space continuous_map measure_theory measure_theory.measure algebra submodule set
 
 variables {T : ℝ}
@@ -135,13 +133,27 @@ def fourier (n : ℤ) : C(add_circle T, ℂ) :=
 
 @[simp] lemma fourier_apply {n : ℤ} {x : add_circle T} : fourier n x = to_circle (n • x) := rfl
 
+@[simp] lemma fourier_coe_apply {n : ℤ} {x : ℝ} :
+  fourier n (x : add_circle T) = complex.exp (2 * π * complex.I * n * x / T) :=
+begin
+  rw [fourier_apply, ←quotient_add_group.coe_zsmul, to_circle, function.periodic.lift_coe,
+    exp_map_circle_apply, complex.of_real_mul, complex.of_real_div, complex.of_real_mul,
+    zsmul_eq_mul, complex.of_real_mul, complex.of_real_int_cast, complex.of_real_bit0,
+    complex.of_real_one],
+  congr' 1, ring,
+end
+
 @[simp] lemma fourier_zero {x : add_circle T} : fourier 0 x = 1 :=
 begin
   induction x using quotient_add_group.induction_on',
-  rw [fourier_apply, to_circle, zero_zsmul, ←quotient_add_group.coe_zero,
-    function.periodic.lift_coe, mul_zero, exp_map_circle_zero, coe_one_unit_sphere],
+  simp only [fourier_coe_apply, algebra_map.coe_zero, mul_zero, zero_mul,
+    zero_div, complex.exp_zero],
 end
 
+@[simp] lemma fourier_eval_zero (n : ℤ) : fourier n (0 : add_circle T) = 1 :=
+by rw [←quotient_add_group.coe_zero, fourier_coe_apply, complex.of_real_zero,
+  mul_zero, zero_div, complex.exp_zero]
+
 @[simp] lemma fourier_one {x : add_circle T} : fourier 1 x = to_circle x :=
 by rw [fourier_apply, one_zsmul]
 
@@ -153,9 +165,17 @@ begin
 end
 
 @[simp] lemma fourier_add {m n : ℤ} {x : add_circle T} :
-  fourier (m + n) x = (fourier m x) * (fourier n x) :=
+  fourier (m + n) x = fourier m x * fourier n x :=
 by simp_rw [fourier_apply, add_zsmul, to_circle_add, coe_mul_unit_sphere]
 
+lemma fourier_norm [fact (0 < T)] (n : ℤ) : ‖@fourier T n‖ = 1 :=
+begin
+  rw continuous_map.norm_eq_supr_norm,
+  have : ∀ (x : add_circle T), ‖fourier n x‖ = 1 := λ x, abs_coe_circle _,
+  simp_rw this,
+  exact @csupr_const _ _ _ has_zero.nonempty _,
+end
+
 /-- For `n ≠ 0`, a translation by `T / 2 / n` negates the function `fourier n`. -/
 lemma fourier_add_half_inv_index {n : ℤ} (hn : n ≠ 0) (hT : 0 < T) (x : add_circle T) :
   fourier n (x + ((T / 2 / n) : ℝ)) = - fourier n x :=
@@ -266,64 +286,114 @@ end
 
 end monomials
 
-section fourier
+section scope_hT -- everything from here on needs `0 < T`
 variables [hT : fact (0 < T)]
 include hT
 
-/-- We define `fourier_series` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haar_add_circle`,
+
+section fourier_coeff
+variables {E : Type} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E]
+
+/-- The `n`-th Fourier coefficient of a function `add_circle T → E`, for `E` a complete normed
+`ℂ`-vector space, defined as the integral over `add_circle T` of `fourier (-n) t • f t`. -/
+def fourier_coeff (f : add_circle T → E) (n : ℤ) : E :=
+∫ (t : add_circle T), fourier (-n) t • f t ∂ haar_add_circle
+
+/-- The Fourier coefficients of a function can be computed as an integral
+over `[a, a + T]` for any real `a`. -/
+lemma fourier_coeff_eq_interval_integral (f : add_circle T → E) (n : ℤ) (a : ℝ) :
+  fourier_coeff f n = (1 / T) • ∫ x in a .. a + T, @fourier T (-n) x • f x :=
+begin
+  have : ∀ (x : ℝ), @fourier T (-n) x • f x = (λ (z : add_circle T), @fourier T (-n) z • f z) x,
+  { intro x, refl, },
+  simp_rw this,
+  rw [fourier_coeff, add_circle.interval_integral_preimage T a,
+    volume_eq_smul_haar_add_circle, integral_smul_measure, ennreal.to_real_of_real hT.out.le,
+    ←smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul],
+end
+
+end fourier_coeff
+
+section fourier_L2
+
+/-- We define `fourier_basis` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haar_add_circle`,
 which by definition is an isometric isomorphism from `Lp ℂ 2 haar_add_circle` to `ℓ²(ℤ, ℂ)`. -/
-def fourier_series : hilbert_basis ℤ ℂ (Lp ℂ 2 $ @haar_add_circle T hT) :=
+def fourier_basis : hilbert_basis ℤ ℂ (Lp ℂ 2 $ @haar_add_circle T hT) :=
 hilbert_basis.mk orthonormal_fourier (span_fourier_Lp_closure_eq_top (by norm_num)).ge
 
-/-- The elements of the Hilbert basis `fourier_series` are the functions `fourier_Lp 2`, i.e. the
+/-- The elements of the Hilbert basis `fourier_basis` are the functions `fourier_Lp 2`, i.e. the
 monomials `fourier n` on the circle considered as elements of `L²`. -/
-@[simp] lemma coe_fourier_series : ⇑(@fourier_series _ hT) = fourier_Lp 2:= hilbert_basis.coe_mk _ _
+@[simp] lemma coe_fourier_basis : ⇑(@fourier_basis _ hT) = 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 `add_circle T` of `λ t, fourier (-i) t * f t`. -/
-lemma fourier_series_repr (f : Lp ℂ 2 $ @haar_add_circle T hT) (i : ℤ) :
-  fourier_series.repr f i = ∫ (t : add_circle T), fourier (-i) t * f t ∂ haar_add_circle :=
+/-- Under the isometric isomorphism `fourier_basis` from `Lp ℂ 2 haar_circle` to `ℓ²(ℤ, ℂ)`, the
+`i`-th coefficient is `fourier_coeff f i`, i.e., the integral over `add_circle T` of
+`λ t, fourier (-i) t * f t` with respect to the Haar measure of total mass 1. -/
+lemma fourier_basis_repr (f : Lp ℂ 2 $ @haar_add_circle T hT) (i : ℤ) :
+  fourier_basis.repr f i = fourier_coeff f i :=
 begin
   transitivity ∫ (t : add_circle T),
     conj (((@fourier_Lp T hT 2 _ i) : add_circle T → ℂ) t) * f t ∂ haar_add_circle,
-  { simp [fourier_series.repr_apply_apply f i, measure_theory.L2.inner_def] },
+  { simp [fourier_basis.repr_apply_apply f i, measure_theory.L2.inner_def] },
   { apply integral_congr_ae,
     filter_upwards [coe_fn_fourier_Lp 2 i] with _ ht,
-    rw [ht, ←fourier_neg] }
+    rw [ht, ←fourier_neg, smul_eq_mul], }
 end
 
 /-- The Fourier series of an `L2` function `f` sums to `f`, in the `L²` space of `add_circle T`. -/
-lemma has_sum_fourier_series (f : Lp ℂ 2 $ @haar_add_circle T hT) :
-  has_sum (λ i, fourier_series.repr f i • fourier_Lp 2 i) f :=
-by simpa using hilbert_basis.has_sum_repr fourier_series f
+lemma has_sum_fourier_series_L2 (f : Lp ℂ 2 $ @haar_add_circle T hT) :
+  has_sum (λ i, fourier_coeff f i • fourier_Lp 2 i) f :=
+by { simp_rw ←fourier_basis_repr, simpa using hilbert_basis.has_sum_repr fourier_basis f }
 
 /-- **Parseval's identity**: for an `L²` function `f` on `add_circle T`, the sum of the squared
 norms of the Fourier coefficients equals the `L²` norm of `f`. -/
-lemma tsum_sq_fourier_series_repr (f : Lp ℂ 2 $ @haar_add_circle T hT) :
-  ∑' i : ℤ, ‖fourier_series.repr f i‖ ^ 2 = ∫ (t : add_circle T), ‖f t‖ ^ 2 ∂ haar_add_circle :=
+lemma tsum_sq_fourier_coeff (f : Lp ℂ 2 $ @haar_add_circle T hT) :
+  ∑' i : ℤ, ‖fourier_coeff f i‖ ^ 2 = ∫ (t : add_circle T), ‖f t‖ ^ 2 ∂ haar_add_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),
+  simp_rw ←fourier_basis_repr,
+  have H₁ : ‖fourier_basis.repr f‖ ^ 2 = ∑' i, ‖fourier_basis.repr f i‖ ^ 2,
+  { exact_mod_cast lp.norm_rpow_eq_tsum _ (fourier_basis.repr f),
     norm_num },
-  have H₂ : ‖fourier_series.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp,
+  have H₂ : ‖fourier_basis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp,
   have H₃ := congr_arg is_R_or_C.re (@L2.inner_def (add_circle T) ℂ ℂ _ _ _ _ f f),
   rw ← integral_re at H₃,
   { simp only [← norm_sq_eq_inner] at H₃,
     rw [← H₁, H₂, H₃], },
   { exact L2.integrable_inner f f },
 end
 
-/-- The Fourier coefficients are given by integrating over the interval `[a, a + T] ⊂ ℝ`. -/
-lemma fourier_series_repr' (f : Lp ℂ 2 $ @haar_add_circle T hT) (n : ℤ) (a : ℝ):
-  fourier_series.repr f n = 1 / T * ∫ x in a .. a + T, @fourier T (-n) x * f x :=
+end fourier_L2
+
+section convergence
+
+variables (f : C(add_circle T, ℂ))
+
+lemma fourier_coeff_to_Lp (n : ℤ) :
+  fourier_coeff (to_Lp 2 haar_add_circle ℂ f) n = fourier_coeff f n :=
+integral_congr_ae (filter.eventually_eq.mul
+  (filter.eventually_of_forall (by tauto))
+  (continuous_map.coe_fn_to_ae_eq_fun haar_add_circle f))
+
+variables {f}
+
+/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series converges
+uniformly to `f`. -/
+lemma has_sum_fourier_series_of_summable (h : summable (fourier_coeff f)) :
+  has_sum (λ i, fourier_coeff f i • fourier i) f :=
 begin
-  have ha : ae_strongly_measurable (λ (t : add_circle T), fourier (-n) t * f t) haar_add_circle :=
-    (map_continuous _).ae_strongly_measurable.mul (Lp.ae_strongly_measurable _),
-  rw [fourier_series_repr, add_circle.interval_integral_preimage T a (ha.smul_measure _),
-    volume_eq_smul_haar_add_circle, integral_smul_measure],
-  have : (T : ℂ) ≠ 0 := by exact_mod_cast hT.out.ne',
-  field_simp [ennreal.to_real_of_real hT.out.le, complex.real_smul],
-  ring,
+  have sum_L2 := has_sum_fourier_series_L2 (to_Lp 2 haar_add_circle ℂ f),
+  simp_rw fourier_coeff_to_Lp at sum_L2,
+  refine continuous_map.has_sum_of_has_sum_Lp (summable_of_summable_norm _) sum_L2,
+  simp_rw [norm_smul, fourier_norm, mul_one, summable_norm_iff],
+  exact h,
 end
 
-end fourier
+/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series of `f`
+converges everywhere pointwise to `f`. -/
+lemma has_pointwise_sum_fourier_series_of_summable
+  (h : summable (fourier_coeff f)) (x : add_circle T) :
+  has_sum (λ i, fourier_coeff f i • fourier i x) (f x) :=
+(continuous_map.eval_clm ℂ x).has_sum (has_sum_fourier_series_of_summable h)
+
+end convergence
+
+end scope_hT

src/measure_theory/function/l2_space.lean

@@ -236,8 +236,8 @@ lemma bounded_continuous_function.inner_to_Lp (f g : α →ᵇ 𝕜) :
   = ∫ x, conj (f x) * g x ∂μ :=
 begin
   apply integral_congr_ae,
-  have hf_ae := f.coe_fn_to_Lp μ,
-  have hg_ae := g.coe_fn_to_Lp μ,
+  have hf_ae := f.coe_fn_to_Lp 2 μ 𝕜,
+  have hg_ae := g.coe_fn_to_Lp 2 μ 𝕜,
   filter_upwards [hf_ae, hg_ae] with _ hf hg,
   rw [hf, hg],
   simp

src/measure_theory/function/lp_space.lean

@@ -2826,11 +2826,11 @@ begin
     (by { rintros - ⟨f, rfl⟩, exact mem_Lp f } : _ ≤ Lp E p μ),
 end
 
-variables (𝕜 : Type*)
+variables (𝕜 : Type*) [fact (1 ≤ p)]
 
 /-- The bounded linear map of considering a bounded continuous function on a finite-measure space
 as an element of `Lp`. -/
-def to_Lp [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] :
+def to_Lp [normed_field 𝕜] [normed_space 𝕜 E] :
   (α →ᵇ E) →L[𝕜] (Lp E p μ) :=
 linear_map.mk_continuous
   (linear_map.cod_restrict
@@ -2840,23 +2840,34 @@ linear_map.mk_continuous
   _
   Lp_norm_le
 
+lemma coe_fn_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] (f : α →ᵇ E) :
+  to_Lp p μ 𝕜 f =ᵐ[μ] f := ae_eq_fun.coe_fn_mk f _
+
 variables {𝕜}
 
-lemma range_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] :
+lemma range_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] :
   ((linear_map.range (to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] Lp E p μ)).to_add_subgroup)
     = measure_theory.Lp.bounded_continuous_function E p μ :=
 range_to_Lp_hom p μ
 
 variables {p}
 
-lemma coe_fn_to_Lp [normed_field 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] (f : α →ᵇ E) :
-  to_Lp p μ 𝕜 f =ᵐ[μ] f :=
-ae_eq_fun.coe_fn_mk f _
-
-lemma to_Lp_norm_le [nontrivially_normed_field 𝕜] [normed_space 𝕜 E] [fact (1 ≤ p)] :
+lemma to_Lp_norm_le [nontrivially_normed_field 𝕜] [normed_space 𝕜 E]:
   ‖(to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] (Lp E p μ))‖ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
 linear_map.mk_continuous_norm_le _ ((measure_univ_nnreal μ) ^ (p.to_real)⁻¹).coe_nonneg _
 
+lemma to_Lp_inj {f g : α →ᵇ E} [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E] :
+  to_Lp p μ 𝕜 f = to_Lp p μ 𝕜 g ↔ f = g :=
+begin
+  refine ⟨λ h, _, by tauto⟩,
+  rw [←fun_like.coe_fn_eq, ←(map_continuous f).ae_eq_iff_eq μ (map_continuous g)],
+  refine (coe_fn_to_Lp p μ 𝕜 f).symm.trans (eventually_eq.trans _ $ coe_fn_to_Lp p μ 𝕜 g),
+  rw h,
+end
+
+lemma to_Lp_injective [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E] :
+  function.injective ⇑(to_Lp p μ 𝕜 : (α →ᵇ E) →L[𝕜] (Lp E p μ)) := λ f g hfg, (to_Lp_inj μ).mp hfg
+
 end bounded_continuous_function
 
 namespace continuous_map
@@ -2906,7 +2917,28 @@ rfl
   (to_Lp p μ 𝕜 f : α →ₘ[μ] E) = f.to_ae_eq_fun μ :=
 rfl
 
-variables [nontrivially_normed_field 𝕜] [normed_space 𝕜 E]
+lemma to_Lp_injective [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E] :
+  function.injective ⇑(to_Lp p μ 𝕜 : C(α, E) →L[𝕜] (Lp E p μ)) :=
+(bounded_continuous_function.to_Lp_injective _).comp
+  (linear_isometry_bounded_of_compact α E 𝕜).injective
+
+lemma to_Lp_inj {f g : C(α, E)} [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E] :
+  to_Lp p μ 𝕜 f = to_Lp p μ 𝕜 g ↔ f = g :=
+(to_Lp_injective μ).eq_iff
+
+variables {μ}
+
+/-- If a sum of continuous functions `g n` is convergent, and the same sum converges in `Lᵖ` to `h`,
+then in fact `g n` converges uniformly to `h`.  -/
+lemma has_sum_of_has_sum_Lp {β : Type*} [μ.is_open_pos_measure] [normed_field 𝕜] [normed_space 𝕜 E]
+  {g : β → C(α, E)} {f : C(α, E)} (hg : summable g)
+  (hg2 : has_sum (to_Lp p μ 𝕜 ∘ g) (to_Lp p μ 𝕜 f)) : has_sum g f :=
+begin
+  convert summable.has_sum hg,
+  exact to_Lp_injective μ (hg2.unique ((to_Lp p μ 𝕜).has_sum $ summable.has_sum hg)),
+end
+
+variables (μ) [nontrivially_normed_field 𝕜] [normed_space 𝕜 E]
 
 lemma to_Lp_norm_eq_to_Lp_norm_coe :
   ‖(to_Lp p μ 𝕜 : C(α, E) →L[𝕜] (Lp E p μ))‖