feat: the Fourier transform is self-adjoint (#10833)

Also extend the notation `𝓕` for the Fourier transform to inner product spaces, introduce a notation `𝓕⁻` for the inverse Fourier transform, and generalize a few results from the real line to inner product spaces.

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -5,7 +5,10 @@ Authors: David Loeffler
 -/
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Measure.Haar.OfBasis
+import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
 
 #align_import analysis.fourier.fourier_transform from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -33,12 +36,17 @@ where `e [x]` is notational sugar for `(e (Multiplicative.ofAdd x) : ℂ)` (avai
 `fourier_transform`). This includes the cases `W` is the dual of `V` and `L` is the canonical
 pairing, or `W = V` and `L` is a bilinear form (e.g. an inner product).
 
-In namespace `fourier`, we consider the more familiar special case when `V = W = 𝕜` and `L` is the
+In namespace `Fourier`, we consider the more familiar special case when `V = W = 𝕜` and `L` is the
 multiplication map (but still allowing `𝕜` to be an arbitrary ring equipped with a measure).
 
 The most familiar case of all is when `V = W = 𝕜 = ℝ`, `L` is multiplication, `μ` is volume, and
-`e` is `Real.fourierChar`, i.e. the character `fun x ↦ exp ((2 * π * x) * I)`. The Fourier integral
-in this case is defined as `Real.fourierIntegral`.
+`e` is `Real.fourierChar`, i.e. the character `fun x ↦ exp ((2 * π * x) * I)` (for which we
+introduce the notation `𝐞` in the locale `FourierTransform`).
+
+Another familiar case (which generalizes the previous one) is when `V = W` is an inner product space
+over `ℝ` and `L` is the scalar product. We introduce two notations `𝓕` for the Fourier transform in
+this case and `𝓕⁻ f (v) = 𝓕 f (-v)` for the inverse Fourier transform. These notations make
+in particular sense for `V = W = ℝ`.
 
 ## Main results
 
@@ -56,6 +64,7 @@ open MeasureTheory Filter
 open scoped Topology
 
 -- To avoid messing around with multiplicative vs. additive characters, we make a notation.
+/-- Notation for multiplicative character applied in an additive setting. -/
 scoped[FourierTransform] notation e "[" x "]" => (e (Multiplicative.ofAdd x) : ℂ)
 
 open FourierTransform
@@ -66,7 +75,9 @@ open FourierTransform
 namespace VectorFourier
 
 variable {𝕜 : Type*} [CommRing 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V]
-  {W : Type*} [AddCommGroup W] [Module 𝕜 W] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {W : Type*} [AddCommGroup W] [Module 𝕜 W]
+  {E F G : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F]
+  [NormedAddCommGroup G] [NormedSpace ℂ G]
 
 section Defs
 
@@ -174,6 +185,63 @@ theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e
 
 end Continuous
 
+section Fubini
+
+variable [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace V] [BorelSpace V]
+  [TopologicalSpace W] [MeasurableSpace W] [BorelSpace W]
+  {e : Multiplicative 𝕜 →* 𝕊} {μ : Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜}
+  {ν : Measure W} [SigmaFinite μ] [SigmaFinite ν] [SecondCountableTopology V]
+
+variable [CompleteSpace E] [CompleteSpace F]
+
+/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
+Version where the multiplication is replaced by a general bilinear form `M`. -/
+theorem integral_bilin_fourierIntegral_eq_flip
+    {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous e)
+    (hL : Continuous fun p : V × W => L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
+    ∫ ξ, M (fourierIntegral e μ L f ξ) (g ξ) ∂ν =
+      ∫ x, M (f x) (fourierIntegral e ν L.flip g x) ∂μ := by
+  by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
+  calc
+  ∫ ξ, M (fourierIntegral e μ L f ξ) (g ξ) ∂ν
+    = ∫ ξ, M.flip (g ξ) (∫ x, e[-L x ξ] • f x ∂μ) ∂ν := rfl
+  _ = ∫ ξ, (∫ x, M.flip (g ξ) (e[-L x ξ] • f x) ∂μ) ∂ν := by
+    congr with ξ
+    apply (ContinuousLinearMap.integral_comp_comm _ _).symm
+    exact (fourier_integral_convergent_iff he hL _).1 hf
+  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e[-L x ξ] • f x) ∂ν) ∂μ := by
+    rw [integral_integral_swap]
+    have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
+      (hg.norm.prod_mul hf.norm).const_mul _
+    apply this.mono
+    · have A : AEStronglyMeasurable (fun (p : W × V) ↦ e[-L p.2 p.1] • f p.2) (ν.prod μ) := by
+        apply (Continuous.aestronglyMeasurable ?_).smul hf.1.snd
+        refine (continuous_induced_rng.mp he).comp (continuous_ofAdd.comp ?_)
+        exact (hL.comp continuous_swap).neg
+      exact M.flip.continuous₂.comp_aestronglyMeasurable (hg.1.fst.prod_mk A)
+    · apply eventually_of_forall
+      rintro ⟨ξ, x⟩
+      simp only [ofAdd_neg, map_inv, coe_inv_unitSphere, SMulHomClass.map_smul,
+        ContinuousLinearMap.flip_apply, Function.uncurry_apply_pair, norm_smul, norm_inv,
+        norm_eq_of_mem_sphere, inv_one, one_mul, norm_mul, norm_norm]
+      exact (M.le_opNorm₂ (f x) (g ξ)).trans (le_of_eq (by ring))
+  _ = ∫ x, (∫ ξ, M (f x) (e[-L.flip ξ x] • g ξ) ∂ν) ∂μ := by simp
+  _ = ∫ x, M (f x) (∫ ξ, e[-L.flip ξ x] • g ξ ∂ν) ∂μ := by
+    congr with x
+    apply ContinuousLinearMap.integral_comp_comm
+    apply (fourier_integral_convergent_iff he _ _).1 hg
+    exact hL.comp continuous_swap
+
+/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint. -/
+theorem integral_fourierIntegral_smul_eq_flip
+    {f : V → ℂ} {g : W → F} (he : Continuous e)
+    (hL : Continuous fun p : V × W => L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
+    ∫ ξ, (fourierIntegral e μ L f ξ) • (g ξ) ∂ν =
+      ∫ x, (f x) • (fourierIntegral e ν L.flip g x) ∂μ :=
+  integral_bilin_fourierIntegral_eq_flip (ContinuousLinearMap.lsmul ℂ ℂ) he hL hf hg
+
+end Fubini
+
 end VectorFourier
 
 /-! ## Fourier theory for functions on `𝕜` -/
@@ -232,12 +300,14 @@ def fourierChar : Multiplicative ℝ →* 𝕊 where
   map_mul' x y := by simp only; rw [toAdd_mul, mul_add, expMapCircle_add]
 #align real.fourier_char Real.fourierChar
 
-theorem fourierChar_apply (x : ℝ) : Real.fourierChar[x] = Complex.exp (↑(2 * π * x) * Complex.I) :=
+@[inherit_doc] scoped[FourierTransform] notation "𝐞" => Real.fourierChar
+
+theorem fourierChar_apply (x : ℝ) : 𝐞[x] = Complex.exp (↑(2 * π * x) * Complex.I) :=
   by rfl
 #align real.fourier_char_apply Real.fourierChar_apply
 
 @[continuity]
-theorem continuous_fourierChar : Continuous Real.fourierChar :=
+theorem continuous_fourierChar : Continuous 𝐞 :=
   (map_continuous expMapCircle).comp (continuous_const.mul continuous_toAdd)
 #align real.continuous_fourier_char Real.continuous_fourierChar
 
@@ -251,23 +321,71 @@ theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type*} [AddCommGroup V]
   by simp_rw [VectorFourier.fourierIntegral, Real.fourierChar_apply, mul_neg, neg_mul]
 #align real.vector_fourier_integral_eq_integral_exp_smul Real.vector_fourierIntegral_eq_integral_exp_smul
 
