feat(Analysis/TemperedDistribution): Fourier transform of derivatives (leanprover-community#34294)

The same theorems as for Schwartz functions follow by using duality.

Author: mcdoll

Mathlib/Analysis/Distribution/TemperedDistribution.lean

@@ -480,6 +480,8 @@ instance instFourierPair : FourierPair 𝓢'(E, F) 𝓢'(E, F) where
 instance instFourierPairInv : FourierInvPair 𝓢'(E, F) 𝓢'(E, F) where
   fourier_fourierInv_eq f := by ext; simp
 
+section embedding
+
 variable [CompleteSpace F]
 
 /-- The distributional Fourier transform and the classical Fourier transform coincide on
@@ -505,6 +507,42 @@ theorem fourierInv_toTemperedDistributionCLM_eq (f : 𝓢(E, F)) :
 @[deprecated (since := "2026-01-14")]
 alias fourierTransformInv_toTemperedDistributionCLM_eq := fourierInv_toTemperedDistributionCLM_eq
 
+end embedding
+
+open LineDeriv Real
+
+/- The line derivative in direction `m` of the Fourier transform is given by the Fourier transform
+of the multiplication with `-(2 * π * Complex.I) • (inner ℝ · m)`. -/
+theorem lineDerivOp_fourier_eq (f : 𝓢'(E, F)) (m : E) :
+    ∂_{m} (𝓕 f) = 𝓕 (- (2 * π * Complex.I) • smulLeftCLM F (inner ℝ · m) f) := by
+  ext u
+  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
+  simp [SchwartzMap.fourier_lineDerivOp_eq, ← smulLeftCLM_ofReal ℂ this]
+
+/- The Fourier transform of line derivative in direction `m` is given by multiplication of
+`(2 * π * Complex.I) • (inner ℝ · m)` with the Fourier transform. -/
+theorem fourier_lineDerivOp_eq (f : 𝓢'(E, F)) (m : E) :
+    𝓕 (∂_{m} f) = (2 * π * Complex.I) • smulLeftCLM F (inner ℝ · m) (𝓕 f) := by
+  ext u
+  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
+  simp [SchwartzMap.lineDerivOp_fourier_eq, ← smulLeftCLM_ofReal ℂ this]
+
+/- The line derivative in direction `m` of the inverse Fourier transform is given by the inverse
+Fourier transform of the multiplication with `(2 * π * Complex.I) • (inner ℝ · m)`. -/
+theorem lineDerivOp_fourierInv_eq (f : 𝓢'(E, F)) (m : E) :
+    ∂_{m} (𝓕⁻ f) = 𝓕⁻ ((2 * π * Complex.I) • smulLeftCLM F (inner ℝ · m) f) := by
+  ext u
+  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
+  simp [SchwartzMap.fourierInv_lineDerivOp_eq, ← smulLeftCLM_ofReal ℂ this]
+
+/- The inverse Fourier transform of line derivative in direction `m` is given by multiplication of
+`-(2 * π * Complex.I) • (inner ℝ · m)` with the inverse Fourier transform. -/
+theorem fourierInv_lineDerivOp_eq (f : 𝓢'(E, F)) (m : E) :
+    𝓕⁻ (∂_{m} f) = -(2 * π * Complex.I) • smulLeftCLM F (inner ℝ · m) (𝓕⁻ f) := by
+  ext u
+  have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
+  simp [SchwartzMap.lineDerivOp_fourierInv_eq, ← smulLeftCLM_ofReal ℂ this]
+
 end Fourier
 
 section DiracDelta