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.

noncomputable 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) => Real.fourierIntegral ⇑x) ⋯ ⋯ ⋯ ⋯

@[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) = Real.fourierIntegral ⇑f

@[simp]

theorem SchwartzMap.fourier_inversion {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] (f : SchwartzMap V E) (x : V) : Real.fourierIntegralInv (Real.fourierIntegral ⇑f) x = f x

@[simp]

theorem SchwartzMap.fourier_inversion_inv {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] (f : SchwartzMap V E) (x : V) : Real.fourierIntegral (Real.fourierIntegralInv ⇑f) x = f x

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] [CompleteSpace E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M (Real.fourierIntegral (⇑f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) (Real.fourierIntegral (⇑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.

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] [CompleteSpace E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M (Real.fourierIntegral (⇑f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) (Real.fourierIntegralInv (⇑g) x)

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] [CompleteSpace E] {F : Type u_6} [NormedAddCommGroup F] [NormedSpace ℂ F] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace F] (f : SchwartzMap V E) (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G) : ∫ (ξ : V), (M (Real.fourierIntegral (⇑f) ξ)) (Real.fourierIntegral (⇑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_8} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f g : SchwartzMap V H) : ∫ (ξ : V), inner ℂ (Real.fourierIntegral (⇑f) ξ) (Real.fourierIntegral (⇑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_8} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H) : ∫ (ξ : V), ‖Real.fourierIntegral (⇑f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

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

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

noncomputable 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

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

@[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) = Real.fourierIntegral ⇑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) = Real.fourierIntegralInv ⇑f