-/-- The Fourier integral for `f : ℝ → E`, with respect to the standard additive character and
-measure on `ℝ`. -/
-def fourierIntegral (f : ℝ → E) (w : ℝ) :=
-  Fourier.fourierIntegral fourierChar volume f w
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {V : Type*} [NormedAddCommGroup V]
+  [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
+  {W : Type*} [NormedAddCommGroup W]
+  [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W]
+
+open scoped RealInnerProductSpace
+
+/-- The Fourier transform of a function on an inner product space, with respect to the standard
+additive character `ω ↦ exp (2 i π ω)`. -/
+def fourierIntegral (f : V → E) (w : V) : E :=
+  VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f w
 #align real.fourier_integral Real.fourierIntegral
 
-theorem fourierIntegral_def (f : ℝ → E) (w : ℝ) :
-    fourierIntegral f w = ∫ v : ℝ, fourierChar[-(v * w)] • f v :=
-  rfl
-#align real.fourier_integral_def Real.fourierIntegral_def
+/-- The inverse Fourier transform of a function on an inner product space, defined as the Fourier
+transform but with opposite sign in the exponential. -/
+def fourierIntegralInv (f : V → E) (w : V) : E :=
+  VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w
 
 @[inherit_doc] scoped[FourierTransform] notation "𝓕" => Real.fourierIntegral
+@[inherit_doc] scoped[FourierTransform] notation "𝓕⁻" => Real.fourierIntegralInv
+
+lemma fourierIntegral_eq (f : V → E) (w : V) :
+    𝓕 f w = ∫ v, 𝐞[-⟪v, w⟫] • f v := rfl
 
-theorem fourierIntegral_eq_integral_exp_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-    (f : ℝ → E) (w : ℝ) :
+lemma fourierIntegral_eq' (f : V → E) (w : V) :
+    𝓕 f w = ∫ v, Complex.exp ((↑(-2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
+  simp_rw [fourierIntegral_eq, Real.fourierChar_apply, mul_neg, neg_mul]
+
+lemma fourierIntegralInv_eq (f : V → E) (w : V) :
+    𝓕⁻ f w = ∫ v, 𝐞[⟪v, w⟫] • f v := by
+  simp [fourierIntegralInv, VectorFourier.fourierIntegral]
+
+lemma fourierIntegralInv_eq' (f : V → E) (w : V) :
+    𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
+  simp_rw [fourierIntegralInv_eq, Real.fourierChar_apply]
+
+lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V → E) (w : V) :
+    𝓕⁻ f w = 𝓕 f (-w) := by
+  simp [fourierIntegral_eq, fourierIntegralInv_eq]
+
+lemma fourierIntegral_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
+    𝓕 (f ∘ A) w = (𝓕 f) (A w) := by
+  simp only [fourierIntegral_eq, ofAdd_neg, map_inv, coe_inv_unitSphere, Function.comp_apply,
+    ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding,
+    ← A.inner_map_map]
+
+lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
+    𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w) := by
+  simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]
+
+theorem fourierIntegral_real_eq (f : ℝ → E) (w : ℝ) :
+    fourierIntegral f w = ∫ v : ℝ, 𝐞[-(v * w)] • f v :=
+  rfl
+#align real.fourier_integral_def Real.fourierIntegral_real_eq
+
+@[deprecated] alias fourierIntegral_def := fourierIntegral_real_eq -- deprecated on 2024-02-21
+
+theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
     𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v := by
-  simp_rw [fourierIntegral_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]
-#align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_eq_integral_exp_smul
+  simp_rw [fourierIntegral_real_eq, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]
+#align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_real_eq_integral_exp_smul
+
+@[deprecated] alias fourierIntegral_eq_integral_exp_smul :=
+  fourierIntegral_real_eq_integral_exp_smul -- deprecated on 2024-02-21
 
 end Real

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -97,7 +97,7 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
       exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
     -- Minor tidying to finish
     _ = 𝓕 f m := by
-      rw [fourierIntegral_eq_integral_exp_smul]
+      rw [fourierIntegral_real_eq_integral_exp_smul]
       congr 1 with x : 1
       rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
       congr 2