feat(analysis/fourier): monomials on the circle are orthonormal (#6952)

Make the circle into a measure space, using Haar measure, and prove that the monomials `z ^ n` are orthonormal when considered as elements of L^2 on the circle.

Author: hrmacbeth

src/analysis/fourier.lean

@@ -0,0 +1,106 @@
+/-
+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.l2_space
+import measure_theory.haar_measure
+import geometry.manifold.instances.circle
+
+/-!
+
+# Fourier analysis on the circle
+
+This file contains some first steps towards 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 `ℂ`
+
+## Main statements
+
+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.
+
+## TODO
+
+* Show that `submodule.span fourier` is dense in `C(circle, ℂ)`, 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.
+* Show that the image of `submodule.span fourier` under `continuous_map.to_Lp` is dense in the
+  `L^2` space on the circle, and thus that the functions `fourier` form a Hilbert basis.  This
+  follows from the previous result using general theory on approximation by continuous functions.
+
+-/
+
+noncomputable theory
+open topological_space continuous_map measure_theory measure_theory.measure
+
+local attribute [instance] fact_one_le_two_ennreal
+
+section haar_circle
+/-! We make the circle into a measure space, using the Haar measure normalized to have total
+measure 1. -/
+
+instance : measurable_space circle := borel circle
+instance : borel_space circle := ⟨rfl⟩
+
+/-- Haar measure on the circle, normalized to have total measure 1. -/
+def haar_circle : measure circle := haar_measure positive_compacts_univ
+
+instance : probability_measure haar_circle := ⟨haar_measure_self⟩
+
+instance : measure_space circle :=
+{ volume := haar_circle,
+  .. circle.measurable_space }
+
+end haar_circle
+
+section fourier
+
+/-- The family of monomials `λ z, z ^ n`, parametrized by `n : ℤ` and considered as bundled
+continuous maps from `circle` to `ℂ`. -/
+@[simps] def fourier (n : ℤ) : C(circle, ℂ) :=
+{ to_fun := λ z, z ^ n,
+  continuous_to_fun := continuous_subtype_coe.fpow nonzero_of_mem_circle n }
+
+@[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
+
+@[simp] lemma fourier_neg {n : ℤ} {z : circle} : fourier (-n) z = complex.conj (fourier n z) :=
+by simp [← coe_inv_circle_eq_conj z]
+
+@[simp] lemma fourier_add {m n : ℤ} {z : circle} :
+  fourier (m + n) z = (fourier m z) * (fourier n z) :=
+by simp [fpow_add (nonzero_of_mem_circle z)]
+
+/-- 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 :=
+begin
+  have : ↑n * ((↑n)⁻¹ * ↑real.pi * complex.I) = ↑real.pi * complex.I,
+  { have : (n:ℂ) ≠ 0 := by exact_mod_cast hn,
+    field_simp,
+    ring },
+  simp [mul_fpow, ← complex.exp_int_mul, complex.exp_pi_mul_I, this]
+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)) :=
+begin
+  rw orthonormal_iff_ite,
+  intros i j,
+  rw continuous_map.inner_to_Lp haar_circle (fourier i) (fourier j),
+  split_ifs,
+  { simp [h, probability_measure.measure_univ, ← fourier_neg, ← fourier_add, -fourier_to_fun] },
+  simp only [← fourier_add, ← fourier_neg, is_R_or_C.conj_to_complex],
+  have hij : -i + j ≠ 0,
+  { rw add_comm,
+    exact sub_ne_zero.mpr (ne.symm h) },
+  exact integral_zero_of_mul_left_eq_neg (is_mul_left_invariant_haar_measure _)
+    (fourier_add_half_inv_index hij)
+end
+
+end fourier

src/data/complex/exponential.lean

@@ -471,6 +471,14 @@ by rw [← mul_right_inj' (exp_ne_zero x), ← exp_add];
 lemma exp_sub : exp (x - y) = exp x / exp y :=
 by simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]
 
