feat(Analysis/Fourier): introduce notation type class for the Fourier transform (#31115)

The reason for introducing this is that the Fourier transform extends to various function spaces, where
it is no longer defined as an integral. We still want to use the notation `𝓕` in that case.

In the file `FourierSchwartz` it becomes apparent how the current definition of `𝓕` causes a lot of coercions that
should not be there as we lose the information that the Fourier transform of a Schwartz function is again a Schwartz function. Using the new notation type class for Schwartz function is done in a subsequent PR.

Author: mcdoll

Mathlib.lean

@@ -1732,6 +1732,7 @@ import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 import Mathlib.Analysis.Fourier.FourierTransform
 import Mathlib.Analysis.Fourier.FourierTransformDeriv
 import Mathlib.Analysis.Fourier.Inversion
+import Mathlib.Analysis.Fourier.Notation
 import Mathlib.Analysis.Fourier.PoissonSummation
 import Mathlib.Analysis.Fourier.RiemannLebesgueLemma
 import Mathlib.Analysis.Fourier.ZMod

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -31,7 +31,7 @@ variable
 /-- 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
-  refine mkCLM (𝓕 ·) ?_ ?_ ?_ ?_
+  refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
   · intro f g x
     simp only [fourierIntegral_eq, add_apply, smul_add]
     rw [integral_add]
@@ -78,17 +78,17 @@ noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
     _ = _ := by simp [mul_assoc]
 
 @[simp] lemma fourierTransformCLM_apply (f : 𝓢(V, E)) :
-    fourierTransformCLM 𝕜 f = 𝓕 f := rfl
+    fourierTransformCLM 𝕜 f = 𝓕 (f : V → E) := rfl
 
 variable [CompleteSpace E]
 
 @[simp]
-theorem fourier_inversion (f : 𝓢(V, E)) (x : V) : 𝓕⁻ (𝓕 f) x = f x :=
+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
 
 @[simp]
-theorem fourier_inversion_inv (f : 𝓢(V, E)) (x : V) : 𝓕 (𝓕⁻ f) x = f x :=
+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
 
@@ -101,13 +101,13 @@ variable [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 ξ) (g ξ) = ∫ x, M (f x) (𝓕 g x) := by
+    ∫ ξ, 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
 
 theorem integral_sesq_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
-    ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ g x) := by
+    ∫ ξ, 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)
     (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
   rwa [flip_innerₗ] at this
@@ -116,19 +116,19 @@ theorem integral_sesq_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M :
 
 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 ξ) (𝓕 g ξ) = ∫ x, M (f x) (g x) := by
+    ∫ ξ, 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
 
 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 ξ, 𝓕 g ξ⟫ = ∫ x, ⟪f x, g x⟫ :=
+    ∫ ξ, ⟪𝓕 (f : V → H) ξ, 𝓕 (g : V → H) ξ⟫ = ∫ x, ⟪f x, g x⟫ :=
   integral_sesq_fourier_fourier f g (innerSL ℂ)
 
 theorem integral_norm_sq_fourier (f : 𝓢(V, H)) :
-    ∫ ξ, ‖𝓕 f ξ‖^2 = ∫ x, ‖f x‖^2 := by
+    ∫ ξ, ‖𝓕 (f : V → H) ξ‖^2 = ∫ x, ‖f x‖^2 := by
   apply Complex.ofRealLI.injective
   simp only [← LinearIsometry.integral_comp_comm]
   convert integral_inner_fourier_fourier f f <;>
@@ -153,22 +153,22 @@ noncomputable def fourierTransformCLE : 𝓢(V, E) ≃L[𝕜] 𝓢(V, E) where
   left_inv := by
     intro f
     ext x
-    change 𝓕 (𝓕 f) (-x) = f 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 ↦ (𝓕 f) (-x)) x = f 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] lemma fourierTransformCLE_apply (f : 𝓢(V, E)) :
-    fourierTransformCLE 𝕜 f = 𝓕 f := rfl
+    fourierTransformCLE 𝕜 f = 𝓕 (f : V → E) := rfl
 
 @[simp] lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) :
