feat: Fourier transform as a continuous linear equiv on Schwartz space (#12144)

We define the Fourier transform on the Schwartz space, as a continuous linear equivalence. First, we define it as a continuous linear map (which amounts to showing that the Fourier transform of a Schwartz function is smooth, with explicit bounds for the successive derivatives in terms of various Schwartz seminorms). Then, we extend it to a continuous linear equivalence thanks to Fourier inversion.

Author: sgouezel

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -5,45 +5,106 @@ Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.FourierTransformDeriv
+import Mathlib.Analysis.Fourier.Inversion
 
 /-!
 # Fourier transform on Schwartz functions
 
-This file will construct the Fourier transform as a continuous linear map acting on Schwartz
-functions.
-
-For now, it only contains the fact that the Fourier transform of a Schwartz function is
-differentiable, with an explicit derivative given by a Fourier transform. See
-`SchwartzMap.hasFDerivAt_fourier`.
+This file constructs the Fourier transform as a continuous linear map acting on Schwartz
+functions, in `fourierTransformCLM`. It is also given as a continuous linear equiv, in
+`fourierTransformCLE`.
 -/
 
-open Real Complex TopologicalSpace SchwartzMap MeasureTheory MeasureTheory.Measure VectorFourier
-
-noncomputable section
-
-variable {D : Type*} [NormedAddCommGroup D] [NormedSpace ℝ D]
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  {V : Type*} [NormedAddCommGroup V] [NormedSpace ℂ V]
-  (L : D →L[ℝ] E →L[ℝ] ℝ)
-
-/-- Multiplication by a linear map on Schwartz space: for `f : D → V` a Schwartz function and `L` a
-bilinear map from `D × E` to `ℝ`, we define a new Schwartz function on `D` taking values in the
-space of linear maps from `E` to `V`, given by
-`(VectorFourier.fourierSMulRightSchwartz L f) (v) = -(2 * π * I) • L (v, ⬝) • f v`.
-The point of this definition is that the derivative of the Fourier transform of `f` is the
-Fourier transform of `VectorFourier.fourierSMulRightSchwartz L f`. -/
-def VectorFourier.fourierSMulRightSchwartz : 𝓢(D, V) →L[ℝ] 𝓢(D, E →L[ℝ] V) :=
-  -(2 * π * I) • (bilinLeftCLM (ContinuousLinearMap.smulRightL ℝ E V).flip L.hasTemperateGrowth)
-
-@[simp]
-lemma VectorFourier.fourierSMulRightSchwartz_apply (f : 𝓢(D, V)) (d : D) :
-    VectorFourier.fourierSMulRightSchwartz L f d = -(2 * π * I) • (L d).smulRight (f d) := rfl
-
-/-- The Fourier transform of a Schwartz map `f` has a Fréchet derivative (everywhere in its domain)
-and its derivative is the Fourier transform of the Schwartz map `mul_L_schwartz L f`. -/
-theorem SchwartzMap.hasFDerivAt_fourierIntegral [MeasurableSpace D] [BorelSpace D]
-    {μ : Measure D} [SecondCountableTopology D] [HasTemperateGrowth μ] (f : 𝓢(D, V)) (w : E) :
-    HasFDerivAt (fourierIntegral fourierChar μ L.toLinearMap₂ f)
-      (fourierIntegral fourierChar μ L.toLinearMap₂ (fourierSMulRightSchwartz L f) w) w :=
-  VectorFourier.hasFDerivAt_fourierIntegral L f.integrable
-    (by simpa using f.integrable_pow_mul μ 1) w
+open Real Complex TopologicalSpace SchwartzMap MeasureTheory MeasureTheory.Measure
+
+open scoped FourierTransform BigOperators
+
+namespace SchwartzMap
+
+variable
+  (𝕜 : Type*) [RCLike 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E]
+  {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
+  [MeasurableSpace V] [BorelSpace V]
+
+/-- 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 (fun (f : V → E) ↦ 𝓕 f) ?_ ?_ ?_ ?_
+  · intro f g x
+    simp only [fourierIntegral_eq, Pi.add_apply, smul_add]
+    rw [integral_add]
+    · exact (fourierIntegral_convergent_iff _).2 f.integrable
+    · exact (fourierIntegral_convergent_iff _).2 g.integrable
+  · intro c f x
+    simp only [fourierIntegral_eq, Pi.smul_apply, RingHom.id_apply, smul_comm _ c, integral_smul]
+  · intro f
+    exact Real.contDiff_fourierIntegral (fun n _ ↦ integrable_pow_mul volume f n)
+  · rintro ⟨k, n⟩
+    refine ⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
+       (2 * π) ^ n * (2 * ↑n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card
+         * 2 ^ integrablePower (volume : Measure V) *
+         (∫ (x : V), (1 + ‖x‖) ^ (- (integrablePower (volume : Measure V) : ℝ))) * 2,
+       ⟨by positivity, fun f x ↦ ?_⟩⟩
+    apply (pow_mul_norm_iteratedFDeriv_fourierIntegral_le (f.smooth ⊤)
+      (fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans
+    simp only [mul_assoc]
+    gcongr
+    calc
+    ∑ p in Finset.range (n + 1) ×ˢ Finset.range (k + 1),
+        ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖
+      ≤ ∑ p in Finset.range (n + 1) ×ˢ Finset.range (k + 1),
+        2 ^ integrablePower (volume : Measure V) *
+        (∫ (x : V), (1 + ‖x‖) ^ (- (integrablePower (volume : Measure V) : ℝ))) * 2 *
+        ((Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
+          (schwartzSeminormFamily 𝕜 V E)) f := by
+      apply Finset.sum_le_sum (fun p hp ↦ ?_)
+      simp only [Finset.mem_product, Finset.mem_range] at hp
+      apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 _ _ _).trans
+      simp only [mul_assoc]
+      rw [two_mul]
+      gcongr
+      · apply Seminorm.le_def.1
+        have : (0, p.2) ∈ (Finset.range (n + integrablePower (volume : Measure V) + 1)
+            ×ˢ Finset.range (k + 1)) := by simp [hp.2]
+        apply Finset.le_sup this (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2 (E := V) (F := E))
+      · apply Seminorm.le_def.1
+        have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ (Finset.range
+            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)) := by
+          simp [hp.2]
+          linarith
+        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 := rfl
+
+variable [CompleteSpace E]
+
+/-- 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) (-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
+    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
+
+@[simp] lemma fourierTransformCLE_symm_apply (f : 𝓢(V, E)) :
+    (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f := by
+  ext x
+  exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm