chore(Analysis/Fourier): split type class, add continuity one (#33633)

The combined type-class `FourierModule` causes problems when using `fourier_add` since it needs a `Semiring R`, which does not appear in the statement. Therefore, we split `FourierModule` into `FourierAdd` and `FourierSMul` (similar to the case of `LineDeriv`.
Moreover, we add the class `ContinuousFourier` which states that the Fourier transform is continuous.

Author: mcdoll

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -37,7 +37,10 @@ variable
 section definition
 
 /-- The Fourier transform on a real inner product space, as a continuous linear map on the
-Schwartz space. -/
+Schwartz space.
+
+This definition is only to define the Fourier transform, use `FourierTransform.fourierCLM` instead.
+-/
 def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
   refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
   · intro f g x
@@ -88,12 +91,17 @@ def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
 instance instFourierTransform : FourierTransform 𝓢(V, E) 𝓢(V, E) where
   fourier f := fourierTransformCLM ℂ f
 
-lemma fourier_coe (f : 𝓢(V, E)) : 𝓕 f = 𝓕 (f : V → E) := rfl
-
-instance instFourierModule : FourierModule 𝕜 𝓢(V, E) 𝓢(V, E) where
+instance instFourierAdd : FourierAdd 𝓢(V, E) 𝓢(V, E) where
   fourier_add := ContinuousLinearMap.map_add _
+
+instance instFourierSMul : FourierSMul 𝕜 𝓢(V, E) 𝓢(V, E) where
   fourier_smul := (fourierTransformCLM 𝕜).map_smul
 
+instance instContinuousFourier : ContinuousFourier 𝓢(V, E) 𝓢(V, E) where
+  continuous_fourier := ContinuousLinearMap.continuous _
+
+lemma fourier_coe (f : 𝓢(V, E)) : 𝓕 f = 𝓕 (f : V → E) := rfl
+
 @[simp]
 theorem fourierTransformCLM_apply (f : 𝓢(V, E)) :
     fourierTransformCLM 𝕜 f = 𝓕 f := rfl
@@ -102,16 +110,21 @@ instance instFourierTransformInv : FourierTransformInv 𝓢(V, E) 𝓢(V, E) whe
   fourierInv := (compCLMOfContinuousLinearEquiv ℂ (LinearIsometryEquiv.neg ℝ (E := V)))
       ∘L (fourierTransformCLM ℂ)
 
+instance instFourierInvAdd : FourierInvAdd 𝓢(V, E) 𝓢(V, E) where
+  fourierInv_add := ContinuousLinearMap.map_add _
+
+instance instFourierInvSMul : FourierInvSMul 𝕜 𝓢(V, E) 𝓢(V, E) where
+  fourierInv_smul := ((compCLMOfContinuousLinearEquiv 𝕜 (D := V) (E := V) (F := E)
+    (LinearIsometryEquiv.neg ℝ (E := V))) ∘L (fourierTransformCLM 𝕜)).map_smul
+
+instance instContinuousFourierInv : ContinuousFourierInv 𝓢(V, E) 𝓢(V, E) where
+  continuous_fourierInv := ContinuousLinearMap.continuous _
+
 lemma fourierInv_coe (f : 𝓢(V, E)) :
     𝓕⁻ f = 𝓕⁻ (f : V → E) := by
   ext x
   exact (fourierInv_eq_fourier_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
@@ -134,18 +147,14 @@ alias fourier_inversion := FourierTransform.fourierInv_fourier_eq
 @[deprecated (since := "2025-11-13")]
 alias fourier_inversion_inv := FourierTransform.fourier_fourierInv_eq
 
-/-- 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 _
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformCLE := FourierTransform.fourierCLE
 
-@[simp]
-lemma fourierTransformCLE_apply (f : 𝓢(V, E)) : fourierTransformCLE 𝕜 f = 𝓕 f := rfl
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformCLE_apply := FourierTransform.fourierCLE_apply
 
-@[simp]
-lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) : (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f := rfl
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformCLE_symm_apply := FourierTransform.fourierCLE_symm_apply
 
 end definition
 

Mathlib/Analysis/Distribution/TemperedDistribution.lean

@@ -333,35 +333,53 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F]
   [InnerProductSpace ℝ E] [NormedSpace ℂ F]
   [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
 
-variable (E F) in
-/-- The Fourier transform on tempered distributions as a continuous linear map. -/
-def fourierTransformCLM : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
-  PointwiseConvergenceCLM.precomp F (SchwartzMap.fourierTransformCLM ℂ)
-
 instance instFourierTransform : FourierTransform 𝓢'(E, F) 𝓢'(E, F) where
-  fourier := fourierTransformCLM E F
+  fourier := PointwiseConvergenceCLM.precomp F (fourierCLM ℂ 𝓢(E, ℂ))
 
-@[simp]
-theorem fourierTransformCLM_apply (f : 𝓢'(E, F)) :
-  fourierTransformCLM E F f = 𝓕 f := rfl
+instance instFourierAdd : FourierAdd 𝓢'(E, F) 𝓢'(E, F) where
+  fourier_add := (PointwiseConvergenceCLM.precomp F (fourierCLM ℂ 𝓢(E, ℂ))).map_add
+
+instance instFourierSMul : FourierSMul ℂ 𝓢'(E, F) 𝓢'(E, F) where
+  fourier_smul := (PointwiseConvergenceCLM.precomp F (fourierCLM ℂ 𝓢(E, ℂ))).map_smul
+
+instance instContinuousFourier : ContinuousFourier 𝓢'(E, F) 𝓢'(E, F) where
+  continuous_fourier := (PointwiseConvergenceCLM.precomp F (fourierCLM ℂ 𝓢(E, ℂ))).cont
 
 @[simp]
-theorem fourierTransform_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕 f g = f (𝓕 g) := rfl
+theorem fourier_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕 f g = f (𝓕 g) := rfl
 
-variable (E F) in
-/-- The inverse Fourier transform on tempered distributions as a continuous linear map. -/
-def fourierTransformInvCLM : 𝓢'(E, F) →L[ℂ] 𝓢'(E, F) :=
-  PointwiseConvergenceCLM.precomp F (SchwartzMap.fourierTransformCLE ℂ).symm.toContinuousLinearMap
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformCLM := FourierTransform.fourierCLM
+
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformCLM_apply := FourierTransform.fourierCLM_apply
+
+@[deprecated (since := "2026-01-06")]
+alias fourierTransform_apply := fourier_apply
 
 instance instFourierTransformInv : FourierTransformInv 𝓢'(E, F) 𝓢'(E, F) where
-  fourierInv := fourierTransformInvCLM E F
+  fourierInv := PointwiseConvergenceCLM.precomp F (fourierInvCLM ℂ 𝓢(E, ℂ))
 
-@[simp]
-theorem fourierTransformInvCLM_apply (f : 𝓢'(E, F)) :
-    fourierTransformInvCLM E F f = 𝓕⁻ f := rfl
+instance instFourierInvAdd : FourierInvAdd 𝓢'(E, F) 𝓢'(E, F) where
+  fourierInv_add := (PointwiseConvergenceCLM.precomp F (fourierInvCLM ℂ 𝓢(E, ℂ))).map_add
+
+instance instFourierInvSMul : FourierInvSMul ℂ 𝓢'(E, F) 𝓢'(E, F) where
+  fourierInv_smul := (PointwiseConvergenceCLM.precomp F (fourierInvCLM ℂ 𝓢(E, ℂ))).map_smul
+
+instance instContinuousFourierInv : ContinuousFourierInv 𝓢'(E, F) 𝓢'(E, F) where
+  continuous_fourierInv := (PointwiseConvergenceCLM.precomp F (fourierInvCLM ℂ 𝓢(E, ℂ))).cont
 
 @[simp]
-theorem fourierTransformInv_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕⁻ f g = f (𝓕⁻ g) := rfl
+theorem fourierInv_apply (f : 𝓢'(E, F)) (g : 𝓢(E, ℂ)) : 𝓕⁻ f g = f (𝓕⁻ g) := rfl
+
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformInvCLM := FourierTransform.fourierInvCLM
+
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformInvCLM_apply := FourierTransform.fourierInvCLM_apply
+
+@[deprecated (since := "2026-01-06")]
+alias fourierTransformInv_apply := fourierInv_apply
 
 instance instFourierPair : FourierPair 𝓢'(E, F) 𝓢'(E, F) where
   fourierInv_fourier_eq f := by ext; simp
@@ -373,19 +391,19 @@ variable [CompleteSpace F]
 
 /-- The distributional Fourier transform and the classical Fourier transform coincide on
 `𝓢(E, F)`. -/
-theorem fourierTransform_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
+theorem fourier_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
     𝓕 (f : 𝓢'(E, F)) = 𝓕 f := by
   ext g
   simpa using integral_fourier_smul_eq g f
 
 /-- The distributional inverse Fourier transform and the classical inverse Fourier transform
 coincide on `𝓢(E, F)`. -/
-theorem fourierTransformInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
+theorem fourierInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
     𝓕⁻ (f : 𝓢'(E, F)) = 𝓕⁻ f := calc
   _ = 𝓕⁻ (toTemperedDistributionCLM E F volume (𝓕 (𝓕⁻ f))) := by
     congr; exact (fourier_fourierInv_eq f).symm
   _ = 𝓕⁻ (𝓕 (toTemperedDistributionCLM E F volume (𝓕⁻ f))) := by
-    rw [fourierTransform_toTemperedDistributionCLM_eq]
+    rw [fourier_toTemperedDistributionCLM_eq]
   _ = _ := fourierInv_fourier_eq _
 
 end Fourier

Mathlib/Analysis/Fourier/LpSpace.lean

@@ -16,7 +16,8 @@ In this file we define the Fourier transform on $L^2$ as a linear isometry equiv
 
 ## Main definitions
 
-* `Lp.fourierTransformₗᵢ`: The Fourier transform on $L^2$ as a linear isometry equivalence.
+* `MeasureTheory.Lp.fourierTransformₗᵢ`: The Fourier transform on $L^2$ as a linear isometry
+  equivalence.
 
 ## Main statements
 
@@ -46,7 +47,7 @@ namespace MeasureTheory.Lp
 variable (E F) in
 /-- The Fourier transform on `L2` as a linear isometry equivalence. -/
 def fourierTransformₗᵢ : (Lp (α := E) F 2) ≃ₗᵢ[ℂ] (Lp (α := E) F 2) :=
-  (fourierTransformCLE ℂ (V := E) (E := F)).toLinearEquiv.extendOfIsometry
+  (fourierEquiv ℂ 𝓢(E, F)).extendOfIsometry
     (toLpCLM ℂ (E := E) F 2 volume) (toLpCLM ℂ (E := E) F 2 volume)
     -- Not explicitly stating the measure as being the volume causes time-outs in the proofs below
     (denseRange_toLpCLM ENNReal.ofNat_ne_top) (denseRange_toLpCLM ENNReal.ofNat_ne_top)
@@ -55,9 +56,27 @@ def fourierTransformₗᵢ : (Lp (α := E) F 2) ≃ₗᵢ[ℂ] (Lp (α := E) F 2
 instance instFourierTransform : FourierTransform (Lp (α := E) F 2) (Lp (α := E) F 2) where
   fourier := fourierTransformₗᵢ E F
 
+instance instFourierAdd : FourierAdd (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  fourier_add := (fourierTransformₗᵢ E F).map_add
+
+instance instFourierSMul : FourierSMul ℂ (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  fourier_smul := (fourierTransformₗᵢ E F).map_smul
+
+instance instContinuousFourier : ContinuousFourier (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  continuous_fourier := (fourierTransformₗᵢ E F).continuous
+
 instance instFourierTransformInv : FourierTransformInv (Lp (α := E) F 2) (Lp (α := E) F 2) where
   fourierInv := (fourierTransformₗᵢ E F).symm
 
+instance instFourierInvAdd : FourierInvAdd (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  fourierInv_add := (fourierTransformₗᵢ E F).symm.map_add
+
+instance instFourierInvSMul : FourierInvSMul ℂ (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  fourierInv_smul := (fourierTransformₗᵢ E F).symm.map_smul
+
+instance instContinuousFourierInv : ContinuousFourierInv (Lp (α := E) F 2) (Lp (α := E) F 2) where
+  continuous_fourierInv := (fourierTransformₗᵢ E F).symm.continuous
+
 instance instFourierPair : FourierPair (Lp (α := E) F 2) (Lp (α := E) F 2) where
   fourierInv_fourier_eq := (Lp.fourierTransformₗᵢ E F).symm_apply_apply
 
@@ -103,11 +122,10 @@ theorem fourier_toTemperedDistribution_eq (f : Lp (α := E) F 2) :
   apply DenseRange.induction_on (p := p)
     (SchwartzMap.denseRange_toLpCLM (p := 2) ENNReal.ofNat_ne_top) f
   · apply isClosed_eq
-    · exact ((TemperedDistribution.fourierTransformCLM E F) ∘L
-        (toTemperedDistributionCLM F volume 2)).cont
-    · exact (toTemperedDistributionCLM F volume 2).cont.comp (fourierTransformₗᵢ E F).continuous
+    · exact (fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous
+    · exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous
   intro f
-  simp [p, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq]
+  simp [p, TemperedDistribution.fourier_toTemperedDistributionCLM_eq]
 
 /-- The `𝓢'`-inverse Fourier transform and the `L2`-inverse Fourier transform coincide on `L2`. -/
 theorem fourierInv_toTemperedDistribution_eq (f : Lp (α := E) F 2) :