-    (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f := by
+    (fourierTransformCLE 𝕜).symm f = 𝓕⁻ (f : V → E) := by
   ext x
   exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm
 

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -5,6 +5,7 @@ Authors: David Loeffler
 -/
 import Mathlib.Algebra.Group.AddChar
 import Mathlib.Analysis.Complex.Circle
+import Mathlib.Analysis.Fourier.Notation
 import Mathlib.MeasureTheory.Group.Integral
 import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.Bochner.Set
@@ -413,20 +414,17 @@ open scoped RealInnerProductSpace
 
 variable [FiniteDimensional ℝ V]
 
-/-- The Fourier transform of a function on an inner product space, with respect to the standard
-additive character `ω ↦ exp (2 i π ω)`.
-Denoted as `𝓕` within the `Real.FourierTransform` namespace. -/
-def fourierIntegral (f : V → E) (w : V) : E :=
-  VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f w
+instance FourierTransform : FourierTransform (V → E) (V → E) where
+  fourierTransform f := VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f
 
-/-- The inverse Fourier transform of a function on an inner product space, defined as the Fourier
-transform but with opposite sign in the exponential.
-Denoted as `𝓕⁻¹` within the `Real.FourierTransform` namespace. -/
-def fourierIntegralInv (f : V → E) (w : V) : E :=
-  VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w
+instance FourierTransformInv : FourierTransformInv (V → E) (V → E) where
+  fourierTransformInv f w := VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w
 
-@[inherit_doc] scoped[FourierTransform] notation "𝓕" => Real.fourierIntegral
-@[inherit_doc] scoped[FourierTransform] notation "𝓕⁻" => Real.fourierIntegralInv
+@[deprecated (since := "2025-11-12")]
+alias fourierIntegral := FourierTransform.fourierTransform
+
+@[deprecated (since := "2025-11-12")]
+alias fourierIntegralInv := FourierTransform.fourierTransformInv
 
 lemma fourierIntegral_eq (f : V → E) (w : V) :
     𝓕 f w = ∫ v, 𝐞 (-⟪v, w⟫) • f v := rfl
@@ -437,7 +435,7 @@ lemma fourierIntegral_eq' (f : V → E) (w : V) :
 
 lemma fourierIntegralInv_eq (f : V → E) (w : V) :
     𝓕⁻ f w = ∫ v, 𝐞 ⟪v, w⟫ • f v := by
-  simp [fourierIntegralInv, VectorFourier.fourierIntegral]
+  simp [FourierTransformInv.fourierTransformInv, VectorFourier.fourierIntegral]
 
 lemma fourierIntegralInv_eq' (f : V → E) (w : V) :
     𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
@@ -469,7 +467,7 @@ lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V →
   simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]
 
 theorem fourierIntegral_real_eq (f : ℝ → E) (w : ℝ) :
-    fourierIntegral f w = ∫ v : ℝ, 𝐞 (-(v * w)) • f v := by
+    𝓕 f w = ∫ v : ℝ, 𝐞 (-(v * w)) • f v := by
   simp_rw [mul_comm _ w]
   rfl
 

