Fourier transform on Schwartz functions

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.

def SchwartzMap.fourierTransformCLM (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : SchwartzMap V E →L[𝕜] SchwartzMap V E

The Fourier transform on a real inner product space, as a continuous linear map on the Schwartz space.

Equations

• SchwartzMap.fourierTransformCLM 𝕜 = SchwartzMap.mkCLM (fun (x : SchwartzMap V E) => FourierTransform.fourier ⇑x) ⋯ ⋯ ⋯ ⋯

instance SchwartzMap.instFourierTransform {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : FourierTransform (SchwartzMap V E) (SchwartzMap V E)

Equations

• SchwartzMap.instFourierTransform = { fourier := fun (f : SchwartzMap V E) => (SchwartzMap.fourierTransformCLM ℂ) f }

theorem SchwartzMap.fourier_coe {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : ⇑(FourierTransform.fourier f) = FourierTransform.fourier ⇑f

instance SchwartzMap.instFourierModule (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : FourierModule 𝕜 (SchwartzMap V E) (SchwartzMap V E)

Equations

• SchwartzMap.instFourierModule 𝕜 = { toFourierTransform := SchwartzMap.instFourierTransform, fourier_add := ⋯, fourier_smul := ⋯ }

@[simp]

theorem SchwartzMap.fourierTransformCLM_apply (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : (fourierTransformCLM 𝕜) f = FourierTransform.fourier f

instance SchwartzMap.instFourierTransformInv {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : FourierTransformInv (SchwartzMap V E) (SchwartzMap V E)

Equations

• One or more equations did not get rendered due to their size.

theorem SchwartzMap.fourierInv_coe {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : ⇑(FourierTransformInv.fourierInv f) = FourierTransformInv.fourierInv ⇑f

instance SchwartzMap.instFourierInvModule (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : FourierInvModule 𝕜 (SchwartzMap V E) (SchwartzMap V E)

Equations

• SchwartzMap.instFourierInvModule 𝕜 = { toFourierTransformInv := SchwartzMap.instFourierTransformInv, fourierInv_add := ⋯, fourierInv_smul := ⋯ }

instance SchwartzMap.instFourierPair {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] : FourierPair (SchwartzMap V E) (SchwartzMap V E)

instance SchwartzMap.instFourierInvPair {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] : FourierInvPair (SchwartzMap V E) (SchwartzMap V E)

@[deprecated FourierPair.fourierInv_fourier_eq (since := "2025-11-13")]

theorem SchwartzMap.fourier_inversion {E : Type u_1} {F : Type u_2} {inst✝ : FourierTransform E F} {inst✝¹ : FourierTransformInv F E} [self : FourierPair E F] (f : E) : FourierTransformInv.fourierInv (FourierTransform.fourier f) = f

Alias of FourierPair.fourierInv_fourier_eq.

@[deprecated FourierInvPair.fourier_fourierInv_eq (since := "2025-11-13")]

theorem SchwartzMap.fourier_inversion_inv {E : Type u_1} {F : Type u_2} {inst✝ : FourierTransform F E} {inst✝¹ : FourierTransformInv E F} [self : FourierInvPair E F] (f : E) : FourierTransform.fourier (FourierTransformInv.fourierInv f) = f

Alias of FourierInvPair.fourier_fourierInv_eq.

def SchwartzMap.fourierTransformCLE (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] : SchwartzMap V E ≃L[𝕜] SchwartzMap V E

The Fourier transform on a real inner product space, as a continuous linear equiv on the Schwartz space.

Equations

• SchwartzMap.fourierTransformCLE 𝕜 = { toLinearEquiv := FourierTransform.fourierEquiv 𝕜 (SchwartzMap V E) (SchwartzMap V E), continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem SchwartzMap.fourierTransformCLE_apply (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] (f : SchwartzMap V E) : (fourierTransformCLE 𝕜) f = FourierTransform.fourier f

@[simp]

theorem SchwartzMap.fourierTransformCLE_symm_apply (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] (f : SchwartzMap V E) : (fourierTransformCLE 𝕜).symm f = FourierTransformInv.fourierInv f

theorem SchwartzMap.integral_bilin_fourier_eq {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransform.fourier g) x)

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.

@[deprecated SchwartzMap.integral_bilin_fourier_eq (since := "2025-11-16")]

theorem SchwartzMap.integral_bilin_fourierIntegral_eq {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransform.fourier g) x)

Alias of SchwartzMap.integral_bilin_fourier_eq.

---

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 SchwartzMap.integral_sesq_fourier_eq {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)

@[deprecated SchwartzMap.integral_sesq_fourier_eq (since := "2025-11-16")]

theorem SchwartzMap.integral_sesq_fourierIntegral_eq {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)

Alias of SchwartzMap.integral_sesq_fourier_eq.

theorem SchwartzMap.integral_sesq_fourier_fourier {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) ((FourierTransform.fourier g) ξ) = ∫ (x : V), (M (f x)) (g x)

Plancherel's theorem for Schwartz functions.

Version where the multiplication is replaced by a general bilinear form M.

theorem SchwartzMap.integral_inner_fourier_fourier {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f g : SchwartzMap V H) : ∫ (ξ : V), inner ℂ ((FourierTransform.fourier f) ξ) ((FourierTransform.fourier g) ξ) = ∫ (x : V), inner ℂ (f x) (g x)

Plancherel's theorem for Schwartz functions.

theorem SchwartzMap.integral_norm_sq_fourier {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : ∫ (ξ : V), ‖(FourierTransform.fourier f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

theorem SchwartzMap.inner_fourier_toL2_eq {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : inner ℂ ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume) ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume) = inner ℂ (f.toLp 2 MeasureTheory.volume) (f.toLp 2 MeasureTheory.volume)

@[deprecated SchwartzMap.inner_fourier_toL2_eq (since := "2025-11-13")]

theorem SchwartzMap.inner_fourierTransformCLM_toL2_eq {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : inner ℂ ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume) ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume) = inner ℂ (f.toLp 2 MeasureTheory.volume) (f.toLp 2 MeasureTheory.volume)

Alias of SchwartzMap.inner_fourier_toL2_eq.

@[simp]

theorem SchwartzMap.norm_fourier_toL2_eq {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : ‖(FourierTransform.fourier f).toLp 2 MeasureTheory.volume‖ = ‖f.toLp 2 MeasureTheory.volume‖

@[deprecated SchwartzMap.norm_fourier_toL2_eq (since := "2025-11-13")]

theorem SchwartzMap.norm_fourierTransformCLM_toL2_eq {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {H : Type u_6} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : ‖(FourierTransform.fourier f).toLp 2 MeasureTheory.volume‖ = ‖f.toLp 2 MeasureTheory.volume‖

Alias of SchwartzMap.norm_fourier_toL2_eq.