feat: expand basic API around Fourier integrals (#12153)

The statements in this PR are mostly straightforward variations around already existing statements, which have proved useful down the road.

Author: sgouezel

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -120,7 +120,7 @@ section Continuous
 
 /-! In this section we assume 𝕜, `V`, `W` have topologies,
   and `L`, `e` are continuous (but `f` needn't be).
-   This is used to ensure that `e [-L v w]` is (a.e. strongly) measurable. We could get away with
+   This is used to ensure that `e (-L v w)` is (a.e. strongly) measurable. We could get away with
    imposing only a measurable-space structure on 𝕜 (it doesn't have to be the Borel sigma-algebra of
    a topology); but it seems hard to imagine cases where this extra generality would be useful, and
    allowing it would complicate matters in the most important use cases.
@@ -241,6 +241,38 @@ end Fubini
 
 end VectorFourier
 
+namespace VectorFourier
+
+variable {𝕜 ι E F V W : Type*} [Fintype ι] [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup V] [NormedSpace 𝕜 V] [MeasurableSpace V] [BorelSpace V]
+  [NormedAddCommGroup W] [NormedSpace 𝕜 W] [MeasurableSpace W] [BorelSpace W]
+  {e : AddChar 𝕜 𝕊} {μ : Measure V} {L : V →L[𝕜] W →L[𝕜] 𝕜}
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace ℝ (M i)]
+
+theorem fourierIntegral_continuousLinearMap_apply
+    {f : V → (F →L[ℝ] E)} {a : F} {w : W} (he : Continuous e) (hf : Integrable f μ) :
+    fourierIntegral e μ L.toLinearMap₂ f w a =
+      fourierIntegral e μ L.toLinearMap₂ (fun x ↦ f x a) w := by
+  rw [fourierIntegral, ContinuousLinearMap.integral_apply]
+  · rfl
+  · apply (fourierIntegral_convergent_iff he _ _).2 hf
+    exact L.continuous₂
+
+theorem fourierIntegral_continuousMultilinearMap_apply
+    {f : V → (ContinuousMultilinearMap ℝ M E)} {m : (i : ι) → M i} {w : W} (he : Continuous e)
+    (hf : Integrable f μ) :
+    fourierIntegral e μ L.toLinearMap₂ f w m =
+      fourierIntegral e μ L.toLinearMap₂ (fun x ↦ f x m) w := by
+  rw [fourierIntegral, ContinuousMultilinearMap.integral_apply]
+  · rfl
+  · apply (fourierIntegral_convergent_iff he _ _).2 hf
+    exact L.continuous₂
+
+end VectorFourier
+
+
 /-! ## Fourier theory for functions on `𝕜` -/
 
 
@@ -333,8 +365,31 @@ theorem fourierIntegral_convergent_iff' {V W : Type*} [NormedAddCommGroup V] [No
   VectorFourier.fourierIntegral_convergent_iff (E := E) (L := L.toLinearMap₂)
     continuous_fourierChar L.continuous₂ _
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
-  {V : Type*} [NormedAddCommGroup V]
+section Apply
+
+variable {ι F V W : Type*} [Fintype ι]
+  [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
+  [NormedAddCommGroup W] [NormedSpace ℝ W] [MeasurableSpace W] [BorelSpace W]
+  {μ : Measure V} {L : V →L[ℝ] W →L[ℝ] ℝ}
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup E] [NormedSpace ℂ E]
+  {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace ℝ (M i)]
+
+theorem fourierIntegral_continuousLinearMap_apply'
+    {f : V → (F →L[ℝ] E)} {a : F} {w : W} (hf : Integrable f μ) :
+    VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f w a =
+      VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (fun x ↦ f x a) w :=
+  VectorFourier.fourierIntegral_continuousLinearMap_apply continuous_fourierChar hf
+
+theorem fourierIntegral_continuousMultilinearMap_apply'
+    {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {w : W} (hf : Integrable f μ) :
+    VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f w m =
+      VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (fun x ↦ f x m) w :=
+  VectorFourier.fourierIntegral_continuousMultilinearMap_apply continuous_fourierChar hf
+
+end Apply
+
+variable {V : Type*} [NormedAddCommGroup V]
   [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
   {W : Type*} [NormedAddCommGroup W]
   [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W]
@@ -370,15 +425,27 @@ lemma fourierIntegralInv_eq' (f : V → E) (w : V) :
     𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
   simp_rw [fourierIntegralInv_eq, Submonoid.smul_def, Real.fourierChar_apply]
 
-lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V → E) (w : V) :
-    𝓕⁻ f w = 𝓕 f (-w) := by
-  simp [fourierIntegral_eq, fourierIntegralInv_eq]
-
 lemma fourierIntegral_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
     𝓕 (f ∘ A) w = (𝓕 f) (A w) := by
   simp only [fourierIntegral_eq, ← A.inner_map_map, Function.comp_apply, ←
     MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]
 
+lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V → E) (w : V) :
+    𝓕⁻ f w = 𝓕 f (-w) := by
+  simp [fourierIntegral_eq, fourierIntegralInv_eq]
+
+lemma fourierIntegralInv_eq_fourierIntegral_comp_neg (f : V → E) :
+    𝓕⁻ f = 𝓕 (fun x ↦ f (-x)) := by
+  ext y
+  rw [fourierIntegralInv_eq_fourierIntegral_neg]
+  change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y
+  exact (fourierIntegral_comp_linearIsometry _ _ _).symm
+
+lemma fourierIntegralInv_comm (f : V → E) :
+    𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f) := by
+  conv_rhs => rw [fourierIntegralInv_eq_fourierIntegral_comp_neg]
+  simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg]
+
 lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
     𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w) := by
   simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]
