feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation (#31114)

Use the new notation for the Fourier transform and its inverse to clean up `FourierSchwartz`.

- Use notation type class and `Prop`-type classes.
- State all lemmas for the Fourier transform on `SchwartzMap` and not on the coercion to functions.
- Add coercion lemmas.
- Move `FourierTransformCLE` up in the file and use `FourierEquiv` from the abstract notation file.
- Use the notation for the Fourier transform and the Schwartz functions in `PoissonSummation`.
- Add my name to the authors list for this PR and the PR for Plancherel's theorem.
- Some golfing

Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>

Author: mcdoll

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel
+Authors: Sébastien Gouëzel, Moritz Doll
 -/
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.FourierTransformDeriv
@@ -18,6 +18,8 @@ functions, in `fourierTransformCLM`. It is also given as a continuous linear equ
 open Real MeasureTheory MeasureTheory.Measure
 open scoped FourierTransform ComplexInnerProductSpace
 
+noncomputable section
+
 namespace SchwartzMap
 
 variable
@@ -28,9 +30,11 @@ variable
   {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
   [MeasurableSpace V] [BorelSpace V]
 
+section definition
+
 /-- The Fourier transform on a real inner product space, as a continuous linear map on the
 Schwartz space. -/
-noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
+def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
   refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
   · intro f g x
     simp only [fourierIntegral_eq, add_apply, smul_add]
@@ -77,99 +81,129 @@ noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
         apply Finset.le_sup this (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2 (E := V) (F := E))
     _ = _ := by simp [mul_assoc]
 
-@[simp] lemma fourierTransformCLM_apply (f : 𝓢(V, E)) :
-    fourierTransformCLM 𝕜 f = 𝓕 (f : V → E) := rfl
+instance instFourierTransform : FourierTransform 𝓢(V, E) 𝓢(V, E) where
+  fourierTransform f := fourierTransformCLM ℂ f
+
+lemma fourier_coe (f : 𝓢(V, E)) : 𝓕 f = 𝓕 (f : V → E) := rfl
+
+instance instFourierModule : FourierModule 𝕜 𝓢(V, E) 𝓢(V, E) where
+  fourier_add := ContinuousLinearMap.map_add _
+  fourier_smul := (fourierTransformCLM 𝕜).map_smul
+
+@[simp]
+theorem fourierTransformCLM_apply (f : 𝓢(V, E)) :
+    fourierTransformCLM 𝕜 f = 𝓕 f := rfl
+
+instance instFourierTransformInv : FourierTransformInv 𝓢(V, E) 𝓢(V, E) where
+  fourierTransformInv := (compCLMOfContinuousLinearEquiv ℂ (LinearIsometryEquiv.neg ℝ (E := V)))
+      ∘L (fourierTransformCLM ℂ)
+
+lemma fourierInv_coe (f : 𝓢(V, E)) :
+    𝓕⁻ f = 𝓕⁻ (f : V → E) := by
+  ext x
+  exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm
+
+instance instFourierInvModule : FourierInvModule 𝕜 𝓢(V, E) 𝓢(V, E) where
+  fourierInv_add := ContinuousLinearMap.map_add _
+  fourierInv_smul := ((compCLMOfContinuousLinearEquiv 𝕜 (D := V) (E := V) (F := E)
+    (LinearIsometryEquiv.neg ℝ (E := V))) ∘L (fourierTransformCLM 𝕜)).map_smul
 
 variable [CompleteSpace E]
 
+instance instFourierPair : FourierPair 𝓢(V, E) 𝓢(V, E) where
+  inv_fourier := by
+    intro f
+    ext x
+    rw [fourierInv_coe, fourier_coe, f.continuous.fourier_inversion f.integrable (𝓕 f).integrable]
+
+instance instFourierInvPair : FourierInvPair 𝓢(V, E) 𝓢(V, E) where
+  fourier_inv := by
+    intro f
+    ext x
+    rw [fourier_coe, fourierInv_coe, f.continuous.fourier_inversion_inv f.integrable
+      (𝓕 f).integrable]
+
+@[deprecated (since := "2025-11-13")]
+alias fourier_inversion := FourierTransform.inv_fourier
+
+@[deprecated (since := "2025-11-13")]
+alias fourier_inversion_inv := FourierTransform.fourier_inv
+
+/-- The Fourier transform on a real inner product space, as a continuous linear equiv on the
+Schwartz space. -/
+def fourierTransformCLE : 𝓢(V, E) ≃L[𝕜] 𝓢(V, E) where
+  __ := FourierTransform.fourierEquiv 𝕜 𝓢(V, E) 𝓢(V, E)
+  continuous_toFun := (fourierTransformCLM 𝕜).continuous
+  continuous_invFun := ContinuousLinearMap.continuous _
+
 @[simp]
-theorem fourier_inversion (f : 𝓢(V, E)) (x : V) : 𝓕⁻ (𝓕 (f : V → E)) x = f x :=
-  Integrable.fourier_inversion f.integrable (fourierTransformCLM ℂ f).integrable
-    f.continuous.continuousAt
+lemma fourierTransformCLE_apply (f : 𝓢(V, E)) : fourierTransformCLE 𝕜 f = 𝓕 f := rfl
 
 @[simp]
-theorem fourier_inversion_inv (f : 𝓢(V, E)) (x : V) : 𝓕 (𝓕⁻ (f : V → E)) x = f x :=
-  Integrable.fourier_inversion_inv f.integrable (fourierTransformCLM ℂ f).integrable
-    f.continuous.continuousAt
+lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) : (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f := rfl
+
+end definition
+
+section fubini
 
 variable
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
   {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
 
-variable [CompleteSpace F]
+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 (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L[ℂ] F →L[ℂ] G) :
-    ∫ ξ, M (𝓕 (f : V → E) ξ) (g ξ) = ∫ x, M (f x) (𝓕 (g : V → F) x) := by
-  have := VectorFourier.integral_bilin_fourierIntegral_eq_flip M (μ := volume) (ν := volume)
-    (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
-  rwa [flip_innerₗ] at this
+    ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕 g x) := by
+  simpa using VectorFourier.integral_bilin_fourierIntegral_eq_flip M (L := (innerₗ V))
+    continuous_fourierChar continuous_inner f.integrable g.integrable
 
 theorem integral_sesq_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
-    ∫ ξ, M (𝓕 (f : V → E) ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ (g : V → F) x) := by
-  have := VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip M (μ := volume) (ν := volume)
+    ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ g x) := by
+  simpa [fourierInv_coe] using VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip M
     (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
-  rwa [flip_innerₗ] at this
 
 /-- Plancherel's theorem for Schwartz functions.
 
 Version where the multiplication is replaced by a general bilinear form `M`. -/
 theorem integral_sesq_fourier_fourier (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
-    ∫ ξ, M (𝓕 (f : V → E) ξ) (𝓕 (g : V → F) ξ) = ∫ x, M (f x) (g x) := by
-  simpa only [fourierTransformCLM_apply, fourier_inversion]
-    using integral_sesq_fourierIntegral_eq f (fourierTransformCLM ℂ g) M
+    ∫ ξ, M (𝓕 f ξ) (𝓕 g ξ) = ∫ x, M (f x) (g x) := by
+  simpa using integral_sesq_fourierIntegral_eq f (𝓕 g) M
+
+end fubini
+
+section L2
 
 variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
 
 /-- Plancherel's theorem for Schwartz functions. -/
 theorem integral_inner_fourier_fourier (f g : 𝓢(V, H)) :
-    ∫ ξ, ⟪𝓕 (f : V → H) ξ, 𝓕 (g : V → H) ξ⟫ = ∫ x, ⟪f x, g x⟫ :=
+    ∫ ξ, ⟪𝓕 f ξ, 𝓕 g ξ⟫ = ∫ x, ⟪f x, g x⟫ :=
   integral_sesq_fourier_fourier f g (innerSL ℂ)
 
 theorem integral_norm_sq_fourier (f : 𝓢(V, H)) :
-    ∫ ξ, ‖𝓕 (f : V → H) ξ‖^2 = ∫ x, ‖f x‖^2 := by
+    ∫ ξ, ‖𝓕 f ξ‖^2 = ∫ x, ‖f x‖^2 := by
   apply Complex.ofRealLI.injective
-  simp only [← LinearIsometry.integral_comp_comm]
-  convert integral_inner_fourier_fourier f f <;>
-  simp [inner_self_eq_norm_sq_to_K]
+  simpa [← LinearIsometry.integral_comp_comm, inner_self_eq_norm_sq_to_K] using
+    integral_inner_fourier_fourier f f
 
-theorem inner_fourierTransformCLM_toL2_eq (f : 𝓢(V, H)) :
-    ⟪(fourierTransformCLM ℂ f).toLp 2, (fourierTransformCLM ℂ f).toLp 2⟫ =
+theorem inner_fourier_toL2_eq (f : 𝓢(V, H)) :
+    ⟪(𝓕 f).toLp 2, (𝓕 f).toLp 2⟫ =
     ⟪f.toLp 2, f.toLp 2⟫ := by
   simp only [inner_toL2_toL2_eq]
   exact integral_sesq_fourier_fourier f f (innerSL ℂ)
 
-theorem norm_fourierTransformCLM_toL2_eq (f : 𝓢(V, H)) :
-    ‖(fourierTransformCLM ℂ f).toLp 2‖ = ‖f.toLp 2‖ := by
-  simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourierTransformCLM_toL2_eq]
+@[deprecated (since := "2025-11-13")]
+alias inner_fourierTransformCLM_toL2_eq := inner_fourier_toL2_eq
 
-/-- The Fourier transform on a real inner product space, as a continuous linear equiv on the
-Schwartz space. -/
-noncomputable def fourierTransformCLE : 𝓢(V, E) ≃L[𝕜] 𝓢(V, E) where
-  __ := fourierTransformCLM 𝕜
-  invFun := (compCLMOfContinuousLinearEquiv 𝕜 (LinearIsometryEquiv.neg ℝ (E := V)))
-      ∘L (fourierTransformCLM 𝕜)
-  left_inv := by
-    intro f
-    ext x
-    change 𝓕 (𝓕 (f : V → E)) (-x) = f x
-    rw [← fourierIntegralInv_eq_fourierIntegral_neg, Continuous.fourier_inversion f.continuous
-      f.integrable (fourierTransformCLM 𝕜 f).integrable]
-  right_inv := by
-    intro f
-    ext x
-    change 𝓕 (fun (x : V) ↦ ((𝓕 (f : V → E)) (-x) : E)) x = f x
-    simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg, Continuous.fourier_inversion_inv
-      f.continuous f.integrable (fourierTransformCLM 𝕜 f).integrable]
-  continuous_invFun := ContinuousLinearMap.continuous _
+@[simp] theorem norm_fourier_toL2_eq (f : 𝓢(V, H)) :
+    ‖(𝓕 f).toLp 2‖ = ‖f.toLp 2‖ := by
+  simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourier_toL2_eq]
 
-@[simp] lemma fourierTransformCLE_apply (f : 𝓢(V, E)) :
-    fourierTransformCLE 𝕜 f = 𝓕 (f : V → E) := rfl
+@[deprecated (since := "2025-11-13")]
+alias norm_fourierTransformCLM_toL2_eq := norm_fourier_toL2_eq
 
-@[simp] lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) :
-    (fourierTransformCLE 𝕜).symm f = 𝓕⁻ (f : V → E) := by
-  ext x
-  exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm
+end L2
 
 end SchwartzMap

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -211,12 +211,14 @@ end RpowDecay
 
 section Schwartz
 
+open scoped SchwartzMap
+
 /-- **Poisson's summation formula** for Schwartz functions. -/
-theorem SchwartzMap.tsum_eq_tsum_fourierIntegral (f : SchwartzMap ℝ ℂ) (x : ℝ) :
-    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, fourierTransformCLM ℝ f n * fourier n (x : UnitAddCircle) := by
+theorem SchwartzMap.tsum_eq_tsum_fourierIntegral (f : 𝓢(ℝ, ℂ)) (x : ℝ) :
+    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) := by
   -- We know that Schwartz functions are `O(‖x ^ (-b)‖)` for *every* `b`; for this argument we take
   -- `b = 2` and work with that.
   apply Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay f.continuous one_lt_two
-    (f.isBigO_cocompact_rpow (-2)) ((fourierTransformCLM ℝ f).isBigO_cocompact_rpow (-2))
+    (f.isBigO_cocompact_rpow (-2)) ((𝓕 f).isBigO_cocompact_rpow (-2))
 
 end Schwartz