feat(Analysis/Fourier): Plancherel's theorem (#29860)

The Plancherel theorem states that the Fourier transform is unitary on L^2. We prove the main step which is that the Fourier transform on Schwartz space preserves the L^2-norm.

Author: mcdoll

Mathlib/Analysis/Complex/Basic.lean

@@ -245,6 +245,9 @@ theorem conjCLE_apply (z : ℂ) : conjCLE z = conj z :=
 def ofRealLI : ℝ →ₗᵢ[ℝ] ℂ :=
   ⟨ofRealAm.toLinearMap, norm_real⟩
 
+@[simp]
+theorem ofRealLI_apply (x : ℝ) : ofRealLI x = x := rfl
+
 theorem isometry_ofReal : Isometry ((↑) : ℝ → ℂ) :=
   ofRealLI.isometry
 

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -16,13 +16,15 @@ functions, in `fourierTransformCLM`. It is also given as a continuous linear equ
 -/
 
 open Real MeasureTheory MeasureTheory.Measure
-open scoped FourierTransform
+open scoped FourierTransform ComplexInnerProductSpace
 
 namespace SchwartzMap
 
 variable
   (𝕜 : Type*) [RCLike 𝕜]
+  {W : Type*} [NormedAddCommGroup W] [NormedSpace ℂ W] [NormedSpace 𝕜 W]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F]
   {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
   [MeasurableSpace V] [BorelSpace V]
 
@@ -80,6 +82,68 @@ noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
 
 variable [CompleteSpace E]
 
+@[simp]
+theorem fourier_inversion (f : 𝓢(V, E)) (x : V) : 𝓕⁻ (𝓕 f) x = f x :=
+  Integrable.fourier_inversion f.integrable (fourierTransformCLM ℂ f).integrable
+    f.continuous.continuousAt
+
+@[simp]
+theorem fourier_inversion_inv (f : 𝓢(V, E)) (x : V) : 𝓕 (𝓕⁻ f) x = f x :=
+  Integrable.fourier_inversion_inv f.integrable (fourierTransformCLM ℂ f).integrable
+    f.continuous.continuousAt
+
+variable
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [NormedSpace 𝕜 F] [SMulCommClass ℂ 𝕜 F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G]
+
+variable [CompleteSpace F]
+
+/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
+Version where the multiplication is replaced by a general bilinear form `M`. -/
+theorem integral_bilin_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L[ℂ] F →L[ℂ] G) :
+    ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕 g x) := by
+  have := VectorFourier.integral_bilin_fourierIntegral_eq_flip M (μ := volume) (ν := volume)
+    (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
+  rwa [flip_innerₗ] at this
+
+theorem integral_sesq_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
+    ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ g x) := by
+  have := VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip M (μ := volume) (ν := volume)
+    (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
+  rwa [flip_innerₗ] at this
+
+/-- Plancherel's theorem for Schwartz functions.
+
+Version where the multiplication is replaced by a general bilinear form `M`. -/
+theorem integral_sesq_fourier_fourier (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
+    ∫ ξ, M (𝓕 f ξ) (𝓕 g ξ) = ∫ x, M (f x) (g x) := by
+  simpa only [fourierTransformCLM_apply, fourier_inversion]
+    using integral_sesq_fourierIntegral_eq f (fourierTransformCLM ℂ g) M
+
+variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+
+/-- Plancherel's theorem for Schwartz functions. -/
+theorem integral_inner_fourier_fourier (f g : 𝓢(V, H)) :
+    ∫ ξ, ⟪𝓕 f ξ, 𝓕 g ξ⟫ = ∫ x, ⟪f x, g x⟫ :=
+  integral_sesq_fourier_fourier f g (innerSL ℂ)
+
+theorem integral_norm_sq_fourier (f : 𝓢(V, H)) :
+    ∫ ξ, ‖𝓕 f ξ‖^2 = ∫ x, ‖f x‖^2 := by
+  apply Complex.ofRealLI.injective
+  simp only [← LinearIsometry.integral_comp_comm]
+  convert integral_inner_fourier_fourier f f <;>
+  simp [inner_self_eq_norm_sq_to_K]
+
+theorem inner_fourierTransformCLM_toL2_eq (f : 𝓢(V, H)) :
+    ⟪(fourierTransformCLM ℂ f).toLp 2, (fourierTransformCLM ℂ f).toLp 2⟫ =
+    ⟪f.toLp 2, f.toLp 2⟫ := by
+  simp only [inner_toL2_toL2_eq]
+  exact integral_sesq_fourier_fourier f f (innerSL ℂ)
+
+theorem norm_fourierTransformCLM_toL2_eq (f : 𝓢(V, H)) :
+    ‖(fourierTransformCLM ℂ f).toLp 2‖ = ‖f.toLp 2‖ := by
+  simp_rw [norm_eq_sqrt_re_inner (𝕜 := ℂ), inner_fourierTransformCLM_toL2_eq]
+
 /-- 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

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -13,6 +13,7 @@ import Mathlib.Analysis.SpecialFunctions.JapaneseBracket
 import Mathlib.Topology.Algebra.UniformFilterBasis
 import Mathlib.MeasureTheory.Integral.IntegralEqImproper
 import Mathlib.Tactic.MoveAdd
+import Mathlib.MeasureTheory.Function.L2Space
 
 /-!
 # Schwartz space
@@ -67,7 +68,7 @@ noncomputable section
 
 open scoped Nat NNReal ContDiff
 
-variable {𝕜 𝕜' D E F G V : Type*}
+variable {𝕜 𝕜' D E F G H V : Type*}
 variable [NormedAddCommGroup E] [NormedSpace ℝ E]
 variable [NormedAddCommGroup F] [NormedSpace ℝ F]
 
@@ -1416,6 +1417,25 @@ theorem continuous_toLp {p : ℝ≥0∞} [Fact (1 ≤ p)] {μ : Measure E} [hμ
 
 end Lp
 
+section L2
+
+open MeasureTheory
+
+variable [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H]
+  [MeasurableSpace H] [BorelSpace H]
+  [NormedAddCommGroup V] [InnerProductSpace ℂ V]
+
+@[simp]
+theorem inner_toL2_toL2_eq (f g : 𝓢(H, V)) (μ : Measure H := by volume_tac) [μ.HasTemperateGrowth] :
+    inner ℂ (f.toLp 2 μ) (g.toLp 2 μ) = ∫ x, inner ℂ (f x) (g x) ∂μ := by
+  apply integral_congr_ae
+  have hf_ae := f.coeFn_toLp 2 μ
+  have hg_ae := g.coeFn_toLp 2 μ
+  filter_upwards [hf_ae, hg_ae] with _ hf hg
+  rw [hf, hg]
+
+end L2
+
 section integration_by_parts
 
 open ENNReal MeasureTheory

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -167,9 +167,39 @@ variable [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [TopologicalSpace V] [
   {e : AddChar 𝕜 𝕊} {μ : Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜}
   {ν : Measure W} [SigmaFinite μ] [SigmaFinite ν] [SecondCountableTopology V]
 
-variable [CompleteSpace E] [CompleteSpace F]
+variable {σ : ℂ →+* ℂ} [RingHomIsometric σ]
+
+/-- Fubini's theorem for the Fourier integral.
 
+This is the main technical step in proving both Parseval's identity and self-adjointness of the
+Fourier transform. -/
+theorem integral_fourierIntegral_swap
+    {f : V → E} {g : W → F} (M : F →L[ℂ] E →SL[σ] G) (he : Continuous e)
+    (hL : Continuous fun p : V × W ↦ L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
+    ∫ ξ, (∫ x, M (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν =
+    ∫ x, (∫ ξ, M (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ := by
+  rw [integral_integral_swap]
+  have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
+    (hg.norm.mul_prod hf.norm).const_mul _
+  apply this.mono
+  · change AEStronglyMeasurable (fun p : W × V ↦ (M (g p.1) (e (-(L p.2) p.1) • f p.2) )) _
+    have A : AEStronglyMeasurable (fun (p : W × V) ↦ e (-L p.2 p.1) • f p.2) (ν.prod μ) := by
+      refine (Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd
+      exact he.comp (hL.comp continuous_swap).neg
+    have A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2) : W × V → F × E)
+      (Measure.prod ν μ) := hg.1.comp_fst.prodMk A
+    have hM : Continuous (fun q ↦ M q.1 q.2 : F × E → G) :=
+      -- There is no `Continuous.clm_apply` for semilinear continuous maps
+      (M.flip.cont.comp continuous_snd).clm_apply continuous_fst
+    apply hM.comp_aestronglyMeasurable A' -- `exact` works, but `apply` is 10x faster!
+  · filter_upwards with ⟨ξ, x⟩
+    simp only [Function.uncurry_apply_pair, norm_mul, norm_norm, ge_iff_le, ← mul_assoc]
+    convert M.le_opNorm₂ (g ξ) (e (-L x ξ) • f x) using 2
+    simp
+
+variable [CompleteSpace E] [CompleteSpace F]
 /-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
+
 Version where the multiplication is replaced by a general bilinear form `M`. -/
 theorem integral_bilin_fourierIntegral_eq_flip
     {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous e)
@@ -178,33 +208,15 @@ theorem integral_bilin_fourierIntegral_eq_flip
       ∫ x, M (f x) (fourierIntegral e ν L.flip g x) ∂μ := by
   by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
   calc
-  _ = ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν := rfl
-  _ = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
+  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
+    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
     congr with ξ
     apply (ContinuousLinearMap.integral_comp_comm _ _).symm
     exact (fourierIntegral_convergent_iff he hL _).2 hf
-  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ := by
-    rw [integral_integral_swap]
-    have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
-      (hg.norm.mul_prod hf.norm).const_mul _
-    apply this.mono
-    · -- This proof can be golfed but becomes very slow; breaking it up into steps
-      -- speeds up compilation.
-      change AEStronglyMeasurable (fun p : W × V ↦ (M (e (-(L p.2) p.1) • f p.2) (g p.1))) _
-      have A : AEStronglyMeasurable (fun (p : W × V) ↦ e (-L p.2 p.1) • f p.2) (ν.prod μ) := by
-        refine (Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd
-        exact he.comp (hL.comp continuous_swap).neg
-      have A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2) : W × V → F × E)
-        (Measure.prod ν μ) := hg.1.comp_fst.prodMk A
-      have B : Continuous (fun q ↦ M q.2 q.1 : F × E → G) := M.flip.continuous₂
-      apply B.comp_aestronglyMeasurable A' -- `exact` works, but `apply` is 10x faster!
-    · filter_upwards with ⟨ξ, x⟩
-      rw [Function.uncurry_apply_pair, Submonoid.smul_def, (M.flip (g ξ)).map_smul,
-        ← Submonoid.smul_def, Circle.norm_smul, ContinuousLinearMap.flip_apply,
-        norm_mul, norm_norm M, norm_mul, norm_norm, norm_norm, mul_comm (‖g _‖), ← mul_assoc]
-      exact M.le_opNorm₂ (f x) (g ξ)
+  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
+    integral_fourierIntegral_swap M.flip he hL hf hg
   _ = ∫ x, (∫ ξ, M (f x) (e (-L.flip ξ x) • g ξ) ∂ν) ∂μ := by
-      simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
+    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
       ContinuousLinearMap.coe_smul', Pi.smul_apply, LinearMap.flip_apply]
   _ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ := by
     congr with x
@@ -220,6 +232,42 @@ theorem integral_fourierIntegral_smul_eq_flip
       ∫ x, (f x) • (fourierIntegral e ν L.flip g x) ∂μ :=
   integral_bilin_fourierIntegral_eq_flip (ContinuousLinearMap.lsmul ℂ ℂ) he hL hf hg
 
+/-- The Fourier transform satisfies `∫ 𝓕 f * conj g = ∫ f * conj (𝓕⁻¹ g)`, which together
+with the Fourier inversion theorem yields Plancherel's theorem. The stated version is more
+convenient since it does only require integrability of `f` and `g`.
+
+Version where the multiplication is replaced by a general bilinear form `M`. -/
+theorem integral_sesq_fourierIntegral_eq_neg_flip
+    {f : V → E} {g : W → F} (M : E →L⋆[ℂ] F →L[ℂ] G) (he : Continuous e)
+    (hL : Continuous fun p : V × W ↦ L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
+    ∫ ξ, M (fourierIntegral e μ L f ξ) (g ξ) ∂ν =
+      ∫ x, M (f x) (fourierIntegral e ν (-L.flip) g x) ∂μ := by
+  by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
+  calc
+  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
+    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
+    congr with ξ
+    apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm
+    exact (fourierIntegral_convergent_iff he hL _).2 hf
+  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
+    integral_fourierIntegral_swap M.flip he hL hf hg
+  _ = ∫ x, (∫ ξ, M (f x) (e (L.flip ξ x) • g ξ) ∂ν) ∂μ := by
+    congr with x
+    congr with ξ
+    rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
+    simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
+      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
+      inv_inv]
+  _ = ∫ x, (∫ ξ, M (f x) (e (-(-L.flip ξ) x) • g ξ) ∂ν) ∂μ := by
+    simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
+      neg_neg]
+  _ = ∫ x, M (f x) (∫ ξ, e (-(-L.flip ξ) x) • g ξ ∂ν) ∂μ := by
+    congr with x
+    apply ContinuousLinearMap.integral_comp_comm
+    have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
+      (continuous_neg.comp hL).comp continuous_swap
+    exact (fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg
+
 end Fubini
 
 lemma fourierIntegral_probChar {V W : Type*} {_ : MeasurableSpace V}

docs/1000.yaml

@@ -1942,7 +1942,9 @@ Q2094241:
 
 Q2096184:
   title: Plancherel theorem
-  # also in undergrad.yml
+  decl: SchwartzMap.integral_inner_fourier_fourier
+  authors: Moritz Doll
+  date: 2025
 
 Q2109761:
   title: Uniformization theorem

docs/undergrad.yaml

@@ -536,7 +536,7 @@ Measures and integral calculus:
     Parseval theorem: 'tsum_sq_fourierCoeff'
     Fourier transform on $\mathrm{L}^1(\R^d)$: 'Real.fourierIntegral'
     Fourier transform on $\mathrm{L}^2(\R^d)$: ''
-    Plancherel’s theorem: ''
+    Plancherel’s theorem: 'SchwartzMap.integral_inner_fourier_fourier'
     Fourier inversion formula: 'Continuous.fourier_inversion'
 
 # 11.