Mathlib/Analysis/Fourier/Notation.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2025 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+import Mathlib.Algebra.Module.Equiv.Defs
+
+/-! # Type classes for the Fourier transform
+
+In this file we define type classes for the Fourier transform and the inverse Fourier transform.
+We introduce the notation `𝓕` and `𝓕⁻` in these classes to denote the Fourier transform and
+the inverse Fourier transform, respectively.
+
+Moreover, we provide type-classes that encode the linear structure and the Fourier inversion
+theorem.
+-/
+
+universe u v w
+
+/--
+The notation typeclass for the Fourier transform.
+
+While the Fourier transform is a linear operator, the notation is for the function `E → F` without
+any additional properties. This makes it possible to use the notation for functions where
+integrability is an issue.
+Moreover, including a scalar multiplication causes problems for inferring the notation type class.
+-/
+class FourierTransform (E : Type u) (F : outParam (Type v)) where
+  /-- `𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent. -/
+  fourierTransform : E → F
+
+/--
+The notation typeclass for the inverse Fourier transform.
+
+While the inverse Fourier transform is a linear operator, the notation is for the function `E → F`
+without any additional properties. This makes it possible to use the notation for functions where
+integrability is an issue.
+Moreover, including a scalar multiplication causes problems for inferring the notation type class.
+-/
+class FourierTransformInv (E : Type u) (F : outParam (Type v)) where
+  /-- `𝓕⁻ f` is the inverse Fourier transform of `f`. The meaning of this notation is
+  type-dependent. -/
+  fourierTransformInv : E → F
+
+namespace FourierTransform
+
+export FourierTransformInv (fourierTransformInv)
+
+@[inherit_doc] scoped notation "𝓕" => fourierTransform
+@[inherit_doc] scoped notation "𝓕⁻" => fourierTransformInv
+
+end FourierTransform
+
+section Module
+
+open scoped FourierTransform
+
+/-- A `FourierModule` is a function space on which the Fourier transform is a linear map. -/
+class FourierModule (R : Type*) (E : Type*) (F : outParam (Type*)) [Add E] [Add F] [SMul R E]
+    [SMul R F] extends FourierTransform E F where
+  fourier_add : ∀ (f g : E), 𝓕 (f + g) = 𝓕 f + 𝓕 g
+  fourier_smul : ∀ (r : R) (f : E), 𝓕 (r • f) = r • 𝓕 f
+
+/-- A `FourierInvModule` is a function space on which the Fourier transform is a linear map. -/
+class FourierInvModule (R : Type*) (E : Type*) (F : outParam (Type*)) [Add E] [Add F] [SMul R E]
+    [SMul R F] extends FourierTransformInv E F where
+  fourierInv_add : ∀ (f g : E), 𝓕⁻ (f + g) = 𝓕⁻ f + 𝓕⁻ g
+  fourierInv_smul : ∀ (r : R) (f : E), 𝓕⁻ (r • f) = r • 𝓕⁻ f
+
+namespace FourierTransform
+
+export FourierModule (fourier_add fourier_smul)
+export FourierInvModule (fourierInv_add fourierInv_smul)
+
+attribute [simp] fourier_add
+attribute [simp] fourier_smul
+attribute [simp] FourierInvModule.fourierInv_add
+attribute [simp] FourierInvModule.fourierInv_smul
+
+variable {R E F : Type*} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F]
+
+section fourierₗ
+
+variable [FourierModule R E F]
+
+variable (R E F) in
+/-- The Fourier transform as a linear map. -/
+def fourierₗ : E →ₗ[R] F where
+  toFun := 𝓕
+  map_add' := fourier_add
+  map_smul' := fourier_smul
+
+@[simp]
+lemma fourierₗ_apply (f : E) : fourierₗ R E F f = 𝓕 f := rfl
+
+@[simp]
+lemma fourier_zero : 𝓕 (0 : E) = 0 :=
+  (fourierₗ R E F).map_zero
+
+end fourierₗ
+
+section fourierInvₗ
+
+variable [FourierInvModule R E F]
+
+variable (R E F) in
+/-- The inverse Fourier transform as a linear map. -/
+def fourierInvₗ : E →ₗ[R] F where
+  toFun := 𝓕⁻
+  map_add' := fourierInv_add
+  map_smul' := fourierInv_smul
+
+@[simp]
+lemma fourierInvₗ_apply (f : E) : fourierInvₗ R E F f = 𝓕⁻ f := rfl
+
+@[simp]
+lemma fourierInv_zero : 𝓕⁻ (0 : E) = 0 :=
+  (fourierInvₗ R E F).map_zero
+
+end fourierInvₗ
+
+end FourierTransform
+
+end Module
+
+section Pair
+
+open FourierTransform
+
+/-- A `FourierPair` is a pair of spaces `E` and `F` such that `𝓕⁻ ∘ 𝓕 = id` on `E`. -/
+class FourierPair (E F : Type*) [FourierTransform E F] [FourierTransformInv F E] where
+  inv_fourier : ∀ (f : E), 𝓕⁻ (𝓕 f) = f
+
+/-- A `FourierInvPair` is a pair of spaces `E` and `F` such that `𝓕 ∘ 𝓕⁻ = id` on `E`. -/
+class FourierInvPair (E F : Type*) [FourierTransform F E] [FourierTransformInv E F] where
+  fourier_inv : ∀ (f : E), 𝓕 (𝓕⁻ f) = f
+
+namespace FourierTransform
+
+export FourierPair (inv_fourier)
+export FourierInvPair (fourier_inv)
+
+attribute [simp] inv_fourier
+attribute [simp] fourier_inv
+
+variable {R E F : Type*} [Semiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F]
+  [FourierModule R E F] [FourierInvModule R F E] [FourierPair E F] [FourierInvPair F E]
+
+variable (R E F) in
+/-- The Fourier transform as a linear equivalence. -/
+def fourierEquiv : E ≃ₗ[R] F where
+  __ := fourierₗ R E F
+  invFun := 𝓕⁻
+  left_inv := inv_fourier
+  right_inv := fourier_inv
+
+@[simp]
+lemma fourierEquiv_apply (f : E) : fourierEquiv R E F f = 𝓕 f := rfl
+
+@[simp]
+lemma fourierEquiv_symm_apply (f : F) : (fourierEquiv R E F).symm f = 𝓕⁻ f := rfl
+
+end FourierTransform
+
+end Pair

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -48,7 +48,8 @@ open ContinuousMap
 `∑' n : ℤ, f (x + n)` is the value at `m` of the Fourier transform of `f`. -/
 theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
     (hf : ∀ K : Compacts ℝ, Summable fun n : ℤ => ‖(f.comp (ContinuousMap.addRight n)).restrict K‖)