@@ -403,4 +470,16 @@ theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
     Integrable (fun v : V ↦ 𝐞 (- ⟪v, w⟫) • f v) μ ↔ Integrable f μ :=
   fourierIntegral_convergent_iff' (innerSL ℝ) w
 
+theorem fourierIntegral_continuousLinearMap_apply
+    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+    {f : V → (F →L[ℝ] E)} {a : F} {v : V} (hf : Integrable f) :
+    𝓕 f v a = 𝓕 (fun x ↦ f x a) v :=
+  fourierIntegral_continuousLinearMap_apply' (L := innerSL ℝ) hf
+
+theorem fourierIntegral_continuousMultilinearMap_apply {ι : Type*} [Fintype ι]
+    {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace ℝ (M i)]
+    {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {v : V} (hf : Integrable f) :
+    𝓕 f v m = 𝓕 (fun x ↦ f x m) v :=
+  fourierIntegral_continuousMultilinearMap_apply' (L := innerSL ℝ) hf
+
 end Real

Mathlib/Analysis/Fourier/Inversion.lean

@@ -170,3 +170,21 @@ theorem Continuous.fourier_inversion (h : Continuous f)
     𝓕⁻ (𝓕 f) = f := by
   ext v
   exact hf.fourier_inversion h'f h.continuousAt
+
+/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
+space is integrable, and its Fourier transform `𝓕 f` is also integrable, then `𝓕 (𝓕⁻ f) = f` at
+continuity points of `f`. -/
+theorem MeasureTheory.Integrable.fourier_inversion_inv
+    (hf : Integrable f) (h'f : Integrable (𝓕 f)) {v : V}
+    (hv : ContinuousAt f v) : 𝓕 (𝓕⁻ f) v = f v := by
+  rw [fourierIntegralInv_comm]
+  exact fourier_inversion hf h'f hv
+
+/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
+space is continuous, integrable, and its Fourier transform `𝓕 f` is also integrable,
+then `𝓕 (𝓕⁻ f) = f`. -/
+theorem Continuous.fourier_inversion_inv (h : Continuous f)
+    (hf : Integrable f) (h'f : Integrable (𝓕 f)) :
+    𝓕 (𝓕⁻ f) = f := by
+  ext v
+  exact hf.fourier_inversion_inv h'f h.continuousAt