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_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [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_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : ⇑((fourierTransformCLM 𝕜) f) = Real.fourierIntegral ⇑f

noncomputable def SchwartzMap.fourierTransformCLE (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [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_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [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_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] (f : SchwartzMap V E) : ⇑((fourierTransformCLE 𝕜).symm f) = Real.fourierIntegralInv ⇑f