feat: the Fourier transform of a Schwartz function is differentiable (#…

…10268)

Mathlib.lean

@@ -751,6 +751,7 @@ import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
+import Mathlib.Analysis.Distribution.FourierSchwartz
 import Mathlib.Analysis.Distribution.SchwartzSpace
 import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Fourier.FourierTransform

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import Mathlib.Analysis.Distribution.SchwartzSpace
+import Mathlib.Analysis.Fourier.FourierTransformDeriv
+import Mathlib.Analysis.SpecialFunctions.JapaneseBracket
+
+/-!
+# 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`.
+-/
+
+open Real Complex MeasureTheory Filter TopologicalSpace SchwartzSpace SchwartzMap MeasureTheory
+  MeasureTheory.Measure FiniteDimensional 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.mul_L_schwartz 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.mul_L_schwartz L f`. -/
+def VectorFourier.mul_L_schwartz : 𝓢(D, V) →L[ℝ] 𝓢(D, E →L[ℝ] V) :=
+  -(2 * π * I) • (bilinLeftCLM (ContinuousLinearMap.smulRightL ℝ E V).flip L.hasTemperateGrowth)
+
+lemma VectorFourier.mul_L_schwartz_apply (f : 𝓢(D, V)) (d : D) :
+    VectorFourier.mul_L_schwartz L f d = VectorFourier.mul_L L f d := rfl
+
+lemma SchwartzMap.integrable_pow_mul [MeasurableSpace D] [BorelSpace D] [FiniteDimensional ℝ D]
+    (f : 𝓢(D, V)) {μ : Measure D} (k : ℕ) [IsAddHaarMeasure μ] :
+    Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ := by
+  let l := finrank ℝ D + 1 + k
+  obtain ⟨C, C_nonneg, hC⟩ : ∃ C, 0 ≤ C ∧ ∀ x, (1 + ‖x‖) ^ l * ‖f x‖ ≤ C := by
+    let m : ℕ × ℕ := (l, 0)
+    refine ⟨2 ^ m.1 * (Finset.Iic m).sup (fun m => SchwartzMap.seminorm ℝ m.1 m.2) f, by positivity,
+      fun x ↦ ?_⟩
+    simpa using f.one_add_le_sup_seminorm_apply (m := m) (k := l) (n := 0) (𝕜 := ℝ) le_rfl le_rfl x
+  have : Integrable (fun x : D => C * (1 + ‖x‖) ^ (-((finrank ℝ D + 1 : ℕ) : ℝ))) μ := by
+    apply (integrable_one_add_norm ?_).const_mul
+    exact Nat.cast_lt.mpr Nat.le.refl
+  apply this.mono ((aestronglyMeasurable_id.norm.pow _).mul f.continuous.aestronglyMeasurable.norm)
+    (eventually_of_forall (fun x ↦ ?_))
+  conv_rhs => rw [norm_of_nonneg (by positivity), rpow_neg (by positivity), ← div_eq_mul_inv]
+  rw [le_div_iff' (by positivity)]
+  simp only [id_eq, Pi.mul_apply, Pi.pow_apply, norm_mul, norm_pow, norm_norm, rpow_nat_cast]
+  calc
+    (1 + ‖x‖) ^ (finrank ℝ D + 1) * (‖x‖ ^ k * ‖f x‖)
+      ≤ (1 + ‖x‖) ^ (finrank ℝ D + 1) * ((1 + ‖x‖) ^ k * ‖f x‖) := by gcongr; simp
+    _ = (1 + ‖x‖) ^ (finrank ℝ D + 1 + k) * ‖f x‖ := by simp only [pow_add, mul_assoc]
+    _ ≤ C := hC x
+
+lemma SchwartzMap.integrable [MeasurableSpace D] [BorelSpace D] [FiniteDimensional ℝ D]
+    (f : 𝓢(D, V)) {μ : Measure D} [IsAddHaarMeasure μ] :
+    Integrable f μ :=
+  (f.integrable_pow_mul (μ := μ) 0).mono f.continuous.aestronglyMeasurable
+    (eventually_of_forall (fun _ ↦ by simp))
+
+attribute [local instance 200] secondCountableTopologyEither_of_left
+
+/-- 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_fourier [CompleteSpace V] [MeasurableSpace D] [BorelSpace D]
+    {μ : Measure D} [FiniteDimensional ℝ D] [IsAddHaarMeasure μ] (f : 𝓢(D, V)) (w : E) :
+    HasFDerivAt (fourierIntegral fourierChar μ L.toLinearMap₂ f)
+      (fourierIntegral fourierChar μ L.toLinearMap₂ (mul_L_schwartz L f) w) w :=
+  VectorFourier.hasFDerivAt_fourier L f.integrable
+    (by simpa using f.integrable_pow_mul (μ := μ) 1) w

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -610,7 +610,6 @@ section TemperateGrowth
 
 /-! ### Functions of temperate growth -/
 
-
 /-- A function is called of temperate growth if it is smooth and all iterated derivatives are
 polynomially bounded. -/
 def _root_.Function.HasTemperateGrowth (f : E → F) : Prop :=
@@ -635,6 +634,35 @@ theorem _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {f
   exact Finset.le_sup hN
 #align function.has_temperate_growth.norm_iterated_fderiv_le_uniform_aux Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux
 
+lemma _root_.Function.HasTemperateGrowth.of_fderiv {f : E → F}
+    (h'f : Function.HasTemperateGrowth (fderiv ℝ f)) (hf : Differentiable ℝ f) {k : ℕ} {C : ℝ}
+    (h : ∀ x, ‖f x‖ ≤ C * (1 + ‖x‖) ^ k) :
+    Function.HasTemperateGrowth f := by
+  refine ⟨contDiff_top_iff_fderiv.2 ⟨hf, h'f.1⟩ , fun n ↦ ?_⟩
+  rcases n with rfl|m
+  · exact ⟨k, C, fun x ↦ by simpa using h x⟩
+  · rcases h'f.2 m with ⟨k', C', h'⟩
+    refine ⟨k', C', fun x ↦ ?_⟩
+    simpa only [ContinuousLinearMap.strongUniformity_topology_eq, Function.comp_apply,
+      LinearIsometryEquiv.norm_map, iteratedFDeriv_succ_eq_comp_right] using h' x
+
+lemma _root_.Function.HasTemperateGrowth.zero :
+    Function.HasTemperateGrowth (fun _ : E ↦ (0 : F)) := by
+  refine ⟨contDiff_const, fun n ↦ ⟨0, 0, fun x ↦ ?_⟩⟩
+  simp only [iteratedFDeriv_zero_fun, Pi.zero_apply, norm_zero, forall_const]
+  positivity
+
+lemma _root_.Function.HasTemperateGrowth.const (c : F) :
+    Function.HasTemperateGrowth (fun _ : E ↦ c) :=
+  .of_fderiv (by simpa using .zero) (differentiable_const c) (k := 0) (C := ‖c‖) (fun x ↦ by simp)
+
+lemma _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) :
+    Function.HasTemperateGrowth f := by
+  apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_)
+  · have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]
+    simpa [this] using .const _
+  · exact (f.le_op_norm x).trans (by simp [mul_add])
+
 end TemperateGrowth
 
 section CLM

Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

@@ -95,25 +95,25 @@ theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ
   rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul]
 #align finite_integral_rpow_sub_one_pow_aux finite_integral_rpow_sub_one_pow_aux
 
-theorem finite_integral_one_add_norm [MeasureSpace E] [BorelSpace E]
-    [(volume : Measure E).IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
-    (∫⁻ x : E, ENNReal.ofReal ((1 + ‖x‖) ^ (-r))) < ∞ := by
+theorem finite_integral_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
+    [μ.IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
+    (∫⁻ x : E, ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ) < ∞ := by
   have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
   -- We start by applying the layer cake formula
   have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) :=
     -- porting note: was `by measurability`
     (measurable_norm.const_add _).pow_const _
   have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
-  rw [lintegral_eq_lintegral_meas_le volume (eventually_of_forall h_pos) h_meas.aemeasurable]
-  have h_int : ∀ t, 0 < t → volume {a : E | t ≤ (1 + ‖a‖) ^ (-r)} =
-      volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) := fun t ht ↦ by
+  rw [lintegral_eq_lintegral_meas_le μ (eventually_of_forall h_pos) h_meas.aemeasurable]
+  have h_int : ∀ t, 0 < t → μ {a : E | t ≤ (1 + ‖a‖) ^ (-r)} =
+      μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) := fun t ht ↦ by
     congr 1
     ext x
     simp only [mem_setOf_eq, mem_closedBall_zero_iff]
     exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
   rw [set_lintegral_congr_fun measurableSet_Ioi (eventually_of_forall h_int)]
-  set f := fun t : ℝ ↦ volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
-  set mB := volume (Metric.ball (0 : E) 1)
+  set f := fun t : ℝ ↦ μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
+  set mB := μ (Metric.ball (0 : E) 1)
   -- the next two inequalities are in fact equalities but we don't need that
   calc
     ∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
@@ -122,7 +122,7 @@ theorem finite_integral_one_add_norm [MeasureSpace E] [BorelSpace E]
   · -- We use estimates from auxiliary lemmas to deal with integral from `0` to `1`
     have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1,
         f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦ by
-      refine' volume.addHaar_closedBall (0 : E) _
+      refine' μ.addHaar_closedBall (0 : E) _
       rw [sub_nonneg]
       exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
     rw [set_lintegral_congr_fun measurableSet_Ioc (ae_of_all _ h_int'),
@@ -138,20 +138,21 @@ theorem finite_integral_one_add_norm [MeasureSpace E] [BorelSpace E]
     exact WithTop.zero_lt_top
 #align finite_integral_one_add_norm finite_integral_one_add_norm
 
-theorem integrable_one_add_norm [MeasureSpace E] [BorelSpace E] [(@volume E _).IsAddHaarMeasure]
-    {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : Integrable fun x : E => (1 + ‖x‖) ^ (-r) := by
+theorem integrable_one_add_norm [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
+    [μ.IsAddHaarMeasure]
+    {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) : Integrable (fun x : E => (1 + ‖x‖) ^ (-r)) μ := by
   constructor
   · measurability
   -- Lower Lebesgue integral
-  have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖₊) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) :=
+  have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖₊ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
     lintegral_nnnorm_eq_of_nonneg fun _ => rpow_nonneg (by positivity) _
   rw [HasFiniteIntegral, this]
   exact finite_integral_one_add_norm hnr
 #align integrable_one_add_norm integrable_one_add_norm
 
-theorem integrable_rpow_neg_one_add_norm_sq [MeasureSpace E] [BorelSpace E]
-    [(@volume E _).IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
-    Integrable fun x : E => ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2) := by
+theorem integrable_rpow_neg_one_add_norm_sq [MeasurableSpace E] [BorelSpace E] {μ : Measure E}
+    [μ.IsAddHaarMeasure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
+    Integrable (fun x : E => ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2)) μ := by
   have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
   refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
     ?_ (eventually_of_forall fun x => ?_)