+lemma exp_int_mul (z : ℂ) (n : ℤ) : complex.exp (n * z) = (complex.exp z) ^ n :=
+begin
+  cases n,
+  { apply complex.exp_nat_mul },
+  { simpa [complex.exp_neg, add_comm, ← neg_mul_eq_neg_mul_symm]
+      using complex.exp_nat_mul (-z) (1 + n) },
+end
+
 @[simp] lemma exp_conj : exp (conj x) = conj (exp x) :=
 begin
   dsimp [exp],

src/geometry/manifold/instances/circle.lean

@@ -54,14 +54,30 @@ lemma circle_def : ↑circle = {z : ℂ | abs z = 1} := by { ext, simp }
 
 @[simp] lemma abs_eq_of_mem_circle (z : circle) : abs z = 1 := by { convert z.2, simp }
 
+@[simp] lemma norm_sq_eq_of_mem_circle (z : circle) : norm_sq z = 1 := by simp [norm_sq_eq_abs]
+
+lemma nonzero_of_mem_circle (z : circle) : (z:ℂ) ≠ 0 := nonzero_of_mem_unit_sphere z
+
 instance : group circle :=
 { inv := λ z, ⟨conj z, by simp⟩,
   mul_left_inv := λ z, subtype.ext $ by { simp [has_inv.inv, ← norm_sq_eq_conj_mul_self,
     ← mul_self_abs] },
   .. circle.to_monoid }
 
-@[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = conj z := rfl
-@[simp] lemma coe_div_circle (z w : circle) : ↑(z / w) = ↑z * conj w := rfl
+lemma coe_inv_circle_eq_conj (z : circle) : ↑(z⁻¹) = conj z := rfl
+
+@[simp] lemma coe_inv_circle (z : circle) : ↑(z⁻¹) = (z : ℂ)⁻¹ :=
+begin
+  rw coe_inv_circle_eq_conj,
+  apply eq_inv_of_mul_right_eq_one,
+  rw [mul_comm, ← complex.norm_sq_eq_conj_mul_self],
+  simp,
+end
+
+@[simp] lemma coe_div_circle (z w : circle) : ↑(z / w) = (z:ℂ) / w :=
+show ↑(z * w⁻¹) = (z:ℂ) * w⁻¹, by simp
+
+instance : compact_space circle := metric.sphere.compact_space _ _
 
 -- the following result could instead be deduced from the Lie group structure on the circle using
 -- `topological_group_of_lie_group`, but that seems a little awkward since one has to first provide
@@ -98,6 +114,9 @@ instance : lie_group (𝓡 1) circle :=
 def exp_map_circle (t : ℝ) : circle :=
 ⟨exp (t * I), by simp [exp_mul_I, abs_cos_add_sin_mul_I]⟩
 
+@[simp] lemma exp_map_circle_apply (t : ℝ) : ↑(exp_map_circle t) = complex.exp (t * complex.I) :=
+rfl
+
 /-- The map `λ t, exp (t * I)` from `ℝ` to the unit circle in `ℂ`, considered as a homomorphism of
 groups. -/
 def exp_map_circle_hom : ℝ →+ (additive circle) :=

src/measure_theory/l2_space.lean

@@ -135,4 +135,51 @@ instance inner_product_space : inner_product_space 𝕜 (α →₂[μ] E) :=
 end inner_product_space
 
 end L2
+
+section inner_continuous
+
+variables {α : Type*} [topological_space α] [measure_space α] [borel_space α] {𝕜 : Type*}
+  [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
+variables (μ : measure α) [finite_measure μ]
+
+open_locale bounded_continuous_function
+
+local attribute [instance] fact_one_le_two_ennreal
+
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 (α →₂[μ] 𝕜) _ x y
+
+/-- For bounded continuous functions `f`, `g` on a finite-measure topological space `α`, the L^2
+inner product is the integral of their pointwise inner product. -/
+lemma bounded_continuous_function.inner_to_Lp (f g : α →ᵇ 𝕜) :
+  ⟪bounded_continuous_function.to_Lp 2 μ 𝕜 f, bounded_continuous_function.to_Lp 2 μ 𝕜 g⟫
+  = ∫ x, is_R_or_C.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 μ,
+  filter_upwards [hf_ae, hg_ae],
+  intros x hf hg,
+  rw [hf, hg],
+  simp
+end
+
+variables [compact_space α]
+
+/-- For continuous functions `f`, `g` on a compact, finite-measure topological space `α`, the L^2
+inner product is the integral of their pointwise inner product. -/
+lemma continuous_map.inner_to_Lp (f g : C(α, 𝕜)) :
+  ⟪continuous_map.to_Lp 2 μ 𝕜 f, continuous_map.to_Lp 2 μ 𝕜 g⟫
+  = ∫ x, is_R_or_C.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 μ,
+  filter_upwards [hf_ae, hg_ae],
+  intros x hf hg,
+  rw [hf, hg],
+  simp
+end
+
+end inner_continuous
+
 end measure_theory

src/measure_theory/lp_space.lean

@@ -1761,7 +1761,7 @@ begin
   { apply_instance }
 end
 
-variables (E p μ)
+variables (p μ)
 
 /-- The normed group homomorphism of considering a bounded continuous function on a finite-measure
 space as an element of `Lp`. -/
@@ -1786,11 +1786,16 @@ linear_map.mk_continuous
   _
   Lp_norm_le
 
-variables {E p 𝕜}
+variables {p 𝕜}
+
+lemma coe_fn_to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [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 [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
   [fact (1 ≤ p)] :
-  ∥to_Lp E p μ 𝕜∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
+  ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
 linear_map.mk_continuous_norm_le _ ((measure_univ_nnreal μ) ^ (p.to_real)⁻¹).coe_nonneg _
 
 end bounded_continuous_function
@@ -1803,43 +1808,49 @@ variables [borel_space E] [second_countable_topology E]
 variables [topological_space α] [compact_space α] [borel_space α]
 variables [finite_measure μ]
 
-variables (𝕜 : Type*) [measurable_space 𝕜] (E p μ) [fact (1 ≤ p)]
+variables (𝕜 : Type*) [measurable_space 𝕜] (p μ) [fact (1 ≤ p)]
 
 /-- The bounded linear map of considering a continuous function on a compact finite-measure
 space `α` as an element of `Lp`.  By definition, the norm on `C(α, E)` is the sup-norm, transferred
 from the space `α →ᵇ E` of bounded continuous functions, so this construction is just a matter of
 transferring the structure from `bounded_continuous_function.to_Lp` along the isometry. -/
 def to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] :
   C(α, E) →L[𝕜] (Lp E p μ) :=
-(bounded_continuous_function.to_Lp E p μ 𝕜).comp
+(bounded_continuous_function.to_Lp p μ 𝕜).comp
   (linear_isometry_bounded_of_compact α E 𝕜).to_linear_isometry.to_continuous_linear_map
 
-variables {E p 𝕜}
+variables {p 𝕜}
+
+lemma coe_fn_to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] (f : C(α,  E)) :
+  to_Lp p μ 𝕜 f =ᵐ[μ] f :=
+ae_eq_fun.coe_fn_mk f _
 
 lemma to_Lp_def [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E] (f : C(α, E)) :
-  to_Lp E p μ 𝕜 f
-  = bounded_continuous_function.to_Lp E p μ 𝕜 (linear_isometry_bounded_of_compact α E 𝕜 f) :=
+  to_Lp p μ 𝕜 f
+  = bounded_continuous_function.to_Lp p μ 𝕜 (linear_isometry_bounded_of_compact α E 𝕜 f) :=
 rfl
 
 @[simp] lemma to_Lp_comp_forget_boundedness [normed_field 𝕜] [opens_measurable_space 𝕜]
   [normed_space 𝕜 E] (f : α →ᵇ E) :
-  to_Lp E p μ 𝕜 (bounded_continuous_function.forget_boundedness α E f)
-  = bounded_continuous_function.to_Lp E p μ 𝕜 f :=
+  to_Lp p μ 𝕜 (bounded_continuous_function.forget_boundedness α E f)
+  = bounded_continuous_function.to_Lp p μ 𝕜 f :=
 rfl
 
 @[simp] lemma coe_to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
   (f : C(α, E)) :
-  (to_Lp E p μ 𝕜 f : α →ₘ[μ] E) = f.to_ae_eq_fun μ :=
+  (to_Lp p μ 𝕜 f : α →ₘ[μ] E) = f.to_ae_eq_fun μ :=
 rfl
 
 variables [nondiscrete_normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E]
 
 lemma to_Lp_norm_eq_to_Lp_norm_coe :
-  ∥to_Lp E p μ 𝕜∥ = ∥bounded_continuous_function.to_Lp E p μ 𝕜∥ :=
-(bounded_continuous_function.to_Lp E p μ 𝕜).op_norm_comp_linear_isometry_equiv _
+  ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥
+  = ∥@bounded_continuous_function.to_Lp _ E _ p μ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ :=
+continuous_linear_map.op_norm_comp_linear_isometry_equiv _ _
 
 /-- Bound for the operator norm of `continuous_map.to_Lp`. -/
-lemma to_Lp_norm_le : ∥to_Lp E p μ 𝕜∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
+lemma to_Lp_norm_le :
+  ∥@to_Lp _ E _ p μ _ _ _ _ _ _ _ _ 𝕜 _ _ _ _ _∥ ≤ (measure_univ_nnreal μ) ^ (p.to_real)⁻¹ :=
 by { rw to_Lp_norm_eq_to_Lp_norm_coe, exact bounded_continuous_function.to_Lp_norm_le μ }
 
 end continuous_map

src/topology/compacts.lean

@@ -48,6 +48,12 @@ instance nonempty_compacts_inhabited [inhabited α] : inhabited (nonempty_compac
 @[nolint has_inhabited_instance]
 def positive_compacts: Type* := { s : set α // is_compact s ∧ (interior s).nonempty  }
 
+/-- In a nonempty compact space, `set.univ` is a member of `positive_compacts`, the compact sets
+with nonempty interior. -/
+def positive_compacts_univ {α : Type*} [topological_space α] [compact_space α] [nonempty α] :
+  positive_compacts α :=
+⟨set.univ, compact_univ, by simp⟩
+
 variables {α}
 
 namespace compacts

src/topology/metric_space/basic.lean

@@ -1320,6 +1320,17 @@ open metric
 class proper_space (α : Type u) [pseudo_metric_space α] : Prop :=
 (compact_ball : ∀x:α, ∀r, is_compact (closed_ball x r))
 
+/-- In a proper pseudometric space, all spheres are compact. -/
+lemma is_compact_sphere {α : Type*} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) :
+  is_compact (sphere x r) :=
+compact_of_is_closed_subset (proper_space.compact_ball x r) is_closed_sphere
+  sphere_subset_closed_ball
+
+/-- In a proper pseudometric space, any sphere is a `compact_space` when considered as a subtype. -/
+instance {α : Type*} [pseudo_metric_space α] [proper_space α] (x : α) (r : ℝ) :
+  compact_space (sphere x r) :=
+is_compact_iff_compact_space.mp (is_compact_sphere _ _)
+
 /-- A proper pseudo metric space is sigma compact, and therefore second countable. -/
 @[priority 100] -- see Note [lower instance priority]
 instance second_countable_of_proper [proper_space α] :