feat(Analysis/Fourier): L2 and TemperedDistribution Fourier transforms coincide (leanprover-community#33242)

The Fourier transform on `L2` is defined via extension of the `SchwartzMap` Fourier transform and the Fourier transform
on `TemperedDistribution` is defined via self-adjointness and every `L2` function defines a tempered distribution. We show that these definitions behave as expected and give the same notion of Fourier transform.

Author: mcdoll

Mathlib/Analysis/Fourier/LpSpace.lean

@@ -5,7 +5,7 @@ Authors: Moritz Doll
 -/
 module
 
-public import Mathlib.Analysis.Distribution.FourierSchwartz
+public import Mathlib.Analysis.Distribution.TemperedDistribution
 public import Mathlib.Analysis.Normed.Operator.Extend
 
 /-!
@@ -20,8 +20,10 @@ In this file we define the Fourier transform on $L^2$ as a linear isometry equiv
 
 ## Main statements
 
-* `SchwartzMap.toLp_fourierTransform_eq`: The Fourier transform on `𝓢(E, F)` agrees with the Fourier
+* `SchwartzMap.toLp_fourier_eq`: The Fourier transform on `𝓢(E, F)` agrees with the Fourier
   transform on $L^2$.
+* `MeasureTheory.Lp.fourier_toTemperedDistribution_eq`: The Fourier transform on $L^2$ agrees with
+  the Fourier transform on `𝓢'(E, F)`.
 
 -/
 
@@ -74,7 +76,7 @@ theorem inner_fourier_eq (f g : Lp (α := E) F 2) : ⟪𝓕 f, 𝓕 g⟫ = ⟪f,
 end MeasureTheory.Lp
 
 @[simp]
-theorem SchwartzMap.toLp_fourierTransform_eq (f : 𝓢(E, F)) : 𝓕 (f.toLp 2) = (𝓕 f).toLp 2 := by
+theorem SchwartzMap.toLp_fourier_eq (f : 𝓢(E, F)) : 𝓕 (f.toLp 2) = (𝓕 f).toLp 2 := by
   apply LinearMap.extendOfNorm_eq
   · exact SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top
   use 1
@@ -83,7 +85,7 @@ theorem SchwartzMap.toLp_fourierTransform_eq (f : 𝓢(E, F)) : 𝓕 (f.toLp 2)
   exact (norm_fourier_toL2_eq f).le
 
 @[simp]
-theorem SchwartzMap.toLp_fourierTransformInv_eq (f : 𝓢(E, F)) : 𝓕⁻ (f.toLp 2) = (𝓕⁻ f).toLp 2 := by
+theorem SchwartzMap.toLp_fourierInv_eq (f : 𝓢(E, F)) : 𝓕⁻ (f.toLp 2) = (𝓕⁻ f).toLp 2 := by
   apply LinearMap.extendOfNorm_eq
   · exact SchwartzMap.denseRange_toLpCLM ENNReal.ofNat_ne_top
   use 1
@@ -92,4 +94,30 @@ theorem SchwartzMap.toLp_fourierTransformInv_eq (f : 𝓢(E, F)) : 𝓕⁻ (f.to
   convert (norm_fourier_toL2_eq (𝓕⁻ f)).symm.le
   simp
 
+namespace MeasureTheory.Lp
+
+/-- The `𝓢'`-Fourier transform and the `L2`-Fourier transform coincide on `L2`. -/
+theorem fourier_toTemperedDistribution_eq (f : Lp (α := E) F 2) :
+    𝓕 (f : 𝓢'(E, F)) = (𝓕 f : Lp (α := E) F 2) := by
+  set p := fun f : Lp (α := E) F 2 ↦ 𝓕 (f : 𝓢'(E, F)) = (𝓕 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
+  intro f
+  simp [p, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq]
+
+/-- The `𝓢'`-inverse Fourier transform and the `L2`-inverse Fourier transform coincide on `L2`. -/
+theorem fourierInv_toTemperedDistribution_eq (f : Lp (α := E) F 2) :
+    𝓕⁻ (f : 𝓢'(E, F)) = (𝓕⁻ f : Lp (α := E) F 2) := calc
+  _ = 𝓕⁻ (Lp.toTemperedDistribution (𝓕 (𝓕⁻ f))) := by
+    congr; exact (fourier_fourierInv_eq f).symm
+  _ = 𝓕⁻ (𝓕 (Lp.toTemperedDistribution (𝓕⁻ f))) := by
+    rw [fourier_toTemperedDistribution_eq]
+  _ = _ := fourierInv_fourier_eq _
+
+end MeasureTheory.Lp
+
 end FourierTransform