-    (m : ℤ) : fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m = 𝓕 f m := by
+    (m : ℤ) : fourierCoeff (Periodic.lift <| f.periodic_tsum_comp_add_zsmul 1) m =
+      𝓕 (f : ℝ → ℂ) m := by
   -- NB: This proof can be shortened somewhat by telescoping together some of the steps in the calc
   -- block, but I think it's more legible this way. We start with preliminaries about the integrand.
   let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨((↑) : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
@@ -87,7 +88,7 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
       simp_rw [eadd]
       exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
     -- Minor tidying to finish
-    _ = 𝓕 f m := by
+    _ = 𝓕 (f : ℝ → ℂ) m := by
       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]
@@ -99,8 +100,8 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
 theorem Real.tsum_eq_tsum_fourierIntegral {f : C(ℝ, ℂ)}
     (h_norm :
       ∀ K : Compacts ℝ, Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict K‖)
-    (h_sum : Summable fun n : ℤ => 𝓕 f n) (x : ℝ) :
-    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 f n * fourier n (x : UnitAddCircle) := by
+    (h_sum : Summable fun n : ℤ => 𝓕 (f : ℝ → ℂ) n) (x : ℝ) :
+    ∑' n : ℤ, f (x + n) = ∑' n : ℤ, 𝓕 (f : ℝ → ℂ) n * fourier n (x : UnitAddCircle) := by
   let F : C(UnitAddCircle, ℂ) :=
     ⟨(f.periodic_tsum_comp_add_zsmul 1).lift, continuous_coinduced_dom.mpr (map_continuous _)⟩
   have : Summable (fourierCoeff F) := by

Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

@@ -354,7 +354,7 @@ theorem _root_.fourierIntegral_gaussian_innerProductSpace' (hb : 0 < b.re) (x w
     ring
 
 theorem _root_.fourierIntegral_gaussian_innerProductSpace (hb : 0 < b.re) (w : V) :
-    𝓕 (fun v ↦ cexp (-b * ‖v‖ ^ 2)) w =
+    𝓕 (fun (v : V) ↦ cexp (-b * ‖v‖ ^ 2)) w =
       (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (-π ^ 2 * ‖w‖ ^ 2 / b) := by
   simpa using fourierIntegral_gaussian_innerProductSpace' hb 0 w
 

docs/overview.yaml

@@ -368,7 +368,7 @@ Analysis:
     Schwartz space: 'SchwartzMap'
 
   Fourier analysis:
-    Fourier transform as an integral: 'Real.fourierIntegral'
+    Fourier transform as an integral: 'Real.fourierIntegral_eq'
     inversion formula: 'Continuous.fourier_inversion'
     Riemann-Lebesgue lemma: 'tendsto_integral_exp_inner_smul_cocompact'
     Parseval formula for Fourier series: 'tsum_sq_fourierCoeff'

docs/undergrad.yaml

@@ -534,7 +534,7 @@ Measures and integral calculus:
     Dirichlet theorem: ''
     Fejer theorem: ''
     Parseval theorem: 'tsum_sq_fourierCoeff'
-    Fourier transform on $\mathrm{L}^1(\R^d)$: 'Real.fourierIntegral'
+    Fourier transform on $\mathrm{L}^1(\R^d)$: 'Real.fourierIntegral_eq'
     Fourier transform on $\mathrm{L}^2(\R^d)$: ''
     Plancherel’s theorem: 'SchwartzMap.integral_inner_fourier_fourier'
     Fourier inversion formula: 'Continuous.fourier_inversion'